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 $\id{is-equiv}(f)$ to be “coherent” is:

Being an isomorphism implies being an equivalence ($\id{is-iso}(f) \to \id{is-equiv}(f)$)

Being an equivalence implies being an isomorphism ($\id{is-equiv}(f) \to \id{is-iso}(f)$); 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-inverible 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 = Σ (is-equiv {A = A} {B = B}) 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) → Partial ψ (fibre (w .fst) a) → fibre (w .fst) a is-eqv' A B (f , is-equiv) a ψ u0 = hcomp (λ i → λ { (ψ = i0) → c .centre ; (ψ = i1) → c .paths (u0 1=1) i }) (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 (λ k → λ { (i = i0) → p2 w j ; (i = i1) → q2 w (j ∨ ~ k) ; (j = i0) → p2 (q2 w (~ k)) i ; (j = i1) → w }) (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 $f$ is an isomorphism consists of a function $g$ in the other direction, together with homotopies exhibiting $g$ as a left- and right- inverse to $f$.

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 = Σ (is-iso {A = A} {B = B})

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→section : {f : A → B} (eqv : is-equiv f) → is-right-inverse (equiv→inverse eqv) f equiv→section eqv y = eqv .is-eqv y .centre .snd equiv→retraction : {f : A → B} (eqv : is-equiv f) → is-left-inverse (equiv→inverse eqv) f equiv→retraction {f = f} eqv x i = eqv .is-eqv (f x) .paths (x , refl) i .fst 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 $f$, its inverse $g$, *and* the proof $s$ that $g$ is a right inverse to $f$. 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 $f : A \to B$ and $g : B \to A$, and we’re given witnesses $s : f (g\ x) = x$ and $t : g (f\ x) = x$ (named for **s**ection and re**t**raction) that $f$ and $g$ are inverses. We want to show that, for any $y$, the fibre of $f$ over $y$ is contractible. It suffices to show that the fibre is propositional, and that it is inhabited.

We begin with showing that the fibre over $y$ is propositional, since that’s the harder of the two arguments. 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 $\pi : x_0 ≡ x_1$ and $p_0 ≡ p_1$ * over* $\pi$.

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 $\pi : p_0 ≡ p_1$, parts of which will be required to assemble the overall proof that $p_0 ≡ p_1$.

We’ll detail the construction of $\pi_0$; for $\pi_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$. Diagramatically, these fit together into a square:

The missing line in this square is $\pi_0$. Since the *inside* (the filler) will be useful to us later, we also give it a name: $\theta$.

π₀ : g y ≡ x0 π₀ i = hcomp (λ k → λ { (i = i0) → g y ; (i = i1) → t x0 k }) (g (p0 (~ i))) θ₀ : Square (ap g (sym p0)) refl (t x0) π₀ θ₀ i j = hfill (λ k → λ { (i = i0) → g y ; (i = i1) → t x0 k }) (inS (g (p0 (~ i)))) j

Since the construction of $\pi_1$ is analogous, I’ll simply present the square. We correspondingly name the missing face $\pi_1$ and the filler $\theta_1$.

π₁ : g y ≡ x1 π₁ i = hcomp (λ k → λ { (i = i0) → g y ; (i = i1) → t x1 k }) (g (p1 (~ i))) θ₁ : Square (ap g (sym p1)) refl (t x1) π₁ θ₁ i j = hfill (λ k → λ { (i = i0) → g y ; (i = i1) → t x1 k }) (inS (g (p1 (~ i)))) j

Joining these paths by their common $g\ y$ face, we obtain $\pi : x_0 ≡ x_1$. This square *also* has a filler, connecting $\pi_0$ and $\pi_1$ over the line $g\ y ≡ \pi\ i$.

This concludes the construction of $\pi$, and thus, the 2D part of the proof. Now, we want to show that $p_0 ≡ p_1$ over a path induced by $\pi$. 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 $\theta$ to be the filler for the square above.

θ : Square refl π₀ π₁ π θ i j = hfill (λ k → λ { (i = i1) → π₁ k ; (i = i0) → π₀ k }) (inS (g y)) j

Observe that we can coherently alter $\theta$ to get $\iota$ below, which expresses that $\id{ap}\ g\ p_0$ and $\id{ap}\ g\ p_1$ are identified.

ι : Square (ap (g ∘ f) π) (ap g p0) (ap g p1) refl ι i j = hcomp (λ k → λ { (i = i0) → θ₀ (~ j) (~ k) ; (i = i1) → θ₁ (~ j) (~ k) ; (j = i0) → t (π i) (~ k) ; (j = i1) → g y }) (θ i (~ j))

This composition can be visualised as the *red* (front) face in the diagram below. The back face is $\theta\ i\ (\neg\ j)$, i.e. `(θ i (~ j))`

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

, the $j = \id{i0}$ (top) face is `t (π i) (~ k)`

, and similarly for $i = \id{i0}$ (left) and $i = \id{i1}$ (right).

The fact that $j$ only appears as $\neg j$ can be understood as the diagram above being *upside-down*. Indeed, $\pi_0$ and $\pi_1$ in the boundary of $\theta$ (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 \circ g$s in the diagram above to get what we wanted: $p_0 ≡ p_1$.

sq1 : Square (ap f π) p0 p1 refl sq1 i j = hcomp (λ k → λ { (i = i0) → s (p0 j) k ; (i = i1) → s (p1 j) k ; (j = i0) → s (f (π i)) k ; (j = i1) → s y k }) (f (ι i j))

The composition above can be visualised as the front (red) face in the cubical diagram below. Once more, left is $i = \id{i0}$, right is $i = \id{i1}$, up is $j = \id{i0}$, and down is $j = \id{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)

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→retraction (eqv .snd) ; linv = equiv→section (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 _ _ _ _)