37 ms·
As 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/Refere
by jbapple 12y ago
As 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.