Equivalences

Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides, maybemabeline, Julian KG, Raymond Baker, fernabnor and louismntnu.

Created on 2022-02-04.
Last modified on 2024-03-20.

module foundation-core.equivalences where
Imports 
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.universe-levels
open import foundation.whiskering-homotopies-composition

open import foundation-core.cartesian-product-types
open import foundation-core.coherently-invertible-maps
open import foundation-core.function-types
open import foundation-core.homotopies
open import foundation-core.identity-types
open import foundation-core.invertible-maps
open import foundation-core.retractions
open import foundation-core.sections

Idea

An equivalence is a map that has a section and a (separate) retraction. This condition is also called being biinvertible.

The condition of biinvertibility may look odd: Why not say that an equivalence is a map that has a 2-sided inverse? The reason is that the condition of invertibility is structure, whereas the condition of being biinvertible is a property. To quickly see this: if f is an equivalence, then it has up to homotopy only one section, and it has up to homotopy only one retraction.

Definition

The predicate of being an equivalence

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2}
  where

  is-equiv : (A → B) → UU (l1 ⊔ l2)
  is-equiv f = section f × retraction f

Components of a proof of equivalence

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} (H : is-equiv f)
  where

  section-is-equiv : section f
  section-is-equiv = pr1 H

  retraction-is-equiv : retraction f
  retraction-is-equiv = pr2 H

  map-section-is-equiv : B → A
  map-section-is-equiv = map-section f section-is-equiv

  map-retraction-is-equiv : B → A
  map-retraction-is-equiv = map-retraction f retraction-is-equiv

  is-section-map-section-is-equiv : is-section f map-section-is-equiv
  is-section-map-section-is-equiv = is-section-map-section f section-is-equiv

  is-retraction-map-retraction-is-equiv :
    is-retraction f map-retraction-is-equiv
  is-retraction-map-retraction-is-equiv =
    is-retraction-map-retraction f retraction-is-equiv

Equivalences

module _
  {l1 l2 : Level} (A : UU l1) (B : UU l2)
  where

  equiv : UU (l1 ⊔ l2)
  equiv = Σ (A → B) is-equiv

infix 6 _≃_

_≃_ : {l1 l2 : Level} (A : UU l1) (B : UU l2) → UU (l1 ⊔ l2)
A ≃ B = equiv A B

Components of an equivalence

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2} (e : A ≃ B)
  where

  map-equiv : A → B
  map-equiv = pr1 e

  is-equiv-map-equiv : is-equiv map-equiv
  is-equiv-map-equiv = pr2 e

  section-map-equiv : section map-equiv
  section-map-equiv = section-is-equiv is-equiv-map-equiv

  map-section-map-equiv : B → A
  map-section-map-equiv = map-section map-equiv section-map-equiv

  is-section-map-section-map-equiv :
    is-section map-equiv map-section-map-equiv
  is-section-map-section-map-equiv =
    is-section-map-section map-equiv section-map-equiv

  retraction-map-equiv : retraction map-equiv
  retraction-map-equiv = retraction-is-equiv is-equiv-map-equiv

  map-retraction-map-equiv : B → A
  map-retraction-map-equiv = map-retraction map-equiv retraction-map-equiv

  is-retraction-map-retraction-map-equiv :
    is-retraction map-equiv map-retraction-map-equiv
  is-retraction-map-retraction-map-equiv =
    is-retraction-map-retraction map-equiv retraction-map-equiv

The identity equivalence

module _
  {l : Level} {A : UU l}
  where

  is-equiv-id : is-equiv (id {l} {A})
  pr1 (pr1 is-equiv-id) = id
  pr2 (pr1 is-equiv-id) = refl-htpy
  pr1 (pr2 is-equiv-id) = id
  pr2 (pr2 is-equiv-id) = refl-htpy

  id-equiv : A ≃ A
  pr1 id-equiv = id
  pr2 id-equiv = is-equiv-id

