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

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

• Being an equivalence implies being an isomorphism ($\mathrm{is-equiv}(f) \to \mathrm{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-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

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 $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 = Σ (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 $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 section and retraction) 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 (∂ 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 $\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 (∂ 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 $\pi : x_0 ≡ x_1$. This square also has a filler, connecting $\pi_0$ and $\pi_1$ over the line $g\ y ≡ \pi\ 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 $\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 (∂ i) j λ where
      k (i = i1) → π₁ k
      k (i = i0) → π₀ k
      k (k = i0) → g y

Observe that we can coherently alter $\theta$ to get $\iota$ below, which expresses that $\mathrm{ap}\ g\ p_0$ and $\mathrm{ap}\ g\ 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 $\theta\ i\ (\neg\ j)$, i.e. (θ i (~ j)) in the code. Similarly, the $j = \mathrm{i1}$ (bottom) face is g y, the $j = \mathrm{i0}$ (top) face is t (π i) (~ k), and similarly for $i = \mathrm{i0}$ (left) and $i = \mathrm{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 (∂ 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 = \mathrm{i0}$, right is $i = \mathrm{i1}$, up is $j = \mathrm{i0}$, and down is $j = \mathrm{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→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  _∙e_
infixr  _≃⟨⟩_ _≃⟨_⟩_
infix   _≃∎

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 _ _ _ _)