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

# Equivs from Pathsπ

In Cubical Type Theory: a
constructive interpretation of the univalence axiom, Cohen et. al.
give a direct *cubical* construction of an equivalence
`A β B`

from a path `A β‘ B`

. This is in contrast
with the *indirect* definition, transporting the identity
equivalence along the path:

private badPathToEquiv : P i0 β P i1 badPathToEquiv = transport (Ξ» i β P i0 β P i) (id , id-equiv)

While is-equiv is a proposition β and thus the
particular proof does not matter propositionally β Agda is still a
programming language, so we still need to *evaluate* the proof.
Cohen et. al.βs construction gives a much shorter normal form for lineβequiv.

private ~P : (i : I) β Type β ~P = Ξ» i β P (~ i) A B : Type β A = P i0 B = P i1

The construction begins by giving the endpoints of P β and the inverse of P β better names. We do the same for transports along P and ~P:

f : A β B f x = coe0β1 P x g : B β A g y = coe1β0 P y

Since f and g are
defined by coercion
along a path, we can define *fillers* u and
v connecting f (resp
g) to the identity function, over P:

u : PathP (Ξ» i β A β P i) id f u i x = coe0βi P i x v : PathP (Ξ» i β B β P i) g id v i y = coe1βi P i y

To prove that f is an
equivalence, by definition, it must have *contractible fibres*. It suffices to show that the
fibre over y is inhabited, and that the
fibre over y is a proposition.

To prove that the fibre over `y`

is inhabited, we
take `g y`

to be the preimage, and prove that there is a path
`f (g y) β‘ y`

, as we are required to do. For this, we use the
βlidβ (the dotted face) of the square below (this is the comp term):

hasFib : (y : B) β fibre f y hasFib y .fst = g y hasFib y .snd i = comp P (β i) Ξ» where j (i = i1) β v j y j (i = i0) β u j (g y) j (j = i0) β g y

To prove that the fibre over y is propositional, there is significantly more work involved. Especially since all of the paths involved are dependent, and thus none of the path operations (especially sym!) apply. We begin by stating the types of what weβre going to construct:

fibProp : (y : B) β is-prop (fibre f y) fibProp y (xβ , Ξ²β) (xβ , Ξ²β) k = Ο k , Ξ» j β Ξ΄ k (~ j) where Ο : xβ β‘ xβ Ξ΄ : Square refl (sym Ξ²β) (sym Ξ²β) (ap f Ο)

While Ο is a line, Ξ΄ is a
*square*. Namely, by looking at its type, we see that its
boundary is the square below. Observe that it is essentially a path
`Ξ²β β‘ Ξ²β`

, lying over `Ο`

, which is exactly what
we need to equate the fibres:

As an intermediate step in the construction of Ξ΄, we construct ΞΈ. However, that is also hard to do directly, so we have four (really, two) more intermediate steps: Οβ/ΞΈβ and Οβ/ΞΈβ.

The line Οβ is the dashed line in the composition below, and ΞΈβ is the square itself. The type of ΞΈβ is hard to look at, so focus on the diagram: It connects Ξ²β and Οβ, in the vertical direction.

square : β (x : A) (Ξ² : f x β‘ y) j i β PartialP (β j β¨ ~ i) (Ξ» _ β P (~ i)) square x Ξ² j i (j = i0) = v (~ i) y square x Ξ² j i (j = i1) = u (~ i) x square x Ξ² j i (i = i0) = Ξ² (~ j) Οβ : g y β‘ xβ Οβ j = comp (Ξ» i β P (~ i)) (β j) (square xβ Ξ²β j) ΞΈβ : SquareP (Ξ» i j β P (~ j)) (sym Ξ²β) (Ξ» i β v (~ i) y) (Ξ» i β u (~ i) xβ) Οβ ΞΈβ j i = fill ~P (β j) i (square xβ Ξ²β j)

Analogously, we have Οβ and ΞΈβ connecting Ξ²β and that, as the dashed line and filler of the square below:

Οβ : g y β‘ xβ Οβ j = comp (Ξ» i β P (~ i)) (β j) (square xβ Ξ²β j) ΞΈβ : SquareP (Ξ» i j β P (~ j)) (sym Ξ²β) (Ξ» i β v (~ i) y) (Ξ» i β u (~ i) xβ) Οβ ΞΈβ j i = fill ~P (β j) i (square xβ Ξ²β j)

Now, we are almost done. Like a magic trick, the paths
`Οβ`

and Οβ we
constructed above to aid in proving Ξ΄
assemble to give a complete proof of Ο, as
the dashed line in the square below:

Ο k = hcomp (β k) Ξ» where j (k = i0) β Οβ j j (k = i1) β Οβ j j (j = i0) β g y ΞΈ : Square refl Οβ Οβ Ο ΞΈ k i = hfill (β k) i Ξ» where j (k = i0) β Οβ j j (k = i1) β Οβ j j (j = i0) β g y

We also have ΞΈ,
which is the filler of the above square - i.e., it is a path connecting
`Οβ`

and Οβ. Now
we can finally assemble Ξ΄.
Since we are constructing a square, we are filling a *cube*,
i.e.Β a path of paths of paths! The βfullβ face of this cube is given by
ΞΈ, which indicates the boundaries of the
other faces. The full cube is right after the definition:

Ξ΄ k j = comp P (β j β¨ β k) Ξ» where i (i = i0) β ΞΈ k j i (j = i0) β v i y i (j = i1) β u i (Ο k) i (k = i0) β ΞΈβ j (~ i) i (k = i1) β ΞΈβ j (~ i)

The idea behind the diagram is to piece together the three squares we
have constructed, ΞΈ,
ΞΈβ and ΞΈβ,
with the intent of getting a composite `Ξ²β β‘ Ξ²β`

. The
purpleish square behind is ΞΈ; The
brownish square in front is Ξ΄.
Finally, putting together the proof of
inhabitation and the proof of
propositionality, we get the desired: f is an
equivalence.

lineβis-equiv : is-equiv f lineβis-equiv .is-eqv y .centre = hasFib y lineβis-equiv .is-eqv y .paths = fibProp y _ lineβequiv : A β B lineβequiv .fst = f lineβequiv .snd = lineβis-equiv