module 1Lab.Equiv where

# Equivalencesπ

The key principle that distinguishes HoTT from other type theories is
the univalence principle:
*isomorphic* types can be *identified*. In cubical type
theory, this turns out to be a theorem; but from a neutral point of
view, it should be read as the *definition* of the identity types
of universes β which are
otherwise left unspecified by MLTT. However, the notion of isomorphism
is not well-behaved when higher dimensional types are involved, so we
canβt actually use it to formulate univalence.

The key issue is that any identity
system is equipped with a path induction principle,
which, if extended to the type of isomorphisms, would let us conclude
that *being an isomorphism* is a proposition: but this is provably not the case. The
result of formulating univalence using isomorphisms is sometimes called
isovalence
β that page has a formalisation of its failure.

We must therefore define a property of functions which refines being
an isomorphism but *is* an isomorphism: functions satisfying this
property will be called equivalences. More specifically, weβre looking
for a family
$is-equiv(f)$
which

is implied by $is-iso(f),$ so that any function with a two-sided inverse is an equivalence. Apart from preserving the connection with the intuitive motivation behind univalence, exhibiting a two-sided inverse to a given map is simply

*easier*than proving that itβs a coherent equivalence.implies $is-iso(f),$ so that knowing that a map is an equivalence also lets you extract a two-sided inverse. Most notions of equivalence will also tell you additional properties about the connection between $f$ and its inverse map.

and finally, is an actual proposition.

Put concisely, weβre looking to define a propositional
truncation of
$is-iso(f)$
β one which allows us to conveniently project out the underlying data.
Since propositional truncations are unique, this means that all type
families satisfying the three bullet points above are
*themselves* equivalent; so any choice made must be
meta-mathematical, driven by concerns like ease of use, and efficiency
of the formalisation.

Here in the 1Lab, we formalise three acceptable notions of equivalence:

- biinvertible
maps, which store
*two*inverses to the given function; - half-adjoint
equivalences, which, in addition to the inverse map and the
witnesses of invertibility, have an extra
*coherence datum*; and - the notion defined in this file,
**contractible maps**, which repackage the notion of equivalence in a homotopically-inspired way.

## Isomorphismsπ

Before we set about defining and working with equivalences, weβll warm up by defining, and proving basic things about, isomorphisms. First, we define what it means for functions to be inverses of eachother, on both the left and 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 function
$g$
which is both a left- and right inverse to
$f$
is called a **two-sided inverse** (to
$f).$
To say that a function is an isomorphism is to equip it with a two-sided
inverse.

Despite the name `is-iso`

, a two-sided inverse is
actual *data* we can equip a function with: itβs not, in general,
valued in propositions.

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

Itβs immediate from the symmetry of the definition that if $g$ is a two-sided inverse to $f,$ then $f$ also inverts $g:$ an isomorphismβs inverse is again an isomorphism.

inverse : is-iso inv inverse .inv = f inverse .rinv = linv inverse .linv = rinv

Iso : β {ββ ββ} β Type ββ β Type ββ β Type _ Iso A B = Ξ£ (A β B) is-iso module _ where open is-iso

Second, a composite of isomorphisms is an isomorphism: if we can undo
$f$
and
$g$
individually, we can undo them sequentially, by first undoing
$g,$
then undoing
$f.$
The observation that the inverse is in the opposite order is sometimes
humorously referred to as the *socks-and-shoes principle*.

β-is-iso : {f : B β C} {g : A β B} β is-iso f β is-iso g β is-iso (f β g) β-is-iso f-im g-im .inv x = g-im .inv (f-im .inv x) β-is-iso {f = f} {g = g} f-im g-im .rinv x = f (g (g-im .inv (f-im .inv x))) β‘β¨ ap f (g-im .rinv _) β©β‘ f (f-im .inv x) β‘β¨ f-im .rinv _ β©β‘ x β β-is-iso {g = g} f-im g-im .linv x = ap (g-im .inv) (f-im .linv (g x)) β g-im .linv x

Finally, the identity map is its own two-sided inverse, so it is an
isomorphism. Keep in mind that, again, there are multiple ways for a map
to *be an isomorphism*. It would be more correct to say that
there is a parametric way to make the identity map into an isomorphism:
if we know more about the specific type, there might be other ways.

