17 Sep
2010
17 Sep
'10
2:17 a.m.
Mike wrote:
If one defined the identity types and pullbacks using limits in Gpd in the kosher 2-categorical sense, then it seems to me that one should be able to define an equivalent model using arbitrary functors between groupoids to represent the dependent types, rather than merely the fibrations.
This seems (to me) to be analogous to extending one's notion of covering space to allow for empty fibres - indeed, the characterisation of covering spaces as representations of Pi_1 needs this. David PS +1 for using 'kosher' :) [For admin and other information see: http://www.mta.ca/~cat-dist/ ]