agda
Simplify `Embedding-into-hLevel→hLevel`
This small PR simplifies the proofs of Embedding-into-hLevel→hLevel and the two special cases for isProp and isSet.
Embedding-into-hLevel→hLevel was unnecessarily defined by case distinction. The reason is probably the definition of isOfHLevel by three instead of two cases:
https://github.com/agda/cubical/blob/a10e25a8c99efa3b1fee5fa70b8203cd70e88656/Cubical/Foundations/HLevels.agda#L44-L47
I assume there are good reasons for this definition of isOfHLevel, but I suppose it was not intended to spark unnecessary case distinctions in places like Embedding-into-hLevel→hLevel.
I have no clue why this was so complicated and I like the new simpler version. Maybe @aljungstrom knows more? (It could have had something to do with attempts to optimize things...)
Does not take longer than usual to type check on my machine. So there can't be any dramatic efficiency difference.
I would guess that is just about having definitional equalities between isOfHLevel 0 and isContr and isOfHLevel 1 and isProp, where isContr and isProp are defined like in the HoTT-Book. isSet then also fits in definitionally.
You did not change the definition of
isOfHLevel.
Correct.
The three-cases definition of isOfHLevel was introduced and discussed here: https://github.com/agda/cubical/pull/68