open import 1Lab.Path.Groupoid open import 1Lab.HLevel open import 1Lab.Path open import 1Lab.Type open is-contr module 1Lab.Equiv where
Equivalencesπ
The big idea of homotopy type theory is that isomorphic types can be identified: the univalence axiom. However, the notion of isomorphism, is, in a sense, not βcoherentβ enough to be used in the definition. For that, we need a coherent definition of equivalence, where βbeing an equivalenceβ is a proposition.
To be more specific, what we need for a notion of equivalence to be βcoherentβ is:
Being an isomorphism implies being an equivalence ()
Being an equivalence implies being an isomorphism (); Taken together with the first point we may summarise: βBeing an equivalence and being an isomorphism are logically equivalent.β
Most importantly, being an equivalence must be a proposition.
The notion we adopt is due to Voevodsky: An equivalence is one that has contractible fibres. Other definitions are possible (e.g.: bi-invertible maps) β but contractible fibres are βprivilegedβ in Cubical Agda because for glueing to work, we need a proof that equivalences have contractible fibres anyway.
private variable ββ ββ : Level A B : Type ββ
A homotopy fibre, fibre or preimage of a
function f
at a point y : B
is the collection
of all elements of A
that f
maps to
y
. Since many choices of name are possible, we settle on
the one that is shortest and most aesthetic: fibre.
fibre : (A β B) β B β Type _ fibre f y = Ξ£ _ Ξ» x β f x β‘ y
A function f
is an equivalence if every one of its
fibres is contractible - that
is, for any element y
in the range, there is exactly one
element in the domain which f
maps to y
. Using
set-theoretic language, f
is an equivalence if the preimage
of every element of the codomain is a singleton.
record is-equiv (f : A β B) : Type (level-of A β level-of B) where no-eta-equality field is-eqv : (y : B) β is-contr (fibre f y) open is-equiv public _β_ : β {ββ ββ} β Type ββ β Type ββ β Type _ _β_ A B = Ξ£ (A β B) is-equiv id-equiv : is-equiv {A = A} (Ξ» x β x) id-equiv .is-eqv y = contr (y , Ξ» i β y) Ξ» { (y' , p) i β p (~ i) , Ξ» j β p (~ i β¨ j) }
For Cubical Agda, the type of equivalences is distinguished, so we have to make a small wrapper to match the interface Agda expects. This is the geometric definition of contractibility, in terms of partial elements and extensibility.
{-# BUILTIN EQUIV _β_ #-} {-# BUILTIN EQUIVFUN fst #-} is-eqv' : β {a b} (A : Type a) (B : Type b) β (w : A β B) (a : B) β (Ο : I) β (p : Partial Ο (fibre (w .fst) a)) β fibre (w .fst) a [ Ο β¦ p ] is-eqv' A B (f , is-equiv) a Ο u0 = inS ( hcomp (β Ο) Ξ» where i (Ο = i0) β c .centre i (Ο = i1) β c .paths (u0 1=1) i i (i = i0) β c .centre) where c = is-equiv .is-eqv a {-# BUILTIN EQUIVPROOF is-eqv' #-}
is-equiv is propositionalπ
A function can be an equivalence in at most one way. This follows from propositions being closed under dependent products, and is-contr being a proposition.
module _ where private is-equiv-is-prop : (f : A β B) β is-prop (is-equiv f) is-equiv-is-prop f x y i .is-eqv p = is-contr-is-prop (x .is-eqv p) (y .is-eqv p) i
Even though the proof above works, we use the direct cubical proof in
this <details>
tag (lifted from the Cubical Agda
library) in the rest of the development for efficiency concerns.
is-equiv-is-prop : (f : A β B) β is-prop (is-equiv f) is-equiv-is-prop f p q i .is-eqv y = let p2 = p .is-eqv y .paths q2 = q .is-eqv y .paths in contr (p2 (q .is-eqv y .centre) i) Ξ» w j β hcomp (β i β¨ β j) Ξ» where k (i = i0) β p2 w j k (i = i1) β q2 w (j β¨ ~ k) k (j = i0) β p2 (q2 w (~ k)) i k (j = i1) β w k (k = i0) β p2 w (i β¨ j)
Isomorphisms from equivalencesπ
For this section, we need a definition of isomorphism. This is the same as ever! An isomorphism is a function that has a two-sided inverse. We first define what it means for a function to invert another on the left and on the right:
is-left-inverse : (B β A) β (A β B) β Type _ is-left-inverse g f = (x : _) β g (f x) β‘ x is-right-inverse : (B β A) β (A β B) β Type _ is-right-inverse g f = (x : _) β f (g x) β‘ x
A proof that a function is an isomorphism consists of a function in the other direction, together with homotopies exhibiting as a left- and right- inverse to .
record is-iso (f : A β B) : Type (level-of A β level-of B) where no-eta-equality constructor iso field inv : B β A rinv : is-right-inverse inv f linv : is-left-inverse inv f inverse : is-iso inv inv inverse = f rinv inverse = linv linv inverse = rinv Iso : β {ββ ββ} β Type ββ β Type ββ β Type _ Iso A B = Ξ£ (A β B) is-iso
Any function that is an equivalence is an isomorphism:
equivβinverse : {f : A β B} β is-equiv f β B β A equivβinverse eqv y = eqv .is-eqv y .centre .fst equivβcounit : β {f : A β B} (eqv : is-equiv f) x β f (equivβinverse eqv x) β‘ x equivβcounit eqv y = eqv .is-eqv y .centre .snd equivβunit : β {f : A β B} (eqv : is-equiv f) x β equivβinverse eqv (f x) β‘ x equivβunit {f = f} eqv x i = eqv .is-eqv (f x) .paths (x , refl) i .fst equivβzig : β {f : A β B} (eqv : is-equiv f) x β ap f (equivβunit eqv x) β‘ equivβcounit eqv (f x) equivβzig {f = f} eqv x i j = hcomp (β i β¨ β j) Ξ» where k (i = i0) β f (equivβunit eqv x j) k (i = i1) β equivβcounit eqv (f x) (j β¨ ~ k) k (j = i0) β equivβcounit eqv (f x) (i β§ ~ k) k (j = i1) β f x k (k = i0) β eqv .is-eqv (f x) .paths (x , refl) j .snd i equivβzag : β {f : A β B} (eqv : is-equiv f) x β ap (equivβinverse eqv) (equivβcounit eqv x) β‘ equivβunit eqv (equivβinverse eqv x) equivβzag {f = f} eqv b = subst (Ξ» b β ap g (Ξ΅ b) β‘ Ξ· (g b)) (Ξ΅ b) (helper (g b)) where g = equivβinverse eqv Ξ΅ = equivβcounit eqv Ξ· = equivβunit eqv helper : β a β ap g (Ξ΅ (f a)) β‘ Ξ· (g (f a)) helper a i j = hcomp (β i β¨ β j) Ξ» where k (i = i0) β g (Ξ΅ (f a) (j β¨ ~ k)) k (i = i1) β Ξ· (Ξ· a (~ k)) j k (j = i0) β g (equivβzig eqv a (~ i) (~ k)) k (j = i1) β Ξ· a (i β§ ~ k) k (k = i0) β Ξ· a (i β§ j) is-equivβis-iso : {f : A β B} β is-equiv f β is-iso f is-iso.inv (is-equivβis-iso eqv) = equivβinverse eqv
We can get an element of x
from the proof that
f
is an equivalence - itβs the point of A
mapped to y
, which we get from centre of contraction for
the fibres of f
over y
.
is-iso.rinv (is-equivβis-iso eqv) y = eqv .is-eqv y .centre .snd
Similarly, that one fibre gives us a proof that the function above is
a right inverse to f
.
is-iso.linv (is-equivβis-iso {f = f} eqv) x i = eqv .is-eqv (f x) .paths (x , refl) i .fst
The proof that the function is a left inverse comes from the
fibres of f
over y
being contractible. Since
we have a fibre - namely, f
maps x
to
f x
by refl - we can get any other we want!
Equivalences from isomorphismsπ
Any isomorphism can be upgraded into an equivalence, in a way that preserves the function , its inverse , and the proof that is a right inverse to . We can not preserve everything, though, as is usual when making something βmore coherentβ. Furthermore, if everything was preserved, is-iso would be a proposition, and this is provably not the case.
The argument presented here is done directly in cubical style, but a less direct proof is also available, by showing that every isomorphism is a half-adjoint equivalence, and that half-adjoint equivalences have contractible fibres.
module _ {f : A β B} (i : is-iso f) where open is-iso i renaming ( inv to g ; rinv to s ; linv to t )
Suppose, then, that and , and weβre given witnesses and (named for section and retraction) that and are inverses. We want to show that, for any , the fibre of over is contractible. It suffices to show that the fibre is propositional, and that it is inhabited.
We begin with showing that the fibre over is propositional, since thatβs the harder of the two arguments. Suppose that we have , , , and as below; Note that and are fibres of over . What we need to show is that we have some and over .
private module _ (y : B) (x0 x1 : A) (p0 : f x0 β‘ y) (p1 : f x1 β‘ y) where
As an intermediate step in proving that , we must show that - without this, we canβt even state that and are identified, since they live in different types! To this end, we will build , parts of which will be required to assemble the overall proof that .
Weβll detail the construction of
;
for
,
the same method is used. We want to construct a line, which we
can do by exhibiting that line as the missing face in a square.
We have equations
(refl),
(the action of g
on p0
), and
by the assumption that
is a right inverse to
.
Diagramatically, these fit together into a square:
The missing line in this square is . Since the inside (the filler) will be useful to us later, we also give it a name: .
Οβ : g y β‘ x0 Οβ i = hcomp (β i) Ξ» where k (i = i0) β g y k (i = i1) β t x0 k k (k = i0) β g (p0 (~ i)) ΞΈβ : Square (ap g (sym p0)) refl (t x0) Οβ ΞΈβ i j = hfill (β i) j Ξ» where k (i = i0) β g y k (i = i1) β t x0 k k (k = i0) β g (p0 (~ i))
Since the construction of is analogous, Iβll simply present the square. We correspondingly name the missing face and the filler .
Οβ : g y β‘ x1 Οβ i = hcomp (β i) Ξ» where j (i = i0) β g y j (i = i1) β t x1 j j (j = i0) β g (p1 (~ i)) ΞΈβ : Square (ap g (sym p1)) refl (t x1) Οβ ΞΈβ i j = hfill (β i) j Ξ» where j (i = i0) β g y j (i = i1) β t x1 j j (j = i0) β g (p1 (~ i))
Joining these paths by their common face, we obtain . This square also has a filler, connecting and over the line .
Ο : x0 β‘ x1 Ο i = hcomp (β i) Ξ» where j (j = i0) β g y j (i = i0) β Οβ j j (i = i1) β Οβ j
This concludes the construction of , and thus, the 2D part of the proof. Now, we want to show that over a path induced by . This is a square with a specific boundary, which can be built by constructing an appropriate open cube, where the missing face is that square. As an intermediate step, we define to be the filler for the square above.
ΞΈ : Square refl Οβ Οβ Ο ΞΈ i j = hfill (β i) j Ξ» where k (i = i1) β Οβ k k (i = i0) β Οβ k k (k = i0) β g y
Observe that we can coherently alter to get below, which expresses that and are identified.
ΞΉ : Square (ap (g β f) Ο) (ap g p0) (ap g p1) refl ΞΉ i j = hcomp (β i β¨ β j) Ξ» where k (k = i0) β ΞΈ i (~ j) k (i = i0) β ΞΈβ (~ j) (~ k) k (i = i1) β ΞΈβ (~ j) (~ k) k (j = i0) β t (Ο i) (~ k) k (j = i1) β g y
This composition can be visualised as the red (front) face
in the diagram below. The back face is
,
i.e.Β (ΞΈ i (~ j))
in the code. Similarly, the
(bottom) face is g y
, the
(top) face is t (Ο i) (~ k)
, and similarly for
(left) and
(right).
The fact that only appears as can be understood as the diagram above being upside-down. Indeed, and in the boundary of (the inner, blue face) are inverted when their types are considered. Weβre in the home stretch: Using our assumption , we can cancel all of the s in the diagram above to get what we wanted: .
sq1 : Square (ap f Ο) p0 p1 refl sq1 i j = hcomp (β i β¨ β j) Ξ» where k (i = i0) β s (p0 j) k k (i = i1) β s (p1 j) k k (j = i0) β s (f (Ο i)) k k (j = i1) β s y k k (k = i0) β f (ΞΉ i j)
The composition above can be visualised as the front (red) face in the cubical diagram below. Once more, left is , right is , up is , and down is .
Putting all of this together, we get that . Since there were no assumptions on any of the variables under consideration, this indeed says that the fibre over is a proposition for any choice of .
is-isoβfibre-is-prop : (x0 , p0) β‘ (x1 , p1) is-isoβfibre-is-prop i .fst = Ο i is-isoβfibre-is-prop i .snd = sq1 i
Since the fibre over is inhabited by , we get that any isomorphism has contractible fibres:
is-isoβis-equiv : is-equiv f is-isoβis-equiv .is-eqv y .centre .fst = g y is-isoβis-equiv .is-eqv y .centre .snd = s y is-isoβis-equiv .is-eqv y .paths z = is-isoβfibre-is-prop y (g y) (fst z) (s y) (snd z)
Applying this to the Iso and _β_ pairs, we can turn any isomorphism into a coherent equivalence.
IsoβEquiv : β {ββ ββ} {A : Type ββ} {B : Type ββ} β Iso A B β A β B IsoβEquiv (f , is-iso) = f , is-isoβis-equiv is-iso
A helpful lemma: Any function between contractible types is an equivalence:
is-contrβis-equiv : β {ββ ββ} {A : Type ββ} {B : Type ββ} β is-contr A β is-contr B β {f : A β B} β is-equiv f is-contrβis-equiv cA cB = is-isoβis-equiv f-is-iso where f-is-iso : is-iso _ is-iso.inv f-is-iso _ = cA .centre is-iso.rinv f-is-iso _ = is-contrβis-prop cB _ _ is-iso.linv f-is-iso _ = is-contrβis-prop cA _ _ is-contrββ : β {ββ ββ} {A : Type ββ} {B : Type ββ} β is-contr A β is-contr B β A β B is-contrββ cA cB = (Ξ» _ β cB .centre) , is-isoβis-equiv f-is-iso where f-is-iso : is-iso _ is-iso.inv f-is-iso _ = cA .centre is-iso.rinv f-is-iso _ = is-contrβis-prop cB _ _ is-iso.linv f-is-iso _ = is-contrβis-prop cA _ _
Equivalence Reasoningπ
To make composing equivalences more intuitive, we implement operators to do equivalence reasoning in the same style as equational reasoning.
_βe_ : β {β ββ ββ} {A : Type β} {B : Type ββ} {C : Type ββ} β A β B β B β C β A β C _eβ»ΒΉ : β {β ββ} {A : Type β} {B : Type ββ} β A β B β B β A _eβ»ΒΉ eqv = IsoβEquiv ( equivβinverse (eqv .snd) , record { inv = eqv .fst ; rinv = equivβunit (eqv .snd) ; linv = equivβcounit (eqv .snd) })
The proofs that equivalences are closed under composition assemble nicely into transitivity operators resembling equational reasoning:
_ββ¨_β©_ : β {β ββ ββ} (A : Type β) {B : Type ββ} {C : Type ββ} β A β B β B β C β A β C A ββ¨ f β©β g = f βe g _ββ¨β©_ : β {β ββ} (A : Type β) {B : Type ββ} β A β B β A β B x ββ¨β© xβ‘y = xβ‘y _ββ : β {β} (A : Type β) β A β A x ββ = _ , id-equiv infixr 30 _βe_ infixr 2 _ββ¨β©_ _ββ¨_β©_ infix 3 _ββ
Propositional Extensionalityπ
The following observation is not very complex, but it is incredibly useful: Equivalence of propositions is the same as biimplication.
prop-ext : β {β β'} {P : Type β} {Q : Type β'} β is-prop P β is-prop Q β (P β Q) β (Q β P) β P β Q prop-ext pprop qprop pβq qβp .fst = pβq prop-ext pprop qprop pβq qβp .snd .is-eqv y .centre = qβp y , qprop _ _ prop-ext pprop qprop pβq qβp .snd .is-eqv y .paths (p' , path) = Ξ£-path (pprop _ _) (is-propβis-set qprop _ _ _ _)