Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Set Quotients #18

Closed
Saizan opened this issue Dec 10, 2014 · 2 comments
Closed

Set Quotients #18

Saizan opened this issue Dec 10, 2014 · 2 comments

Comments

@Saizan
Copy link

Saizan commented Dec 10, 2014

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
Copy link
Contributor

favonia commented Sep 13, 2015 •
edited
Loading

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.

@favonia
Copy link
Contributor

favonia commented May 5, 2016

@Saizan I am going to assume the new quotient code is satisfactory. Feel free to re-open.

@favonia favonia closed this as completed May 5, 2016
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@Saizan @favonia