open import 1Lab.Path.Cartesian
open import 1Lab.Path.Reasoning
open import 1Lab.HLevel
open import 1Lab.Equiv
open import 1Lab.Path
open import 1Lab.Type

module 1Lab.Equiv.FromPath {ℓ} (P : (i : I) → Type ℓ) where

Transport is an equivalence🔗

Showing that transport is an equivalence could be done essentially by path induction, since the transp function associated to a line of types $P$ is identical to the identity function over $P\text{.}$ This is a very straightforward argument:

private
  bad-transport-is-equiv : is-equiv (transp P i0)
  bad-transport-is-equiv = transp (λ i → is-equiv (coe0→i P i)) i0 id-equiv

While is-equiv is a proposition— and thus the particular proof does not matter propositionally— Agda is still a programming language, the data of an equivalence includes the inverse function, and the inverse we obtain from this construction is not simply transport along the inverse of $P\text{:}$ it has an extra reflexive transport along $P(i1)\text{,}$ which does not compute away when $P(i1)$ is neutral.

  _ : equiv→inverse bad-transport-is-equiv
    ≡ transport refl ∘ transp (λ i → P (~ i)) i0
  _ = refl

We can instead construct the proof that transp along $P$ is an equivalence directly. We start by naming all the relevant endpoints:

  A B : Type ℓ
  A = P i0
  B = P i1

  f : A → B
  f x = coe0→1 P x

  g : B → A
  g y = coe1→0 P y

We can then directly prove that $f$ and $g$ are inverses, fixing the computation of the inverse. Since having a two-sided inverse is enough to imply that a function is an equivalence, we would be done; however, that general theorem relies on replacing the unit $\eta :gf\sim \mathrm{id}$ by something which satisfies the triangle identities, whereas in this case we can show by a direct cubical argument that our $\eta$ already satisfies the triangle identities.

  ε : (y : B) → f (g y) ≡ y
  ε y i = coe P i i1 (coe P i1 i y)

  η : (x : A) → g (f x) ≡ x
  η x i = coe P (~ i) i0 (coe P i0 (~ i) x)

It will suffice to give a square ${\zeta }_1$ with the boundary below, since in that case (assuming we have $y:B$ and the data $x:A\text{,}$ $\alpha :fx\equiv y$ of a fibre $f^y\text{)}$ we can construct $\beta :gy\equiv x$ as the composite $$gy\stackrel{\mathrm{ap}g\alpha }{\to }g(fx)\stackrel{\eta x}{\to }x\text{,}$$ and glue ${\zeta }_1$ along ∙-filler' to give us the necessary square identifying $\mathrm{ap}f\beta \text{,}$ $\epsilon$ and $\alpha \text{.}$

  module _ (y : B) (x : A) (α : f x ≡ y) where
    β : g y ≡ x
    β = ap g (sym α) ∙ η x

    ζ₁ : Square (ap f (η x)) (ε (f x)) refl refl
    ζ : Square (ap f β) (ε y) α refl
    ζ i j = hcomp (∂ i ∨ ∂ j) λ where
      k (k = i0) → ζ₁ i j

      k (i = i0) → ε (α k) j
      k (i = i1) → α (k ∧ j)
      k (j = i0) → f (∙-filler' (ap g (sym α)) (η x) k i)
      k (j = i1) → α k

    ζ₁ i j = comp P (∂ i ∨ ∂ j) λ where
      k (k = i0) → η x (i ∨ ~ j)

      k (i = i0) → coe P j k (coe-path P (λ j → coe0→i P j x) k j i)
      k (j = i0) → coe P j k (coe-path P (λ j → coe0→i P j x) k j i)

      k (i = i1) → coe P i0 k x
      k (j = i1) → hcomp (∂ i ∨ ∂ k) λ where
        j (j = i0) → coe-path P (λ j → coe P k j (coe0→i P k x)) i1 k i

        j (i = i1) → coei→i P k (coe0→i P k x) j
        j (i = i0) → coe P i1 k (coe P k i1 (coe0→i P k x))

        j (k = i0) → η x i
        j (k = i1) → f x

We can now simply package the components up.

transp-is-equiv : is-equiv (transp P i0)
transp-is-equiv .is-eqv y .centre = record { snd = ε y }
transp-is-equiv .is-eqv y .paths (x , α) i = record
  { snd = ζ y x α i }

line→equiv : A ≃ B
line→equiv .fst = transp P i0
line→equiv .snd = transp-is-equiv

At the level of points and paths, this construction computes very nicely, with the only hitch being a stray reflexivity path added to the unit. The witness for the triangle identity is our ζ, and so made up of quite a few hcomps, but still much better (by virtue of the unit and counit being simpler) than is possible by simply transporting the proof that the identity is an equivalence.

_ : equiv→inverse transp-is-equiv ≡ g
_ = refl

_ : equiv→counit transp-is-equiv ≡ transport⁻transport (λ i → P (~ i))
_ = refl

_ : ∀ {x}
  → equiv→unit transp-is-equiv x
  ≡ refl ∙ transport⁻transport (λ i → P i) x
_ = refl