Properties

A map is invertible if and only if it is an equivalence

Proof: It is clear that if a map is invertible, then it is also biinvertible, and hence an equivalence.

For the converse, suppose that f : A → B is an equivalence with section g : B → A equipped with G : f ∘ g ~ id, and retraction h : B → A equipped with H : h ∘ f ~ id. We claim that the map g : B → A is also a retraction. To see this, we concatenate the following homotopies

         H⁻¹ ·r g ·r f                  h ·l G ·r f           H
  g ∘ h ---------------> h ∘ f ∘ g ∘ f -------------> h ∘ f -----> id.

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B}
  where

  is-equiv-is-invertible' : is-invertible f → is-equiv f
  is-equiv-is-invertible' (g , H , K) = ((g , H) , (g , K))

  is-equiv-is-invertible :
    (g : B → A) (H : f ∘ g ~ id) (K : g ∘ f ~ id) → is-equiv f
  is-equiv-is-invertible g H K = is-equiv-is-invertible' (g , H , K)

  is-retraction-map-section-is-equiv :
    (H : is-equiv f) → is-retraction f (map-section-is-equiv H)
  is-retraction-map-section-is-equiv H =
    ( ( inv-htpy
        ( ( is-retraction-map-retraction-is-equiv H) ·r
          ( map-section-is-equiv H ∘ f))) ∙h
      ( map-retraction-is-equiv H ·l is-section-map-section-is-equiv H ·r f)) ∙h
    ( is-retraction-map-retraction-is-equiv H)

  is-invertible-is-equiv : is-equiv f → is-invertible f
  pr1 (is-invertible-is-equiv H) = map-section-is-equiv H
  pr1 (pr2 (is-invertible-is-equiv H)) = is-section-map-section-is-equiv H
  pr2 (pr2 (is-invertible-is-equiv H)) = is-retraction-map-section-is-equiv H

Coherently invertible maps are equivalences

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B}
  where

  is-equiv-is-coherently-invertible :
    is-coherently-invertible f → is-equiv f
  is-equiv-is-coherently-invertible H =
    is-equiv-is-invertible' (is-invertible-is-coherently-invertible H)

  is-equiv-is-transpose-coherently-invertible :
    is-transpose-coherently-invertible f → is-equiv f
  is-equiv-is-transpose-coherently-invertible H =
    is-equiv-is-invertible'
      ( is-invertible-is-transpose-coherently-invertible H)

The following maps are not simple constructions and should not be computed with. Therefore, we mark them as abstract.

  abstract
    is-coherently-invertible-is-equiv :
      is-equiv f → is-coherently-invertible f
    is-coherently-invertible-is-equiv =
      is-coherently-invertible-is-invertible ∘ is-invertible-is-equiv

  abstract
    is-transpose-coherently-invertible-is-equiv :
      is-equiv f → is-transpose-coherently-invertible f
    is-transpose-coherently-invertible-is-equiv =
      is-transpose-coherently-invertible-is-invertible ∘ is-invertible-is-equiv

Structure obtained from being coherently invertible

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} (H : is-equiv f)
  where

  map-inv-is-equiv : B → A
  map-inv-is-equiv = pr1 (is-invertible-is-equiv H)

  is-section-map-inv-is-equiv : is-section f map-inv-is-equiv
  is-section-map-inv-is-equiv =
    is-section-map-inv-is-coherently-invertible-is-invertible
      ( is-invertible-is-equiv H)

  is-retraction-map-inv-is-equiv : is-retraction f map-inv-is-equiv
  is-retraction-map-inv-is-equiv =
    is-retraction-map-inv-is-coherently-invertible-is-invertible
      ( is-invertible-is-equiv H)

  coherence-map-inv-is-equiv :
    coherence-is-coherently-invertible f
      ( map-inv-is-equiv)
      ( is-section-map-inv-is-equiv)
      ( is-retraction-map-inv-is-equiv)
  coherence-map-inv-is-equiv =
    coh-is-coherently-invertible-is-invertible (is-invertible-is-equiv H)

  is-equiv-map-inv-is-equiv : is-equiv map-inv-is-equiv
  is-equiv-map-inv-is-equiv =
    is-equiv-is-invertible f
      ( is-retraction-map-inv-is-equiv)
      ( is-section-map-inv-is-equiv)

