transpEquiv: Transporting from an extent to i1 is an equivalence

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,10 +78,8 @@ 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

Cubical/Foundations/Univalence.agda

@@ -191,9 +191,11 @@ 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
 
+-- 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 extent φ -- where the transport is constant -- is i0.
 isEquivTransport : {A B : Type ℓ} (p : A ≡ B) → isEquiv (transport p)
-isEquivTransport p =
-  transport (λ i → isEquiv (transp (λ j → p (i ∧ j)) (~ i))) (idIsEquiv _)
+isEquivTransport p = isEquivTransp (λ i → p i) i0
 
 pathToEquiv : {A B : Type ℓ} → A ≡ B → A ≃ B
 pathToEquiv p .fst = transport p