Add 1-Groupoid structure of equivalences #719
Conversation
Should we consider replacing [IsEquiv] with a definition that has more judgmental properties, and doesn't require [Funext] for proving all of the groupoid structure? (Is there such a definition?) This closes HoTT#703.
JasonGross
force-pushed
the
equiv-groupoids
branch
from
6739849
to
257840f
Compare
|
It would be nice to package this up in a tactic/ rewrite database. Nit: Without univalence this is only a pregroupoid, isn't it. |
|
Nice! LGTM.
I am very doubtful. |
I asked a question on the mailing list a while back about making more properties judgmental, and @peterlefanulumsdaine replied with a way to get judgmental involutivity of symmetry. That the inverse of the identity is the identity should also hold strictly for this definition. Looking more at it, if we add a weak-eta rule for inductive types to Coq, then the left and right units for paths are strict, and the left and right units for this definition of equivalence also become strict. It's not clear to me if/how we can strictify associativity for paths, but if we manage that, then it also becomes strict for this definition of equivalences. I don't think there's any hope for the left and right inverse laws, but this would still be much more than we have now. Should we consider switching? (Separate issue?) |
Yes. Should I rename the file? |
I will add a comment about pulling the relevant code from PathGroupoids. I don't want to write the tactic without using it anywhere, because then it is likely to break. |
Comment added
I've changed the title of the file, but will only change the filename if asked. |
|
I don't think it's worth renaming the file. In fact it's not even technically a pregroupoid but a pre-oo-groupoid... |
|
Peter's definition goes up a universe level, so I don't think we should use it. |
|
APOE? |
Add 1-Groupoid structure of equivalences
Should we consider replacing [IsEquiv] with a definition that has more
judgmental properties, and doesn't require [Funext] for proving all of
the groupoid structure? (Is there such a definition?)