The inverse of an equivalence is an equivalence

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2} (e : A ≃ B)
  where

  map-inv-equiv : B → A
  map-inv-equiv = map-inv-is-equiv (is-equiv-map-equiv e)

  is-section-map-inv-equiv : is-section (map-equiv e) map-inv-equiv
  is-section-map-inv-equiv = is-section-map-inv-is-equiv (is-equiv-map-equiv e)

  is-retraction-map-inv-equiv : is-retraction (map-equiv e) map-inv-equiv
  is-retraction-map-inv-equiv =
    is-retraction-map-inv-is-equiv (is-equiv-map-equiv e)

  coherence-map-inv-equiv :
    coherence-is-coherently-invertible
      ( map-equiv e)
      ( map-inv-equiv)
      ( is-section-map-inv-equiv)
      ( is-retraction-map-inv-equiv)
  coherence-map-inv-equiv =
    coherence-map-inv-is-equiv (is-equiv-map-equiv e)

  is-equiv-map-inv-equiv : is-equiv map-inv-equiv
  is-equiv-map-inv-equiv = is-equiv-map-inv-is-equiv (is-equiv-map-equiv e)

  inv-equiv : B ≃ A
  pr1 inv-equiv = map-inv-equiv
  pr2 inv-equiv = is-equiv-map-inv-equiv

The 3-for-2 property of equivalences

The 3-for-2 property of equivalences asserts that for any commuting triangle of maps

       h
  A ------> B
   \       /
   f\     /g
     \   /
      V V
       X,

if two of the three maps are equivalences, then so is the third.

We also record special cases of the 3-for-2 property of equivalences, where we only assume maps g : B → X and h : A → B. In this special case, we set f := g ∘ h and the triangle commutes by refl-htpy.

André Joyal proposed calling this property the 3-for-2 property, despite most mathematicians calling it the 2-out-of-3 property. The story goes that on the produce market is is common to advertise a discount as "3-for-2". If you buy two apples, then you get the third for free. Similarly, if you prove that two maps in a commuting triangle are equivalences, then you get the third for free.

The left map in a commuting triangle is an equivalence if the other two maps are equivalences

module _
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
  (f : A → X) (g : B → X) (h : A → B) (T : f ~ g ∘ h)
  where

  abstract
    is-equiv-left-map-triangle : is-equiv h → is-equiv g → is-equiv f
    pr1 (is-equiv-left-map-triangle H G) =
      section-left-map-triangle f g h T
        ( section-is-equiv H)
        ( section-is-equiv G)
    pr2 (is-equiv-left-map-triangle H G) =
      retraction-left-map-triangle f g h T
        ( retraction-is-equiv G)
        ( retraction-is-equiv H)

The right map in a commuting triangle is an equivalence if the other two maps are equivalences

module _
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
  (f : A → X) (g : B → X) (h : A → B) (H : f ~ g ∘ h)
  where

  abstract
    is-equiv-right-map-triangle :
      is-equiv f → is-equiv h → is-equiv g
    is-equiv-right-map-triangle
      ( section-f , retraction-f)
      ( (sh , is-section-sh) , retraction-h) =
        ( pair
          ( section-right-map-triangle f g h H section-f)
          ( retraction-left-map-triangle g f sh
            ( inv-htpy
              ( ( H ·r map-section h (sh , is-section-sh)) ∙h
                ( g ·l is-section-map-section h (sh , is-section-sh))))
            ( retraction-f)
            ( h , is-section-sh)))

If the left and right maps in a commuting triangle are equivalences, then the top map is an equivalence

