Dan Christensen

`image` as well. The issue is that if I `Require Import HoTT` in external work, I now get the versions from Sets/Ordinal.v by default.

It probably won't scale to keep everything globally unique all of the time, but it is handy when things are mostly unique, so that you can tell locally what something...

It turns out that Ordinals.v could just use `Modality.image (Tr (-1)) f` and the related facts about it, except for one minor thing: currently Ordinals.v defines its `image` using `HIT.quotient`...

I started this, but got bogged down a bit. Here are the steps I was thinking of: - Change `HIT.quotient` to not cheat with universes. Probably simplest to just assume...

Thanks for pointing that out! So one task is: - Remove HIT.quotient from the library, and use Colimits/Quotient instead. The good news is that that is really orthogonal to the...

It's definitely important to be able to talk about equivalences between types in different universes. E.g. the formalization of one of my recent preprints has ``` Record IsSmall@{i j |...

No, it doesn't work, since I don't want to assume `i

I also don't see what this has to do with the error message in the initial comment in this issue. Why are the universes the same in some cases and...

Since one can just type `apply equiv_inverse`, which is easy and clear, I don't think it's a good idea to make `symmetry` clever. Then a reader would have to go...

I think some minimal compatibility with the Coq stdlib is useful, but for types that are unique to HoTT, we might as well be systematic.