A direct proof of univalence from uaβ and uaη#1069

Merged

mortberg merged 3 commits intoagda:masterfrom phijor:phijor/univalence-from-eta-beta

Nov 3, 2023

+95-44

Commits on Nov 3, 2023

transpEquiv: Transporting from an extent to i1 is an equivalence
phijor
committed
Move direct proof of uaη to Cubical.Foundations.Univalence
phijor
committed
Direct proof of univalence avoiding induction on paths & equivalences
phijor
committed