module _
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
  (f : A → X) (g : B → X) (h : A → B) (H : f ~ g ∘ h)
  where

  section-is-equiv-top-map-triangle :
    is-equiv g → is-equiv f → section h
  section-is-equiv-top-map-triangle G F =
    section-left-map-triangle h
      ( map-retraction-is-equiv G)
      ( f)
      ( inv-htpy
        ( ( map-retraction g (retraction-is-equiv G) ·l H) ∙h
          ( is-retraction-map-retraction g (retraction-is-equiv G) ·r h)))
      ( section-is-equiv F)
      ( g , is-retraction-map-retraction-is-equiv G)

  map-section-is-equiv-top-map-triangle :
    is-equiv g → is-equiv f → B → A
  map-section-is-equiv-top-map-triangle G F =
    map-section h (section-is-equiv-top-map-triangle G F)

  abstract
    is-equiv-top-map-triangle :
      is-equiv g → is-equiv f → is-equiv h
    is-equiv-top-map-triangle
      ( section-g , (rg , is-retraction-rg))
      ( section-f , retraction-f) =
      ( pair
        ( section-left-map-triangle h rg f
          ( inv-htpy
            ( ( map-retraction g (rg , is-retraction-rg) ·l H) ∙h
              ( is-retraction-map-retraction g (rg , is-retraction-rg) ·r h)))
          ( section-f)
          ( g , is-retraction-rg))
        ( retraction-top-map-triangle f g h H retraction-f))

Composites of equivalences are equivalences

module _
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
  where

  abstract
    is-equiv-comp :
      (g : B → X) (h : A → B) → is-equiv h → is-equiv g → is-equiv (g ∘ h)
    pr1 (is-equiv-comp g h (sh , rh) (sg , rg)) = section-comp g h sh sg
    pr2 (is-equiv-comp g h (sh , rh) (sg , rg)) = retraction-comp g h rg rh

  equiv-comp : B ≃ X → A ≃ B → A ≃ X
  pr1 (equiv-comp g h) = map-equiv g ∘ map-equiv h
  pr2 (equiv-comp g h) = is-equiv-comp (pr1 g) (pr1 h) (pr2 h) (pr2 g)

  infixr 15 _∘e_
  _∘e_ : B ≃ X → A ≃ B → A ≃ X
  _∘e_ = equiv-comp

If a composite and its right factor are equivalences, then so is its left factor

module _
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
  where

  is-equiv-left-factor :
    (g : B → X) (h : A → B) →
    is-equiv (g ∘ h) → is-equiv h → is-equiv g
  is-equiv-left-factor g h is-equiv-gh is-equiv-h =
      is-equiv-right-map-triangle (g ∘ h) g h refl-htpy is-equiv-gh is-equiv-h

If a composite and its left factor are equivalences, then so is its right factor

module _
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
  where

  is-equiv-right-factor :
    (g : B → X) (h : A → B) →
    is-equiv g → is-equiv (g ∘ h) → is-equiv h
  is-equiv-right-factor g h is-equiv-g is-equiv-gh =
    is-equiv-top-map-triangle (g ∘ h) g h refl-htpy is-equiv-g is-equiv-gh

Equivalences are closed under homotopies

