From ad4c842e98303c966085eab8632f1b435f6aea60 Mon Sep 17 00:00:00 2001
From: phijor <phijor@users.noreply.github.com>
Date: Fri, 13 Oct 2023 10:24:55 +0200
Subject: [PATCH] Direct proof of `uaOver` from Glue types (#1066)

---
 Cubical/Foundations/Univalence/Dependent.agda | 74 ++++++++++++++++---
 1 file changed, 64 insertions(+), 10 deletions(-)

diff --git a/Cubical/Foundations/Univalence/Dependent.agda b/Cubical/Foundations/Univalence/Dependent.agda
index 396f7d078b..c9a39e61cb 100644
--- a/Cubical/Foundations/Univalence/Dependent.agda
+++ b/Cubical/Foundations/Univalence/Dependent.agda
@@ -21,20 +21,74 @@ private
 
 
 -- Dependent Univalence
-
--- A quicker proof provided by @ecavallo: uaOver e F equiv = ua→ (λ a → ua (_ , equiv a))
--- Unfortunately it gives a larger term overall.
-uaOver :
+--
+-- Given families `P` and `Q` over base types `A` and `B`
+-- respectively, and given
+--  * an equivalence of base types `e : A ≃ B`,
+--  * and and a pointwise equivalence of the families,
+-- construct a dependent path over `ua e` between the families.
+module _
   {A B : Type ℓ} {P : A → Type ℓ'} {Q : B → Type ℓ'}
   (e : A ≃ B) (F : mapOver (e .fst) P Q)
   (equiv : isEquivOver {P = P} {Q = Q} F)
-  → PathP (λ i → ua e i → Type ℓ') P Q
-uaOver {A = A} {P = P} {Q} e F equiv i x =
-  hcomp (λ j → λ
-    { (i = i0) → ua (_ , equiv x) (~ j)
-    ; (i = i1) → Q x })
-  (Q (unglue (i ∨ ~ i) x))
+  where
+  private
+    -- Bundle `F` and `equiv` into a pointwise equivalence of `P` and `Q`:
+    Γ : (a : A) → P a ≃ Q (equivFun e a)
+    Γ a = F a , equiv a
+
+    -- A quick proof provided by @ecavallo.
+    -- Unfortunately it gives a larger term overall.
+    _ : PathP (λ i → ua e i → Type ℓ') P Q
+    _ = ua→ (λ a → ua (Γ a))
+
+  uaOver : PathP (λ i → ua e i → Type ℓ') P Q
+  uaOver i x = Glue Base {φ} equiv-boundary where
+    -- Like `ua`, `uaOver` is obtained from a line of
+    -- Glue-types, except that they are glued
+    -- over a line dependent on `ua e : A ≡ B`.
+
+    -- `x` is a point along the path `A ≡ B` obtained
+    -- from univalence, i.e. glueing over `B`:
+    --
+    --  A = = (ua e) = = B
+    --  |                |
+    -- (e)          (idEquiv B)
+    --  |                |
+    --  v                v
+    --  B =====(B)====== B
+    _ : Glue B {φ = i ∨ ~ i} (λ { (i = i0) → A , e ; (i = i1) → B , idEquiv B })
+    _ = x
+
+    -- We can therefore `unglue` it to obtain a term in the base line of `ua e`,
+    -- i.e. term of type `B`:
+    φ = i ∨ ~ i
+    b : B
+    b = unglue φ x
+
+    -- This gives us a line `(i : I) ⊢ Base` in the universe of types,
+    -- along which we can glue the equivalences `Γ x` and `idEquiv (Q x)`:
+    --
+    -- P (e x) = = = = = = Q x
+    --    |                |
+    --  (Γ x)        (idEquiv (Q x))
+    --    |                |
+    --    v                v
+    --   Q x ===(Base)=== Q x
+    Base : Type ℓ'
+    Base = Q b
+
+    equiv-boundary : Partial φ (Σ[ T ∈ Type ℓ' ] T ≃ Base)
+    equiv-boundary (i = i0) = P x , Γ x
+    equiv-boundary (i = i1) = Q x , idEquiv (Q x)
+
+    -- Note that above `(i = i0) ⊢ x : A` and `(i = i1) ⊢ x : B`,
+    -- thus `P x` and `Q x` are well-typed.
+    _ : Partial i B
+    _ = λ { (i = i1) → x }
 
+    _ : Partial (~ i) A
+    _ = λ { (i = i0) → x }
 
 -- Dependent `isoToPath`