Move direct proof of uaη to Cubical.Foundations.Univalence

This proof is due to @dolio, cf. commit e42a6fa.

Cubical/Foundations/Transport.agda

@@ -82,11 +82,8 @@ transpEquiv p = Equiv.transpEquiv (λ i → p i)
 {-# WARNING_ON_USAGE transpEquiv "Deprecated: Use the more general `transpEquiv` from `Cubical.Foundations.Equiv` instead" #-}
 
 uaTransportη : ∀ {ℓ} {A B : Type ℓ} (P : A ≡ B) → ua (pathToEquiv P) ≡ P
-uaTransportη P i j
-  = Glue (P i1) λ where
-      (j = i0) → P i0 , pathToEquiv P
-      (i = i1) → P j , transpEquiv P j
-      (j = i1) → P i1 , idEquiv (P i1)
+uaTransportη = uaη
+{-# WARNING_ON_USAGE uaTransportη "Deprecated: Use `uaη` from `Cubical.Foundations.Univalence` instead of `uaTransportη`" #-}
 
 pathToIso : ∀ {ℓ} {A B : Type ℓ} → A ≡ B → Iso A B
 Iso.fun (pathToIso x) = transport x

Cubical/Foundations/Univalence.agda

@@ -240,7 +240,14 @@ uaβ : {A B : Type ℓ} (e : A ≃ B) (x : A) → transport (ua e) x ≡ equivFu
 uaβ e x = transportRefl (equivFun e x)
 
 uaη : ∀ {A B : Type ℓ} → (P : A ≡ B) → ua (pathToEquiv P) ≡ P
-uaη = J (λ _ q → ua (pathToEquiv q) ≡ q) (cong ua pathToEquivRefl ∙ uaIdEquiv)
+uaη {A = A} {B = B} P i j = Glue B {φ = φ} sides where
+  -- Adapted from a proof by @dolio, cf. commit e42a6fa1
+  φ = i ∨ j ∨ ~ j
+
+  sides : Partial φ (Σ[ T ∈ Type _ ] T ≃ B)
+  sides (i = i1) = P j , transpEquiv (λ k → P k) j
+  sides (j = i0) = A , pathToEquiv P
+  sides (j = i1) = B , idEquiv B
 
 -- Lemmas for constructing and destructing dependent paths in a function type where the domain is ua.
 ua→ : ∀ {ℓ ℓ'} {A₀ A₁ : Type ℓ} {e : A₀ ≃ A₁} {B : (i : I) → Type ℓ'}

Cubical/Foundations/Univalence/Universe.agda

@@ -50,7 +50,7 @@ module UU-Lemmas where
     : ∀ x y (p : El x ≡ El y)
     → cong El (un x y (pathToEquiv p)) ≡ p
   cong-un-te x y p
-    = comp (pathToEquiv p) ∙ uaTransportη p
+    = comp (pathToEquiv p) ∙ uaη p
 
   nu-un : ∀ x y (e : El x ≃ El y) → nu x y (un x y e) ≡ e
   nu-un x y e