open import 1Lab.HLevel
open import 1Lab.Path
open import 1Lab.Type

open is-contr

module 1Lab.Equiv where


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 isβˆ’equiv(f)\id{is-equiv}(f) to be β€œcoherent” is:

  • Being an isomorphism implies being an equivalence (isβˆ’iso(f)β†’isβˆ’equiv(f)\id{is-iso}(f) \to \id{is-equiv}(f))

  • Being an equivalence implies being an isomorphism (isβˆ’equiv(f)β†’isβˆ’iso(f)\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.

    ℓ₁ β„“β‚‚ : 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
    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 _≃_ #-}

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 ff is an isomorphism consists of a function gg in the other direction, together with homotopies exhibiting gg as a left- and right- inverse to ff.

record is-iso (f : A β†’ B) : Type (level-of A βŠ” level-of B) where
  constructor iso
    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

  : {f : A → B} (eqv : is-equiv f) → is-right-inverse (equiv→inverse eqv) f
equiv→section eqv y = eqv .is-eqv y .centre .snd

  : {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 ff, its inverse gg, and the proof ss that gg is a right inverse to ff. 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β†’Bf : A \to B and g:Bβ†’Ag : B \to A, and we’re given witnesses s:f(gΒ x)=xs : f (g\ x) = x and t:g(fΒ x)=xt : g (f\ x) = x (named for section and retraction) that ff and gg are inverses. We want to show that, for any yy, the fibre of ff over yy is contractible. It suffices to show that the fibre is propositional, and that it is inhabited.

We begin with showing that the fibre over yy is propositional, since that’s the harder of the two arguments. Suppose that we have yy, x0x_0, x1x_1, p0p_0 and p1p_1 as below; Note that (x0,p0)(x_0, p_0) and (x1,p1)(x_1, p_1) are fibres of ff over yy. What we need to show is that we have some Ο€:x0≑x1\pi : x_0 ≑ x_1 and p0≑p1p_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 p0≑p1p_0 ≑ p_1, we must show that x0≑x1x_0 ≑ x_1 - without this, we can’t even state that p0p_0 and p1p_1 are identified, since they live in different types! To this end, we will build Ο€:p0≑p1\pi : p_0 ≑ p_1, parts of which will be required to assemble the overall proof that p0≑p1p_0 ≑ p_1.

We’ll detail the construction of Ο€0\pi_0; for Ο€1\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Β yg\ y ≑ g\ y (refl), gΒ (fΒ x0)≑gΒ yg\ (f\ x_0) ≑ g\ y (the action of g on p0), and gΒ (fΒ x0)=x0g\ (f\ x_0) = x_0 by the assumption that gg is a right inverse to ff. Diagramatically, these fit together into a square:

The missing line in this square is Ο€0\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 Ο€1\pi_1 is analogous, I’ll simply present the square. We correspondingly name the missing face Ο€1\pi_1 and the filler ΞΈ1\theta_1.

Joining these paths by their common gΒ yg\ y face, we obtain Ο€:x0≑x1\pi : x_0 ≑ x_1. This square also has a filler, connecting Ο€0\pi_0 and Ο€1\pi_1 over the line gΒ y≑π ig\ y ≑ \pi\ i.

This concludes the construction of Ο€\pi, and thus, the 2D part of the proof. Now, we want to show that p0≑p1p_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 apΒ gΒ p0\id{ap}\ g\ p_0 and apΒ gΒ p1\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 ΞΈΒ iΒ (¬ j)\theta\ i\ (\neg\ j), i.e.Β (ΞΈ i (~ j)) in the code. Similarly, the j=i1j = \id{i1} (bottom) face is g y, the j=i0j = \id{i0} (top) face is t (Ο€ i) (~ k), and similarly for i=i0i = \id{i0} (left) and i=i1i = \id{i1} (right).

The fact that jj only appears as Β¬j\neg j can be understood as the diagram above being upside-down. Indeed, Ο€0\pi_0 and Ο€1\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)=xs : f (g\ x) = x, we can cancel all of the f∘gf \circ gs in the diagram above to get what we wanted: p0≑p1p_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=i0i = \id{i0}, right is i=i1i = \id{i1}, up is j=i0j = \id{i0}, and down is j=i1j = \id{i1}.

Putting all of this together, we get that (x0,p0)≑(x1,p1)(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 yy is a proposition for any choice of yy.

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