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

* `transpEquiv`: Transporting from an extent to `i1` is an equivalence

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

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

* Direct proof of `univalence` avoiding induction on paths & equivalences

The computation rules `uaβ` and `uaη` show that `pathToEquiv` and `ua`
define both directions of an isomorphism.  This sidesteps the proof in
module `Univalence`, which is done by induction on paths (`J`) and
equivalences (`EquivJ`).

Cubical/Foundations/Equiv/Base.agda

@@ -29,3 +29,37 @@ idEquiv A .snd = idIsEquiv A
 -- the definition using Π-type
 isEquiv' : ∀ {ℓ}{ℓ'}{A : Type ℓ}{B : Type ℓ'} → (A → B) → Type (ℓ-max ℓ ℓ')
 isEquiv' {B = B} f = (y : B) → isContr (fiber f y)
+
+-- Transport along a line of types A, constant on some extent φ, is an equivalence.
+isEquivTransp : ∀ {ℓ : I → Level} (A : (i : I) → Type (ℓ i)) → ∀ (φ : I) → isEquiv (transp (λ j → A (φ ∨ j)) φ)
+isEquivTransp A φ = u₁ where
+  -- NB: The transport in question is the `coei→1` or `squeeze` operation mentioned
+  -- at `Cubical.Foundations.CartesianKanOps` and
+  -- https://1lab.dev/1Lab.Path.html#coei%E2%86%921
+  coei→1 : A φ → A i1
+  coei→1 = transp (λ j → A (φ ∨ j)) φ
+
+  -- A line of types, interpolating between propositions:
+  -- (k = i0): the identity function is an equivalence
+  -- (k = i1): transport along A is an equivalence
+  γ : (k : I) → Type _
+  γ k = isEquiv (transp (λ j → A (φ ∨ (j ∧ k))) (φ ∨ ~ k))
+
+  _ : γ i0 ≡ isEquiv (idfun (A φ))
+  _ = refl
+
+  _ : γ i1 ≡ isEquiv coei→1
+  _ = refl
+
+  -- We have proof that the identity function *is* an equivalence,
+  u₀ : γ i0
+  u₀ = idIsEquiv (A φ)
+
+  -- and by transporting that evidence along γ, we prove that
+  -- transporting along A is an equivalence, too.
+  u₁ : γ i1
+  u₁ = transp γ φ u₀
+
+transpEquiv : ∀ {ℓ : I → Level} (A : (i : I) → Type (ℓ i)) → ∀ φ → A φ ≃ A i1
+transpEquiv A φ .fst = transp (λ j → A (φ ∨ j)) φ
+transpEquiv A φ .snd = isEquivTransp A φ

Cubical/Foundations/Everything.agda

@@ -6,6 +6,7 @@ open import Cubical.Foundations.Prelude public
 
 open import Cubical.Foundations.Function public
 open import Cubical.Foundations.Equiv public
+  hiding (transpEquiv) -- Hide to avoid clash with Transport.transpEquiv
 open import Cubical.Foundations.Equiv.Properties public
 open import Cubical.Foundations.Equiv.Fiberwise
 open import Cubical.Foundations.Equiv.PathSplit public

Cubical/Foundations/Transport.agda

@@ -8,7 +8,7 @@
 module Cubical.Foundations.Transport where
 
 open import Cubical.Foundations.Prelude
-open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Equiv as Equiv hiding (transpEquiv)
 open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.Univalence
 open import Cubical.Foundations.GroupoidLaws