private id-iso : is-iso {A = A} id id-iso .inv = id id-iso .rinv x = refl id-iso .linv x = refl

## Equivalences properπ

With that out of the way, we can actually define the property of
functions that weβll adopt under the name *equivalence*. The
notion of contractible maps is due to Voevodsky, and it very elegantly
packages the data of an inverse in a way that is immediately seen to be
coherent. However, it turns out to have a very simple motivating
explanation at the level of sets:

Recall that the **preimage** of a function
$f:AβB$
over a point
$y:B,$
written
$f_{β}(y),$
is the set
${x:AΒβ£Βf(x)=y}.$
The properties of
$f$
being injective and surjective can be profitably rephrased in terms of
its preimages:

a function is injective if each of its preimages has

*at most one*element. For if we have $x,y:A$ and $p:f(x)=f(y),$ then we can look at the set $f_{β}(f(x)):$ it has elements given by $(x,refl),$ and $(y,p).$ For these to be the same, we must have $x=y,$ so $f$ is injective.a function is surjective if each of its preimages has

*at least one*element, in the sense of propositional truncations. This is the actual definition: for the preimage $f_{β}(y)$ to be inhabited means that there exists $x:A$ with $f(x)=y.$

Putting these together, a function is a bijection if each of its fibres has exactly one element. Phrased as above, weβve actually arrived exactly at the definition of equivalence proposed by Voevodsky: we just have to rephrase a few things.

Rather than talking about preimages, in the context of homotopy type
theory, we refer to them as **(homotopy) fibres** over a
given point. Not only is this an objectively more aesthetic name, but it
reminds us that the path
$f(x)=y$
is actual *structure* we are equipping the point with, rather
than being a property of points.

fibre : (A β B) β B β Type _ fibre {A = A} f y = Ξ£[ x β A ] (f x β‘ y)

Finally, rather than talking of types with *exactly one
element*, we already have a rephrasing which works at the level of
homotopy type theory: contractibility. This is
exactly the conjunction of the assertions above, just packaged in a way
that does not require us to first define propositional
truncations. A function is an **equivalence** if all of
its fibres are contractible:

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

To warm up, letβs show that the identity map is an equivalence, working with the definition directly. First, we have to show that the fibre over $y$ has an element, for which we can take $(y,refl),$ since what weβre looking for boils down to an element $y:A$ which is mapped to $y$ by the identity function.

id-equiv : is-equiv {A = A} id id-equiv .is-eqv y .centre = y , refl

Then, given any pair
$(x,p)$
with
$x:A$
and
$p:x=y,$
we must show that we have
$(y,refl)=(x,p).$
But this is exactly what path
induction promises us! Rather than an appeal to transport, we can
directly use a *connection*:

id-equiv .is-eqv y .paths (x , p) i = p (~ i) , Ξ» j β p (~ i β¨ j)

