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

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

  • Being an equivalence implies being an isomorphism (isequiv(f)isiso(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:ABf : A \to B and g:BAg : 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 π:x0x1\pi : x_0 ≡ x_1 and p0p1p_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 p0p1p_0 ≡ p_1, we must show that x0x1x_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 π:p0p1\pi : p_0 ≡ p_1, parts of which will be required to assemble the overall proof that p0p1p_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 yg 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 π:x0x1\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 p0p1p_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 fgf \circ gs in the diagram above to get what we wanted: p0p1p_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 _ _ _ _)