We show that if f ~ g, then f is an equivalence if and only if g is an equivalence. Furthermore, we show that if f and g are homotopic equivaleces, then their inverses are also homotopic.

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2}
  where

  abstract
    is-equiv-htpy :
      {f : A → B} (g : A → B) → f ~ g → is-equiv g → is-equiv f
    pr1 (pr1 (is-equiv-htpy g G ((h , H) , (k , K)))) = h
    pr2 (pr1 (is-equiv-htpy g G ((h , H) , (k , K)))) = (G ·r h) ∙h H
    pr1 (pr2 (is-equiv-htpy g G ((h , H) , (k , K)))) = k
    pr2 (pr2 (is-equiv-htpy g G ((h , H) , (k , K)))) = (k ·l G) ∙h K

  is-equiv-htpy-equiv : {f : A → B} (e : A ≃ B) → f ~ map-equiv e → is-equiv f
  is-equiv-htpy-equiv e H = is-equiv-htpy (map-equiv e) H (is-equiv-map-equiv e)

  abstract
    is-equiv-htpy' : (f : A → B) {g : A → B} → f ~ g → is-equiv f → is-equiv g
    is-equiv-htpy' f H = is-equiv-htpy f (inv-htpy H)

  is-equiv-htpy-equiv' : (e : A ≃ B) {g : A → B} → map-equiv e ~ g → is-equiv g
  is-equiv-htpy-equiv' e H =
    is-equiv-htpy' (map-equiv e) H (is-equiv-map-equiv e)

  htpy-map-inv-is-equiv :
    {f g : A → B} (H : f ~ g) (F : is-equiv f) (G : is-equiv g) →
    map-inv-is-equiv F ~ map-inv-is-equiv G
  htpy-map-inv-is-equiv H F G =
    htpy-map-inv-is-invertible H
      ( is-invertible-is-equiv F)
      ( is-invertible-is-equiv G)

Any retraction of an equivalence is an equivalence

abstract
  is-equiv-is-retraction :
    {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} {g : B → A} →
    is-equiv f → (g ∘ f) ~ id → is-equiv g
  is-equiv-is-retraction {A = A} {f = f} {g = g} is-equiv-f H =
    is-equiv-right-map-triangle id g f (inv-htpy H) is-equiv-id is-equiv-f

Any section of an equivalence is an equivalence

abstract
  is-equiv-is-section :
    {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} {g : B → A} →
    is-equiv f → f ∘ g ~ id → is-equiv g
  is-equiv-is-section {B = B} {f = f} {g = g} is-equiv-f H =
    is-equiv-top-map-triangle id f g (inv-htpy H) is-equiv-f is-equiv-id

If a section of f is an equivalence, then f is an equivalence

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B)
  where

  abstract
    is-equiv-is-equiv-section :
      (s : section f) → is-equiv (map-section f s) → is-equiv f
    is-equiv-is-equiv-section (g , G) S = is-equiv-is-retraction S G

If a retraction of f is an equivalence, then f is an equivalence

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B)
  where

  abstract
    is-equiv-is-equiv-retraction :
      (r : retraction f) → is-equiv (map-retraction f r) → is-equiv f
    is-equiv-is-equiv-retraction (g , G) R = is-equiv-is-section R G

Any section of an equivalence is homotopic to its inverse

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2} (e : A ≃ B)
  where

  htpy-map-inv-equiv-section :
    (f : section (map-equiv e)) → map-inv-equiv e ~ map-section (map-equiv e) f
  htpy-map-inv-equiv-section (f , H) =
    (map-inv-equiv e ·l inv-htpy H) ∙h (is-retraction-map-inv-equiv e ·r f)

Any retraction of an equivalence is homotopic to its inverse

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2} (e : A ≃ B)
  where

  htpy-map-inv-equiv-retraction :
    (f : retraction (map-equiv e)) →
    map-inv-equiv e ~ map-retraction (map-equiv e) f
  htpy-map-inv-equiv-retraction (f , H) =
    (inv-htpy H ·r map-inv-equiv e) ∙h (f ·l is-section-map-inv-equiv e)

Equivalences in commuting squares

is-equiv-equiv :
  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
  {f : A → B} {g : X → Y} (i : A ≃ X) (j : B ≃ Y)
  (H : (map-equiv j ∘ f) ~ (g ∘ map-equiv i)) → is-equiv g → is-equiv f
is-equiv-equiv {f = f} {g} i j H K =
  is-equiv-right-factor
    ( map-equiv j)
    ( f)
    ( is-equiv-map-equiv j)
    ( is-equiv-left-map-triangle
      ( map-equiv j ∘ f)
      ( g)
      ( map-equiv i)
      ( H)
      ( is-equiv-map-equiv i)
      ( K))

