A direct proof of univalence from uaβ and uaη

[phijor]

While trying to resolve the duplication between uaη and uaTransportη mentioned in this comment, I noticed that together with uaβ this yields a very "cubical" proof of univalenceIso, avoiding induction on paths and equivalences completely. I attempted to code-golf away the use of isoToIsEquiv and prove isEquivPathToEquiv directly, but wasn't able to (at least not more efficiently).

In detail, the commits do the following:

• 0dcfa97 moves transpEquiv to Cubical.Foundations.Equiv.Base and generalizes it to arbitrary lines of types. Arguably, this should be called isEquivCoei→1 and live in *.CartesianKanOps, but there's a module dependency cycle involving that and *.GroupoidLaws that I'm not sure how to break.
• 39f61f4 moves the direct proof of uaη via Glue types from *.Transport to *.Univalence, deprecates uaTransportη in the former.
• cc06407 gives a direct proof of univalenceIso. The 1lab has a similar proof, they note however that uaη "is hard".

I'd like some feedback on these changes, so I'm marking this as a draft for now. In particular, I'm not sure how and where to place things in the module hierarchy, how to deprecate stuff (if at all), and whether the new proof is even better at all. Additionally, the improved proof of uaη is by @dolio originally, and I don't want the attribution to be lost.

Pinging @mortberg who encouraged the cleanup as part of #1017.

[mortberg]

I think this looks good. Any opinions @ecavallo ?

[ecavallo]

Seems fine to me.

[mortberg]

I marked this as ready for review so that I can make a proper review. It's nice to see that uaη has a direct proof, maybe the 1lab should be updated as well

[mortberg]

Just a suggestion and small request, otherwise very nice contribution!

[phijor]

Thanks, I took care of your requests. Once you're happy with the changes I will rebase and squash my commits.

[phijor]

I'm really unhappy having to add transpEquiv to Equiv.Base though. If #1001 gets merged, one could import from CartesianKanOps instead of having to add unrelated definitions to such a core module.

[mortberg]

I'm really unhappy having to add transpEquiv to Equiv.Base though. If #1001 gets merged, one could import from CartesianKanOps instead of having to add unrelated definitions to such a core module.

But isn't transpEquiv a very basic equivalence that fits in Equiv.Base? I'd rather have it there than in CartesianKanOps (which was mostly added as proof of concept and at least I did not envision it being used much elsewhere in the library)

[phijor]

Rebased on current master and squashed.

But isn't transpEquiv a very basic equivalence that fits in Equiv.Base?

Convinced. Let's leave it in Equiv.Base.

I'd rather have it there than in CartesianKanOps (which was mostly added as proof of concept and at least I did not envision it being used much elsewhere in the library)

I see. I think coe etc. could improve readability of some proofs (the 1lab uses it in quite a few places), but that's a discussion for another time.