2 May
2015
2 May
'15
6:50 p.m.
The groupoid model of Martin Hofmann and me does make sense in any topos with say NNO. For getting universes you need universes in the topos. But this is about getting split models. But I'd expect everything goes through also for non-split models. Thomas [For admin and other information see: http://www.mta.ca/~cat-dist/ ]