is-equiv-equiv' :
  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
  {f : A → B} {g : X → Y} (i : A ≃ X) (j : B ≃ Y)
  (H : (map-equiv j ∘ f) ~ (g ∘ map-equiv i)) → is-equiv f → is-equiv g
is-equiv-equiv' {f = f} {g} i j H K =
  is-equiv-left-factor
    ( g)
    ( map-equiv i)
    ( is-equiv-left-map-triangle
      ( g ∘ map-equiv i)
      ( map-equiv j)
      ( f)
      ( inv-htpy H)
      ( K)
      ( is-equiv-map-equiv j))
    ( is-equiv-map-equiv i)

We will assume a commuting square

        h
    A -----> C
    |        |
  f |        | g
    V        V
    B -----> D
        i

module _
  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4}
  (f : A → B) (g : C → D) (h : A → C) (i : B → D) (H : (i ∘ f) ~ (g ∘ h))
  where

  abstract
    is-equiv-top-is-equiv-left-square :
      is-equiv i → is-equiv f → is-equiv g → is-equiv h
    is-equiv-top-is-equiv-left-square Ei Ef Eg =
      is-equiv-top-map-triangle (i ∘ f) g h H Eg (is-equiv-comp i f Ef Ei)

  abstract
    is-equiv-top-is-equiv-bottom-square :
      is-equiv f → is-equiv g → is-equiv i → is-equiv h
    is-equiv-top-is-equiv-bottom-square Ef Eg Ei =
      is-equiv-top-map-triangle (i ∘ f) g h H Eg (is-equiv-comp i f Ef Ei)

  abstract
    is-equiv-bottom-is-equiv-top-square :
      is-equiv f → is-equiv g → is-equiv h → is-equiv i
    is-equiv-bottom-is-equiv-top-square Ef Eg Eh =
      is-equiv-left-factor i f
        ( is-equiv-left-map-triangle (i ∘ f) g h H Eh Eg)
        ( Ef)

  abstract
    is-equiv-left-is-equiv-right-square :
      is-equiv h → is-equiv i → is-equiv g → is-equiv f
    is-equiv-left-is-equiv-right-square Eh Ei Eg =
      is-equiv-right-factor i f Ei
        ( is-equiv-left-map-triangle (i ∘ f) g h H Eh Eg)

  abstract
    is-equiv-right-is-equiv-left-square :
      is-equiv h → is-equiv i → is-equiv f → is-equiv g
    is-equiv-right-is-equiv-left-square Eh Ei Ef =
      is-equiv-right-map-triangle (i ∘ f) g h H (is-equiv-comp i f Ef Ei) Eh

Equivalences are embeddings

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2}
  where

  abstract
    is-emb-is-equiv :
      {f : A → B} → is-equiv f → (x y : A) → is-equiv (ap f {x} {y})
    is-emb-is-equiv H x y =
      is-equiv-is-invertible'
        ( is-invertible-ap-is-coherently-invertible
          ( is-coherently-invertible-is-equiv H))

  equiv-ap :
    (e : A ≃ B) (x y : A) → (x ＝ y) ≃ (map-equiv e x ＝ map-equiv e y)
  pr1 (equiv-ap e x y) = ap (map-equiv e)
  pr2 (equiv-ap e x y) = is-emb-is-equiv (is-equiv-map-equiv e) x y

  map-inv-equiv-ap :
    (e : A ≃ B) (x y : A) → map-equiv e x ＝ map-equiv e y → x ＝ y
  map-inv-equiv-ap e x y = map-inv-equiv (equiv-ap e x y)

Equivalence reasoning

Equivalences can be constructed by equational reasoning in the following way:

equivalence-reasoning
  X ≃ Y by equiv-1
    ≃ Z by equiv-2
    ≃ V by equiv-3

