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 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 (λ 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$ .

    π : x0 ≡ x1
    π i = hcomp (λ k → λ { (i = i0) → π₀ k
                         ; (i = i1) → π₁ k
                         })
                (g y)

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