@@ -78,17 +78,12 @@ liftEquiv : ∀ {ℓ ℓ'} {A B : Type ℓ} (P : Type ℓ → Type ℓ') (e : A
 liftEquiv P e = substEquiv P (ua e)
 
 transpEquiv : ∀ {ℓ} {A B : Type ℓ} (p : A ≡ B) → ∀ i → p i ≃ B
-transpEquiv P i .fst = transp (λ j → P (i ∨ j)) i
-transpEquiv P i .snd
-  = transp (λ k → isEquiv (transp (λ j → P (i ∨ (j ∧ k))) (i ∨ ~ k)))
-      i (idIsEquiv (P i))
+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

@@ -170,6 +170,60 @@ EquivJ : {A B : Type ℓ} (P : (A : Type ℓ) → (e : A ≃ B) → Type ℓ')
        → (r : P B (idEquiv B)) → (e : A ≃ B) → P A e
 EquivJ P r e = subst (λ x → P (x .fst) (x .snd)) (contrSinglEquiv e) r
 
+-- Transport along a path is an equivalence.
+-- The proof is a special case of isEquivTransp where the line of types is
+-- given by p, and the extend φ -- where the transport is constant -- is i0.
+isEquivTransport : {A B : Type ℓ} (p : A ≡ B) → isEquiv (transport p)
+isEquivTransport p = isEquivTransp A φ where
+  A : I → Type _
+  A i = p i
+
+  φ : I
+  φ = i0
+
+pathToEquiv : {A B : Type ℓ} → A ≡ B → A ≃ B
+pathToEquiv p .fst = transport p
+pathToEquiv p .snd = isEquivTransport p
+
+pathToEquivRefl : {A : Type ℓ} → pathToEquiv refl ≡ idEquiv A
+pathToEquivRefl {A = A} = equivEq (λ i x → transp (λ _ → A) i x)
+
+-- The computation rule for ua. Because of "ghcomp" it is now very
+-- simple compared to cubicaltt:
+-- https://github.com/mortberg/cubicaltt/blob/master/examples/univalence.ctt#L202
+uaβ : {A B : Type ℓ} (e : A ≃ B) (x : A) → transport (ua e) x ≡ equivFun e x
+uaβ e x = transportRefl (equivFun e x)
+
+uaη : ∀ {A B : Type ℓ} → (P : A ≡ B) → ua (pathToEquiv P) ≡ P
+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
+
+pathToEquiv-ua : {A B : Type ℓ} (e : A ≃ B) → pathToEquiv (ua e) ≡ e
+pathToEquiv-ua e = equivEq (funExt (uaβ e))
+
+ua-pathToEquiv : {A B : Type ℓ} (p : A ≡ B) → ua (pathToEquiv p) ≡ p
+ua-pathToEquiv = uaη
+
+-- Univalence
+univalenceIso : {A B : Type ℓ} → Iso (A ≡ B) (A ≃ B)
+univalenceIso .Iso.fun = pathToEquiv
+univalenceIso .Iso.inv = ua
+univalenceIso .Iso.rightInv = pathToEquiv-ua
+univalenceIso .Iso.leftInv = ua-pathToEquiv
+
+isEquivPathToEquiv : {A B : Type ℓ} → isEquiv (pathToEquiv {A = A} {B = B})
+isEquivPathToEquiv = isoToIsEquiv univalenceIso
+
+univalence : {A B : Type ℓ} → (A ≡ B) ≃ (A ≃ B)
+univalence .fst = pathToEquiv
+univalence .snd = isEquivPathToEquiv
+
 -- Assuming that we have an inverse to ua we can easily prove univalence
 module Univalence (au : ∀ {ℓ} {A B : Type ℓ} → A ≡ B → A ≃ B)
                   (aurefl : ∀ {ℓ} {A : Type ℓ} → au refl ≡ idEquiv A) where
@@ -191,30 +245,6 @@ module Univalence (au : ∀ {ℓ} {A B : Type ℓ} → A ≡ B → A ≃ B)
   thm : ∀ {ℓ} {A B : Type ℓ} → isEquiv au
   thm {A = A} {B = B} = isoToIsEquiv {B = A ≃ B} isoThm
 
-isEquivTransport : {A B : Type ℓ} (p : A ≡ B) → isEquiv (transport p)
-isEquivTransport p =
-  transport (λ i → isEquiv (transp (λ j → p (i ∧ j)) (~ i))) (idIsEquiv _)
-
-pathToEquiv : {A B : Type ℓ} → A ≡ B → A ≃ B
-pathToEquiv p .fst = transport p
-pathToEquiv p .snd = isEquivTransport p
-
-pathToEquivRefl : {A : Type ℓ} → pathToEquiv refl ≡ idEquiv A
-pathToEquivRefl {A = A} = equivEq (λ i x → transp (λ _ → A) i x)
-
-pathToEquiv-ua : {A B : Type ℓ} (e : A ≃ B) → pathToEquiv (ua e) ≡ e
-pathToEquiv-ua = Univalence.au-ua pathToEquiv pathToEquivRefl
-
-ua-pathToEquiv : {A B : Type ℓ} (p : A ≡ B) → ua (pathToEquiv p) ≡ p
-ua-pathToEquiv = Univalence.ua-au pathToEquiv pathToEquivRefl
-
--- Univalence
-univalenceIso : {A B : Type ℓ} → Iso (A ≡ B) (A ≃ B)
-univalenceIso = Univalence.isoThm pathToEquiv pathToEquivRefl
-
-univalence : {A B : Type ℓ} → (A ≡ B) ≃ (A ≃ B)
-univalence = ( pathToEquiv , Univalence.thm pathToEquiv pathToEquivRefl  )
-
 -- The original map from UniMath/Foundations
 eqweqmap : {A B : Type ℓ} → A ≡ B → A ≃ B
 eqweqmap {A = A} e = J (λ X _ → A ≃ X) (idEquiv A) e
@@ -231,15 +261,6 @@ univalenceUAH = ( _ , univalenceStatement )
 univalencePath : {A B : Type ℓ} → (A ≡ B) ≡ Lift (A ≃ B)
 univalencePath = ua (compEquiv univalence LiftEquiv)
 
--- The computation rule for ua. Because of "ghcomp" it is now very
--- simple compared to cubicaltt:
--- https://github.com/mortberg/cubicaltt/blob/master/examples/univalence.ctt#L202
-uaβ : {A B : Type ℓ} (e : A ≃ B) (x : A) → transport (ua e) x ≡ equivFun e x
-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)
-
 -- 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 ℓ'}
   {f₀ : A₀ → B i0} {f₁ : A₁ → B i1}

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