-- This helper is for functions f, g that cancel eachother, up to -- definitional equality, without any case analysis on the argument: strict-fibres : β {β β'} {A : Type β} {B : Type β'} {f : A β B} (g : B β A) (b : B) β Ξ£[ t β fibre f (f (g b)) ] ((t' : fibre f b) β Path (fibre f (f (g b))) t (g (f (t' .fst)) , ap (f β g) (t' .snd))) strict-fibres {f = f} g b .fst = (g b , refl) strict-fibres {f = f} g b .snd (a , p) i = (g (p (~ i)) , Ξ» j β f (g (p (~ i β¨ j)))) -- This is more efficient than using IsoβEquiv. When f (g x) is definitionally x, -- the type reduces to essentially is-contr (fibre f b).

Since Cubical Agda has primitives that refer to equivalences, we have
to take some time to teach the system about the type we just defined
above. In addition to teaching it how to project the underlying function
of an equivalence, we must prove that an equivalence has contractible
fibres β but what the system asks of us is that each partial fibre be
*extensible*: the cubical phrasing of contractibility.

{-# 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' #-}

equiv-centre : (e : A β B) (y : B) β fibre (e .fst) y equiv-centre e y = e .snd .is-eqv y .centre equiv-path : (e : A β B) (y : B) β (v : fibre (e .fst) y) β Path _ (equiv-centre e y) v equiv-path e y = e .snd .is-eqv y .paths

### is-equiv is a propositionπ

Since being contractible is a proposition, and being an equivalence simply quantifies contractibility over each fibre, we can directly conclude that being an equivalence is a proposition.

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

### Equivalences are invertibleπ

We can now show that equivalences are invertible. This will amount to taking apart the proof that each fibre is contractible. If we have $y:B,$ then the centre of contraction of $f_{β}(y)$ gives us a distinguished $x:A$ and a path $f(x)=y:$

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) (y : B) β f (equivβinverse eqv y) β‘ y equivβcounit eqv y = eqv .is-eqv y .centre .snd

Now we have to show that applying the inverse to $f(x)$ gives us back $x.$ But note that $f_{β}(fx)$ has two inhabitants: the centre of contraction, which is projected by the inverse, but also the simpler $(x,refl).$ Since the fibre is contractible, we have a path $f_{β1}(fx)=x.$

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

Contractibility gives us, in addition to a path between the
*points*
$f_{β1}(fx)=x,$
a particular higher-dimensional *square*. Note that we have two
ways of proving that
$ff_{β1}fx=fx,$
corresponding to either cancelling the outer
$ff_{β1}$
or the inner
$f_{β1}f:$
$f(Ξ·x)$
and
$Ξ΅fx.$
The square we obtain tells us that these are actually the same:

equivβsquare : β {f : A β B} (eqv : is-equiv f) (x : A) β Square (ap f (equivβunit eqv x)) (equivβcounit eqv (f x)) refl refl equivβsquare {f = f} eqv x i j = eqv .is-eqv (f x) .paths (x , refl) i .snd j

However, the square above is slightly skewed: we would have preferred
for the two non-trivial paths to be in opposite sides, so that it would
correspond to a `Path`

between the paths. We can
use `hcomp`

to slide one of the faces
around to get us the more useful direct proof that
$f(Ξ·x)=Ξ΅fx.$

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 (k = i0) β equivβsquare eqv x j i 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

## Note that the law established above has a symmetric counterpart, showing that $f_{β1}(Ξ΅x)=Ξ·f_{β1}(x).$ However, we can prove that this follows from the law above, using another cubical argument. Since the extent of the proof is another lifting problem, we wonβt expand on the details.

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)

Finally, itβll be convenient for us to package some of the theorems above into a proof that every equivalence is an isomorphism:

is-equivβis-iso : {f : A β B} β is-equiv f β is-iso f is-equivβis-iso eqv .is-iso.inv = equivβinverse eqv is-equivβis-iso eqv .is-iso.rinv = equivβcounit eqv is-equivβis-iso eqv .is-iso.linv = equivβunit eqv

## Improving isomorphismsπ

Having shown that being an equivalence is a proposition and
*implies* being an isomorphism, weβre left with the trickiest
part: showing that itβs *implied by* being an isomorphism. The
argument presented here is *natively cubical*; we do everything
in terms of lifting properties. There is a more βalgebraicβ version,
factoring through the intermediate notion of half-adjoint
equivalence, available on that page.

Weβll write
$(f,g,s,t)$
for the the function
$f:AβB,$
its inverse
$g:BβA,$
and the two homotopies. Our construction *definitionally*
preserves
$f,$
$g$
and the homotopy
$s:fgβΌid.$
However, it can *not* preserve the proof
$t:gfβΌid,$
since that would imply that `is-iso`

is a proposition, which,
again, is provably not the
case.

module _ {f : A β B} (i : is-iso f) where open is-iso i renaming (inv to g ; rinv to s ; linv to t)

We want to show that, for any
$y,$
the `fibre`

of
$f$
over
$y$
is contractible. According to our decomposition above, it will suffice
to show that the fibre is propositional, and that it is inhabited.
Inhabitation is easy β
$(gy,sy)$
belongs to the fibre
$f_{β}(y).$
Letβs focus on propositionality.

Suppose that we have
$y,$
$x_{0},$
$x_{1},$
$p_{0}$
and
$p_{1}$
as below; Note that
$(x_{0},p_{0})$
and
$(x_{1},p_{1})$
are fibres of
$f$
over
$y.$
What we need to show is that we have some
$Ο:x_{0}β‘x_{1}$
and
$p_{0}β‘p_{1}$
* over*
$Ο.$

private module _ (y : B) (x0 x1 : A) (p0 : f x0 β‘ y) (p1 : f x1 β‘ y) where

