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

# Equivs from Pathsπ

In (Cohen
et al. 2016), a direct *cubical* construction of an
equivalence `A β B`

from a path `A β‘ B`

is
presented. 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

## References

- Cohen, Cyril, Thierry Coquand, Simon Huber, and Anders MΓΆrtberg. 2016. βCubical Type Theory: A Constructive Interpretation of the Univalence Axiom.β https://arxiv.org/abs/1611.02108.