Improvements to Univalence.agda

[anshwad10]

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.

[anshwad10]

fixing pathToEquiv is also on my todo list; currently invEq (pathToEquiv p) does not reduce to transport (sym p) which really bugs me

[mortberg]

Sounds like very good improvements to me. Let me know when it's ready for review and I'll take a closer look

[anshwad10]

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

[ecavallo]

(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: #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.)

[anshwad10]

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.

[anshwad10]

I could also change the definition of isEquivTransp, which is probably the better way

[anshwad10]

Once we have identity systems defined (#1254) I'll also prove that equivalences are an identity system and derive the computation rule for EquivJ