As an intermediate step in proving that
$p_{0}β‘p_{1},$
we *must* show that
$x_{0}β‘x_{1}$
β without this, we canβt even *state* that
$p_{0}$
and
$p_{1}$
are identified, since they live in different types! To this end, we will
build
$Ο:x_{0}β‘x_{1},$
parts of which will be required to assemble the overall proof that
$p_{0}β‘p_{1}.$

Weβll detail the construction of
$Ο_{0};$
for
$Ο_{1},$
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
$gΒyβ‘gΒy$
(`refl`

),
$gΒ(fΒx_{0})β‘gΒy$
(the action of `g`

on `p0`

), and
$gΒ(fΒx_{0})=x_{0}$
by the assumption that
$g$
is a right inverse to
$f.$
Diagrammatically, these fit together into a square:

The missing line in this square is
$Ο_{0}.$
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 $Ο_{1}$ is analogous, Iβll simply present the square. We correspondingly name the missing face $Ο_{1}$ and the filler $ΞΈ_{1}.$

Οβ : 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
$gΒy$
face, we obtain
$Ο:x_{0}β‘x_{1}.$
This square *also* has a filler, connecting
$Ο_{0}$
and
$Ο_{1}$
over the line
$gΒyβ‘ΟΒi.$

Ο : 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
$p_{0}β‘p_{1}$
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 $apgΒp_{0}$ and $apgΒp_{1}$ 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Β(Β¬Βj),$
i.e.Β `(ΞΈ i (~ j))`

in the code. Similarly, the
$j=i1$
(bottom) face is `g y`

, the
$j=i0$
(top) face is `t (Ο i) (~ k)`

, and similarly for
$i=i0$
(left) and
$i=i1$
(right).

The fact that
$j$
only appears as
$Β¬j$
can be understood as the diagram above being *upside-down*.
Indeed,
$Ο_{0}$
and
$Ο_{1}$
in the boundary of
$ΞΈ$
(the inner, blue face) are inverted when their types are considered.
Weβre in the home stretch: Using our assumption
$s:f(gΒx)=x,$
we can cancel all of the
$fβgs$
in the diagram above to get what we wanted:
$p_{0}β‘p_{1}.$

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 $i=i0,$ right is $i=i1,$ up is $j=i0,$ and down is $j=i1.$

Putting all of this together, we get that $(x_{0},p_{0})β‘(x_{1},p_{1}).$ Since there were no assumptions on any of the variables under consideration, this indeed says that the fibre over $y$ is a proposition for any choice of $y.$

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 $y$ is inhabited by $(gΒy,sΒy),$ 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)

If we package this differently, then we can present it as a map between the types of isomorphisms $AβB$ and equivalences $AβB.$

IsoβEquiv : Iso A B β A β B IsoβEquiv (f , is-iso) = f , is-isoβis-equiv is-iso

