agda
Improvements to Univalence.agda
I had a few gripes with this file. First of all, I noticed that ua→ and ua→⁻ used transports unnecessarily, so I rewrote them and made it simpler, and while I was at it I also proved that ua→ is an equivalence. For this I needed the lemma ua-unglueIso and I also added commSqIsEq' to Equiv.agda which proves the other triangle identity for equivalences. I also rewrote uaInvEquiv and uaCompEquiv to use a direct proof instead of EquivJ. I also noticed that almost all the definitions in the module took {A B : Type ℓ} as implicit arguments, so I made them into private variables.
Also, I noticed the comment -- TODO: there should be a direct proof of this that doesn't use equivToIso about invEquiv so I might fix that in this PR as well later.
fixing pathToEquiv is also on my todo list; currently invEq (pathToEquiv p) does not reduce to transport (sym p) which really bugs me
Sounds like very good improvements to me. Let me know when it's ready for review and I'll take a closer look
So there is literally an unused better definition of pathToEquiv in Agda.Builtin.Cubical, so I'm gonna get rid of the current pathToEquiv and use the builtin one
(Mentioned this on Discord, repeating here for the record) We added a definition of pathToEquiv to the library with the intent of removing it from Agda.Builtin.Cubical: https://github.com/agda/cubical/issues/259. Is there anything stopping us from doing so now? (Which definition we should use here is a different question that I have not formed an opinion about.)
The current definition of pathToEquiv in the library is not that good, because equivTransp That's why I though it would be better to use the builtin one.
So I suppose I can inline that definition, or we can use isoToEquiv pathToIso. isoToEquiv pathToIso isn't perfectly optimized, because isoToEquiv has to mess up one of the units.
I could also change the definition of isEquivTransp, which is probably the better way
Once we have identity systems defined (#1254) I'll also prove that equivalences are an identity system and derive the computation rule for EquivJ