Set Quotients
Saizan opened this issue · 2 comments
Saizan commented
would it make sense to port this definition of Set quotients from the Coq lib?
https://github.com/HoTT/HoTT/blob/master/theories/hit/quotient.v
The one in old/ makes use of spheres which seems overkill?
favonia commented
I put in something in /lib/types/SetQuotient.agda. Is it what you wanted? The one in old/ was done without (direct) truncation; nowadays truncations are more accepted as an inherent part of defining HITs.