Alan Morrison wrote his MSc dissertation "Reasoning in Arithmetic Universes" in 1996 at the Department of Computing, Imperial College, under my supervision.

It is an excellent summary of much of what was known then about arithmetic universes from work, much of it still unpublished, of André Joyal and, following him, Gavin Wraith.