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
: P i0 ≃ P i1
badPathToEquiv = transport (λ i → P i0 ≃ P i) (id , id-equiv) badPathToEquiv
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
: (i : I) → Type ℓ
~P = λ i → P (~ i)
~P
: Type ℓ
A B = P i0
A = P i1 B
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
:
: A → B
f = coe0→1 P x
f x
: B → A
g = coe1→0 P y g 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
:
: PathP (λ i → A → P i) id f
u = coe0→i P i x
u i x
: PathP (λ i → B → P i) g id
v = coe1→i P i y v 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):
: (y : B) → fibre f y
hasFib .fst = g y
hasFib y .snd i = comp P (∂ i) λ where
hasFib y (i = i1) → v j y
j (i = i0) → u j (g y)
j (j = i0) → g y j
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:
: (y : B) → is-prop (fibre f y)
fibProp (x₀ , β₀) (x₁ , β₁) k = ω k , λ j → δ k (~ j) where
fibProp y : 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.
: ∀ (x : A) (β : f x ≡ y) j i → PartialP (∂ j ∨ ~ i) (λ _ → P (~ i))
square (j = i0) = v (~ i) y
square x β j i (j = i1) = u (~ i) x
square x β j i (i = i0) = β (~ j)
square x β j i
: g y ≡ x₀
ω₀ = comp (λ i → P (~ i)) (∂ j) (square x₀ β₀ j)
ω₀ j
: SquareP (λ i j → P (~ j)) (sym β₀) (λ i → v (~ i) y) (λ i → u (~ i) x₀) ω₀
θ₀ = fill ~P (∂ j) i (square x₀ β₀ j) θ₀ j i
Analogously, we have ω₁
and
θ₁
connecting β₁
and that, as the dashed line and
filler of the square below:
: g y ≡ x₁
ω₁ = comp (λ i → P (~ i)) (∂ j) (square x₁ β₁ j)
ω₁ j
: SquareP (λ i j → P (~ j)) (sym β₁) (λ i → v (~ i) y) (λ i → u (~ i) x₁) ω₁
θ₁ = fill ~P (∂ j) i (square x₁ β₁ j) θ₁ j i
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:
= hcomp (∂ k) λ where
ω k (k = i0) → ω₀ j
j (k = i1) → ω₁ j
j (j = i0) → g y
j
: Square refl ω₀ ω₁ ω
θ = hfill (∂ k) i λ where
θ k i (k = i0) → ω₀ j
j (k = i1) → ω₁ j
j (j = i0) → g y j
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:
= comp P (∂ j ∨ ∂ k) λ where
δ k j (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) 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.
: is-equiv f
line→is-equiv .is-eqv y .centre = hasFib y
line→is-equiv .is-eqv y .paths = fibProp y _
line→is-equiv
: A ≃ B
line→equiv .fst = f
line→equiv .snd = line→is-equiv line→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.