inverse-is-equiv : {f : A β B} (eqv : is-equiv f) β is-equiv (equivβinverse eqv) inverse-is-equiv {f = f} eqv .is-eqv x .centre = record { fst = f x ; snd = equivβunit eqv x } inverse-is-equiv {A = A} {B = B} {f = f} eqv .is-eqv x .paths (y , p) = q where g = equivβinverse eqv Ξ· = equivβunit eqv Ξ΅ = equivβcounit eqv zag = equivβzag eqv q : (f x , Ξ· x) β‘ (y , p) q i .fst = (ap f (sym p) β Ξ΅ y) i q i .snd j = hcomp (β i β¨ β j) Ξ» where k (k = i0) β zag y j i k (i = i0) β Ξ· (p k) (j β§ k) k (i = i1) β p (k β§ j) k (j = i0) β g (β-filler' (ap f (sym p)) (Ξ΅ y) k i) k (j = i1) β Ξ· (p k) (i β¨ k) module Equiv {β β'} {A : Type β} {B : Type β'} (f : A β B) where to = f .fst from = equivβinverse (f .snd) Ξ· = equivβunit (f .snd) Ξ΅ = equivβcounit (f .snd) zig = equivβzig (f .snd) zag = equivβzag (f .snd) injective : β {x y} β to x β‘ to y β x β‘ y injective p = ap fst $ is-contrβis-prop (f .snd .is-eqv _) (_ , refl) (_ , sym p) injectiveβ : β {x y z} β to x β‘ z β to y β‘ z β x β‘ y injectiveβ p q = ap fst $ is-contrβis-prop (f .snd .is-eqv _) (_ , p) (_ , q) inverse : B β A inverse = from , inverse-is-equiv (f .snd) adjunctl : β {x y} β to x β‘ y β x β‘ from y adjunctl p = sym (Ξ· _) β ap from p adjunctr : β {x y} β x β‘ from y β to x β‘ y adjunctr p = ap to p β Ξ΅ _ open is-iso adjunct : β {x y} β (to x β‘ y) β (x β‘ from y) adjunct {x} {y} .fst = adjunctl adjunct {x} {y} .snd = is-isoβis-equiv Ξ» where .inv β adjunctr .rinv p β J (Ξ» _ p β sym (Ξ· _) β ap from (ap to (sym p) β Ξ΅ _) β‘ sym p) (sym (β-swapl (β-idr _ β sym (zag _) β sym (β-idl _) β sym (ap-β from _ _)))) (sym p) .linv β J (Ξ» _ p β ap to (sym (Ξ· _) β ap from p) β Ξ΅ _ β‘ p) (sym (β-swapr (β-idl _ β ap sym (sym (zig _)) β sym (β-idr _) β sym (ap-β to _ _))))

## Simple constructionsπ

Having established the three desiderata for a notion of equivalence, we will spend the rest of this module constructing readily-available equivalences, and establishing basic facts about them.

### Contractible typesπ

If
$A$
and
$B$
are contractible types, then any function
$f:AβB$
must be homotopic to the function which sends everything in
$A$
to the centre of
$B;$
This function is invertible by sending everything *in
$B$*
to the centre of
$A.$
Therefore, any function between contractible types is an
equivalence.

is-contrβis-equiv : 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 _ f-is-iso .is-iso.inv _ = cA .centre f-is-iso .is-iso.rinv _ = is-contrβis-prop cB _ _ f-is-iso .is-iso.linv _ = is-contrβis-prop cA _ _

Pairing this with the βcanonicalβ function, we obtain an equivalence between any contractible types. Since the unit type is contractible, any contractible type is equivalent to the unit.

is-contrββ : is-contr A β is-contr B β A β B is-contrββ cA cB = (Ξ» _ β cB .centre) , is-contrβis-equiv cA cB is-contrβββ€ : is-contr A β A β β€ is-contrβββ€ c = is-contrββ c β€-is-contr

### Strictness of the empty typeπ

We say that an initial object is
*strict* if every map into it is an equivalence. This holds of
the empty type, and moreover, the proof is delightfully simple! Since
showing that
$f:Aββ₯$
is an equivalence boils down to showing something about
$f$
*given a point
$y:β₯$*,
itβs immediate that any map into the empty type is an equivalence.

Β¬-is-equiv : (f : A β β₯) β is-equiv f Β¬-is-equiv f .is-eqv () is-emptyβββ₯ : Β¬ A β A β β₯ is-emptyβββ₯ Β¬a = _ , Β¬-is-equiv Β¬a

### Propositional extensionality (redux)π

Following the trend set by contractible types, above, another h-level
for which constructing equivalences is easy are the propositions. If
$P$
and
$Q$
are propositions, then any map
$PβP$
(resp.
$QβQ)$
must be homotopic to the identity, and consequently any pair of
functions
$PβQ$
and
$QβP$
is a pair of inverses. Put another way, any *biimplication*
between propositions is an equivalence.

biimp-is-equiv : (f : P β Q) β (Q β P) β is-equiv f biimp-is-equiv f g .is-eqv y .centre .fst = g y biimp-is-equiv f g .is-eqv y .centre .snd = qprop (f (g y)) y biimp-is-equiv f g .is-eqv y .paths (p' , path) = Ξ£-pathp (pprop (g y) p') (is-propβsquarep (Ξ» _ _ β qprop) _ _ _ _) prop-ext : (P β Q) β (Q β P) β P β Q prop-ext pβq qβp .fst = pβq prop-ext pβq qβp .snd = biimp-is-equiv pβq qβp

### Groupoid operationsπ

Since types are
higher groupoids, we have certain algebraic laws regarding the
behaviour of path operations which can be expressed as saying that they
form equivalences. First, the *inverse path* operation is
definitionally involutive, so itβs its own two-sided inverse:

sym-equiv : β {β} {A : Type β} {x y : A} β (x β‘ y) β (y β‘ x) sym-equiv .fst = sym sym-equiv .snd = is-isoβis-equiv (iso sym (Ξ» _ β refl) (Ξ» _ β refl))

If we have a path
$p:x=y,$
then
$p_{β1}pq=q,$
and
$pp_{β1}r=r.$
Viewing this as a function of
$q,$
it says that the operation *precompose with
$p$*
is inverted on both sides by precomposition with
$p_{β1}.$

β-pre-equiv : β {β} {A : Type β} {x y z : A} β x β‘ y β (y β‘ z) β (x β‘ z) β-pre-equiv p .fst q = p β q β-pre-equiv p .snd = is-isoβis-equiv Ξ» where .inv q β sym p β q .rinv q β β-assoc p _ _ Β·Β· ap (_β q) (β-invr p) Β·Β· β-idl q .linv q β β-assoc (sym p) _ _ Β·Β· ap (_β q) (β-invl p) Β·Β· β-idl q

Similarly, *post*composition with
$p$
is inverted on both sides by postcomposition with
$p_{β1},$
so it too is an equivalence.

β-post-equiv : β {β} {A : Type β} {x y z : A} β y β‘ z β (x β‘ y) β (x β‘ z) β-post-equiv p .fst q = q β p β-post-equiv p .snd = is-isoβis-equiv Ξ» where .inv q β q β sym p .rinv q β sym (β-assoc q _ _) Β·Β· ap (q β_) (β-invl p) Β·Β· β-idr q .linv q β sym (β-assoc q _ _) Β·Β· ap (q β_) (β-invr p) Β·Β· β-idr q

### The Lift typeπ

Because Agdaβs universes are not *cumulative*, we can not
freely move a type
$A:Type_{0}$
to conclude that
$A:Type_{1},$
or to higher universes. To work around this, we have a `Lift`

type, which, given a small
type
$A:Type_{i}$
and some universe
$j>i,$
gives us a *name* for
$A$
in
$Type_{j}.$
To know that this operation is coherent, we can prove that the lifting
map

is an equivalence: the name of
$A$
in
$Type_{j}$
really is equivalent to the type we started with. Because `Lift`

is a very well-behaved
record type, the proof that this is an equivalence looks very similar to
the proof that the identity function is an equivalence:

Lift-β : β {a β} {A : Type a} β Lift β A β A Lift-β .fst (lift a) = a Lift-β .snd .is-eqv a .centre = lift a , refl Lift-β .snd .is-eqv a .paths (x , p) i .fst = lift (p (~ i)) Lift-β .snd .is-eqv a .paths (x , p) i .snd j = p (~ i β¨ j)

Finally, while weβre here, we can easily prove that the `Lift`

type *respects
equivalences*, in that if we have small
$AβB,$
then their liftings
$Lift_{j}A$
and
$Lift_{j}B$
will still be equivalent.

Lift-ap : β {a b β β'} {A : Type a} {B : Type b} β A β B β Lift β A β Lift β' B Lift-ap (f , eqv) .fst (lift x) = lift (f x) Lift-ap f .snd .is-eqv (lift y) .centre = lift (Equiv.from f y) , ap lift (Equiv.Ξ΅ f y) Lift-ap f .snd .is-eqv (lift y) .paths (lift x , q) i = lift (p i .fst) , Ξ» j β lift (p i .snd j) where p = f .snd .is-eqv y .paths (x , ap Lift.lower q)

### Involutionsπ

Finally, we can show here that any *involution* β a function
$AβA,$
which inverts *itself* β is an equivalence.

is-involutiveβis-equiv : {f : A β A} β (β a β f (f a) β‘ a) β is-equiv f is-involutiveβis-equiv inv = is-isoβis-equiv (iso _ inv inv)

## Closure propertiesπ

We will now show a rather fundamental property of equivalences: they
are closed under *two-out-of-three*. This means that, considering
$f:AβB,$
$g:BβC,$
and
$(gβf):AβC$
as a set of three things, if any two are an equivalence, then so is the
third:

module _ {β ββ ββ} {A : Type β} {B : Type ββ} {C : Type ββ} {f : A β B} {g : B β C} where

β-is-equiv : is-equiv f β is-equiv g β is-equiv (g β f) equiv-cancell : is-equiv g β is-equiv (g β f) β is-equiv f equiv-cancelr : is-equiv f β is-equiv (g β f) β is-equiv g

We have already shown the first of these, when the individual functions are equivalences, since being an equivalence is logically equivalent to being an isomorphism. Supposing that $g$ and $gβf$ are, then we can show that

$BgβC(gf)_{β1}βA$is an inverse to $f;$ the other case is symmetric. Since both of the proofs are just calculations, we will not comment on them.

## However, we will render them for the curious reader. Itβs an instructive exercise to work these out for yourself!

β-is-equiv ef eg = is-isoβis-equiv (β-is-iso (is-equivβis-iso eg) (is-equivβis-iso ef)) equiv-cancell eg egf = is-isoβis-equiv (iso inv right left) where inv : B β A inv x = equivβinverse egf (g x) opaque right : is-right-inverse inv f right x = f (equivβinverse egf (g x)) β‘Λβ¨ equivβunit eg _ β©β‘Λ equivβinverse eg (g (f (equivβinverse egf (g x)))) β‘β¨ ap (equivβinverse eg) (equivβcounit egf _) β©β‘ equivβinverse eg (g x) β‘β¨ equivβunit eg _ β©β‘ x β left : is-left-inverse inv f left x = equivβunit egf x equiv-cancelr ef egf = is-isoβis-equiv (iso inv right left) where inv : C β B inv x = f (equivβinverse egf x) right : is-right-inverse inv g right x = equivβcounit egf x left : is-left-inverse inv g left x = f (equivβinverse egf (g x)) β‘Λβ¨ ap (f β equivβinverse egf β g) (equivβcounit ef _) β©β‘Λ f (equivβinverse egf (g (f (equivβinverse ef x)))) β‘β¨ ap f (equivβunit egf _) β©β‘ f (equivβinverse ef x) β‘β¨ equivβcounit ef _ β©β‘ x β

Specialising these, any left- or right- inverse of an equivalence
must be homotopic to the specified one, so that *it too* is an
equivalence.

left-inverseβequiv : {f : A β B} {g : B β A} β is-left-inverse g f β is-equiv f β is-equiv g left-inverseβequiv linv ef = equiv-cancelr ef (subst is-equiv (sym (funext linv)) id-equiv) right-inverseβequiv : {f : A β B} {g : B β A} β is-right-inverse g f β is-equiv f β is-equiv g right-inverseβequiv rinv ef = equiv-cancell ef (subst is-equiv (sym (funext rinv)) id-equiv)

### Equivalence reasoningπ

To simplify working with chains of equivalences, we can re-package
their closure operations as mixfix operators, so that we have a
shorthand notation for working with composites of pairs of equivalences
*and* long chains of equivalences, where making the intermediate
steps explicit is more important.

idβ : β {β} {A : Type β} β A β A idβ = id , id-equiv _βe_ : A β B β B β C β A β C _βe_ (f , ef) (g , eg) = g β f , β-is-equiv ef eg _eβ»ΒΉ : A β B β B β A ((f , ef) eβ»ΒΉ) = equivβinverse ef , inverse-is-equiv ef ββ¨β©-syntax : β {β ββ ββ} (A : Type β) {B : Type ββ} {C : Type ββ} β B β C β A β B β A β C ββ¨β©-syntax A g f = f βe g _βΛβ¨_β©_ : β {β ββ ββ} (A : Type β) {B : Type ββ} {C : Type ββ} β B β A β B β C β A β C A βΛβ¨ f β©βΛ g = f eβ»ΒΉ βe g _ββ¨β©_ : β {β ββ} (A : Type β) {B : Type ββ} β A β B β A β B x ββ¨β© xβ‘y = xβ‘y _ββ : β {β} (A : Type β) β A β A x ββ = idβ

infixr 30 _βe_ infix 31 _eβ»ΒΉ infixr 2 ββ¨β©-syntax _ββ¨β©_ _βΛβ¨_β©_ infix 3 _ββ infix 21 _β_ syntax ββ¨β©-syntax x q p = x ββ¨ p β© q lift-inj : β {β β'} {A : Type β} {a b : A} β lift {β = β'} a β‘ lift {β = β'} b β a β‘ b lift-inj p = ap Lift.lower p