3 ms·
I'm no expert, but I believe the hope is that quotients are easier to work with in HoTT than they would be elsewhere since you can treat the resulting "cosets"
by tel 12y ago
I'm no expert, but I believe the hope is that quotients are easier to work with in HoTT than they would be elsewhere since you can treat the resulting "cosets" as true objects instead of structure with proof.
Also, it should be much easier to transport proofs from type to type according to isomorphisms that are discovered.
I'm hardly versed enough to say whether those things are (a) true (b) actually occurring (c) powerful enough to be worth the potential headaches HoTT incurs or (d) deserving of acclaim, but it's at least my understanding.
- jbapple 12y agoAs far as quotients go, I have used setoids before for that purpose. Maybe HoTT makes quotients even more convenient. http://coq.inria.fr/V8.2pl1/refman/Reference-Manual030.html http://coq.inria.fr/V8.2pl1/refman/Reference-Manual030.html
- tel 12y agoYes, my understanding is that quotients should be much more convenient to use than setoids. Univalance means you can more or less ignore equality in the quotient after you define it---proofs should just be transportable.