24 Sep
2010
24 Sep
'10
12:50 p.m.
Intensional Id-types might be convenient for providing a logic where equality gets identified with isomorphism or even weak equivalence. But that's not avoiding equality it's rather `liberal'ising it.
Vladimir Voevodsky just posted a draft manuscript about these issues: http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations.html Bas [For admin and other information see: http://www.mta.ca/~cat-dist/ ]