The equivalence constructed in this way is equiv-1 ∘e (equiv-2 ∘e equiv-3), i.e., the equivivalence is associated fully to the right.

Note. In situations where it is important to have precise control over an equivalence or its inverse, it is often better to avoid making use of equivalence reasoning. For example, since many of the entries proving that a map is an equivalence are marked as abstract in agda-unimath, the inverse of an equivalence often does not compute to any map that one might expect the inverse to be. If inverses of equivalences are used in equivalence reasoning, this results in a composed equivalence that also does not compute to any expected underlying map.

Even if a proof by equivalence reasoning is clear to the human reader, constructing equivalences by hand by constructing maps back and forth and two homotopies witnessing that they are mutual inverses is often the most straigtforward solution that gives the best expected computational behavior of the constructed equivalence. In particular, if the underlying map or its inverse are noteworthy maps, it is good practice to define them directly rather than as underlying maps of equivalences constructed by equivalence reasoning.

infixl 1 equivalence-reasoning_
infixl 0 step-equivalence-reasoning

equivalence-reasoning_ :
  {l1 : Level} (X : UU l1) → X ≃ X
equivalence-reasoning X = id-equiv

step-equivalence-reasoning :
  {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} →
  (X ≃ Y) → (Z : UU l3) → (Y ≃ Z) → (X ≃ Z)
step-equivalence-reasoning e Z f = f ∘e e

syntax step-equivalence-reasoning e Z f = e ≃ Z by f

See also

  • For the notion of coherently invertible maps, also known as half-adjoint equivalences, see foundation.coherently-invertible-maps.
  • For the notion of maps with contractible fibers see foundation.contractible-maps.
  • For the notion of path-split maps see foundation.path-split-maps.
  • For the notion of finitely coherent equivalence, see [foundation.finitely-coherent-equivalence)(foundation.finitely-coherent-equivalence.md).
  • For the notion of finitely coherently invertible map, see [foundation.finitely-coherently-invertible-map)(foundation.finitely-coherently-invertible-map.md).
  • For the notion of infinitely coherent equivalence, see foundation.infinitely-coherent-equivalences.

Table of files about function types, composition, and equivalences

ConceptFile
Decidable dependent function typesfoundation.decidable-dependent-function-types
Dependent universal property of equivalencesfoundation.dependent-universal-property-equivalences
Descent for equivalencesfoundation.descent-equivalences
Equivalence extensionalityfoundation.equivalence-extensionality
Equivalence inductionfoundation.equivalence-induction
Equivalencesfoundation.equivalences
Equivalences (foundation-core)foundation-core.equivalences
Families of equivalencesfoundation.families-of-equivalences
Fibered equivalencesfoundation.fibered-equivalences
Function extensionalityfoundation.function-extensionality
Function typesfoundation.function-types
Function types (foundation-core)foundation-core.function-types
Functional correspondencesfoundation.functional-corresponcences
Functoriality of dependent function typesfoundation.functoriality-dependent-function-types
Functoriality of dependent function types (foundation-core)foundation-core.functoriality-dependent-function-types
Functoriality of function typesfoundation.functoriality-function-types
Implicit function typesfoundation.implicit-function-types
Iterating functionsfoundation.iterating-functions
Postcompositionfoundation.postcomposition
Precomposition of dependent functionsfoundation.precomposition-dependent-functions
Precomposition of dependent functions (foundation-core)foundation-core.precomposition-dependent-functions
Precomposition of functionsfoundation.precomposition-functions
Precomposition of functions (foundation-core)foundation-core.precomposition-functions
Precomposition of functions into subuniversesfoundation.precomposition-functions-into-subuniverses
Type arithmetic of dependent function typesfoundation.type-arithmetic-dependent-function-types
Univalence implies function extensionalityfoundation.univalence-implies-function-extensionality
Universal property of equivalencesfoundation.universal-property-equivalences
Weak function extensionalityfoundation.weak-function-extensionality

Recent changes