Equivalences

Content created by Egbert Rijke, Fredrik Bakke, Jonathan Prieto-Cubides, Vojtěch Štěpančík, Elisabeth Stenholm, Eléonore Mangel, Raymond Baker and maybemabeline.

Created on 2022-01-26.
Last modified on 2024-06-05.

module foundation.equivalences where

open import foundation-core.equivalences public
Imports
open import foundation.action-on-identifications-functions
open import foundation.cones-over-cospan-diagrams
open import foundation.dependent-pair-types
open import foundation.equivalence-extensionality
open import foundation.function-extensionality
open import foundation.functoriality-fibers-of-maps
open import foundation.logical-equivalences
open import foundation.transport-along-identifications
open import foundation.transposition-identifications-along-equivalences
open import foundation.truncated-maps
open import foundation.universal-property-equivalences
open import foundation.universe-levels

open import foundation-core.commuting-triangles-of-maps
open import foundation-core.contractible-maps
open import foundation-core.contractible-types
open import foundation-core.embeddings
open import foundation-core.fibers-of-maps
open import foundation-core.function-types
open import foundation-core.functoriality-dependent-pair-types
open import foundation-core.homotopies
open import foundation-core.identity-types
open import foundation-core.injective-maps
open import foundation-core.propositions
open import foundation-core.pullbacks
open import foundation-core.retractions
open import foundation-core.retracts-of-types
open import foundation-core.sections
open import foundation-core.subtypes
open import foundation-core.truncation-levels
open import foundation-core.type-theoretic-principle-of-choice

Properties

Any equivalence is an embedding

We already proved in foundation-core.equivalences that equivalences are embeddings. Here we have _↪_ available, so we record the map from equivalences to embeddings.

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

  is-emb-equiv : (e : A  B)  is-emb (map-equiv e)
  is-emb-equiv e = is-emb-is-equiv (is-equiv-map-equiv e)

  emb-equiv : (A  B)  (A  B)
  pr1 (emb-equiv e) = map-equiv e
  pr2 (emb-equiv e) = is-emb-equiv e

Equivalences have a contractible type of sections

Proof: Since equivalences are contractible maps, and products of contractible types are contractible, it follows that the type

  (b : B) → fiber f b

is contractible, for any equivalence f. However, by the type theoretic principle of choice it follows that this type is equivalent to the type

  Σ (B → A) (λ g → (b : B) → f (g b) = b),

which is the type of sections of f.

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

  abstract
    is-contr-section-is-equiv : {f : A  B}  is-equiv f  is-contr (section f)
    is-contr-section-is-equiv {f} is-equiv-f =
      is-contr-equiv'
        ( (b : B)  fiber f b)
        ( distributive-Π-Σ)
        ( is-contr-Π (is-contr-map-is-equiv is-equiv-f))

Equivalences have a contractible type of retractions

Proof: Since precomposing by an equivalence is an equivalence, and equivalences are contractible maps, it follows that the fiber of the map

  (B → A) → (A → A)

at id : A → A is contractible, i.e., the type Σ (B → A) (λ h → h ∘ f = id) is contractible. Furthermore, since fiberwise equivalences induce equivalences on total spaces, it follows from function extensionality` that the type

  Σ (B → A) (λ h → h ∘ f ~ id)

is contractible. In other words, the type of retractions of an equivalence is contractible.

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

  abstract
    is-contr-retraction-is-equiv :
      {f : A  B}  is-equiv f  is-contr (retraction f)
    is-contr-retraction-is-equiv {f} is-equiv-f =
      is-contr-equiv'
        ( Σ (B  A)  h  h  f  id))
        ( equiv-tot  h  equiv-funext))
        ( is-contr-map-is-equiv (is-equiv-precomp-is-equiv f is-equiv-f A) id)

The underlying retract of an equivalence

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

  retract-equiv : A  B  A retract-of B
  retract-equiv e =
    ( map-equiv e , map-inv-equiv e , is-retraction-map-inv-equiv e)

  retract-inv-equiv : B  A  A retract-of B
  retract-inv-equiv = retract-equiv  inv-equiv

Being an equivalence is a property

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

  is-contr-is-equiv-is-equiv : {f : A  B}  is-equiv f  is-contr (is-equiv f)
  is-contr-is-equiv-is-equiv is-equiv-f =
    is-contr-product
      ( is-contr-section-is-equiv is-equiv-f)
      ( is-contr-retraction-is-equiv is-equiv-f)

  abstract
    is-property-is-equiv : (f : A  B)  (H K : is-equiv f)  is-contr (H  K)
    is-property-is-equiv f H =
      is-prop-is-contr (is-contr-is-equiv-is-equiv H) H

  is-equiv-Prop : (f : A  B)  Prop (l1  l2)
  pr1 (is-equiv-Prop f) = is-equiv f
  pr2 (is-equiv-Prop f) = is-property-is-equiv f

  eq-equiv-eq-map-equiv :
    {e e' : A  B}  (map-equiv e)  (map-equiv e')  e  e'
  eq-equiv-eq-map-equiv = eq-type-subtype is-equiv-Prop

  abstract
    is-emb-map-equiv :
      is-emb (map-equiv {A = A} {B = B})
    is-emb-map-equiv = is-emb-inclusion-subtype is-equiv-Prop

  is-injective-map-equiv :
    is-injective (map-equiv {A = A} {B = B})
  is-injective-map-equiv = is-injective-is-emb is-emb-map-equiv

  emb-map-equiv : (A  B)  (A  B)
  pr1 emb-map-equiv = map-equiv
  pr2 emb-map-equiv = is-emb-map-equiv

The 3-for-2 property of being an equivalence

If the right factor is an equivalence, then the left factor being an equivalence is equivalent to the composite being one

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

  equiv-is-equiv-right-map-triangle :
    { f : A  B} (e : B  C) (h : A  C)
    ( H : coherence-triangle-maps h (map-equiv e) f) 
    is-equiv f  is-equiv h
  equiv-is-equiv-right-map-triangle {f} e h H =
    equiv-iff-is-prop
      ( is-property-is-equiv f)
      ( is-property-is-equiv h)
      ( λ is-equiv-f 
        is-equiv-left-map-triangle h (map-equiv e) f H is-equiv-f
          ( is-equiv-map-equiv e))
      ( is-equiv-top-map-triangle h (map-equiv e) f H (is-equiv-map-equiv e))

  equiv-is-equiv-left-factor :
    { f : A  B} (e : B  C) 
    is-equiv f  is-equiv (map-equiv e  f)
  equiv-is-equiv-left-factor {f} e =
    equiv-is-equiv-right-map-triangle e (map-equiv e  f) refl-htpy

If the left factor is an equivalence, then the right factor being an equivalence is equivalent to the composite being one

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

  equiv-is-equiv-top-map-triangle :
    ( e : A  B) {f : B  C} (h : A  C)
    ( H : coherence-triangle-maps h f (map-equiv e)) 
    is-equiv f  is-equiv h
  equiv-is-equiv-top-map-triangle e {f} h H =
    equiv-iff-is-prop
      ( is-property-is-equiv f)
      ( is-property-is-equiv h)
      ( is-equiv-left-map-triangle h f (map-equiv e) H (is-equiv-map-equiv e))
      ( λ is-equiv-h 
        is-equiv-right-map-triangle h f
          ( map-equiv e)
          ( H)
          ( is-equiv-h)
          ( is-equiv-map-equiv e))

  equiv-is-equiv-right-factor :
    ( e : A  B) {f : B  C} 
    is-equiv f  is-equiv (f  map-equiv e)
  equiv-is-equiv-right-factor e {f} =
    equiv-is-equiv-top-map-triangle e (f  map-equiv e) refl-htpy

The 6-for-2 property of equivalences

Consider a commuting diagram of maps

         i
    A ------> X
    |       ∧ |
  f |     /   | g
    |   h     |
    ∨ /       ∨
    B ------> Y.
         j

The 6-for-2 property of equivalences asserts that if i and j are equivalences, then so are h, f, g, and the triple composite g ∘ h ∘ f. The 6-for-2 property is also commonly known as the 2-out-of-6 property.

First proof: Since i is an equivalence, it follows that i is surjective. This implies that h is surjective. Furthermore, since j is an equivalence it follows that j is an embedding. This implies that h is an embedding. The map h is therefore both surjective and an embedding, so it must be an equivalence. The fact that f and g are equivalences now follows from a simple application of the 3-for-2 property of equivalences.

Unfortunately, the above proof requires us to import surjective-maps, which causes a cyclic module dependency. We therefore give a second proof, which avoids the fact that maps that are both surjective and an embedding are equivalences.

Second proof: By reasoning similar to that in the first proof, it suffices to show that the diagonal filler h is an equivalence. The map f ∘ i⁻¹ is a section of h, since we have (h ∘ f ~ i) → (h ∘ f ∘ i⁻¹ ~ id) by transposing along equivalences. Similarly, the map j⁻¹ ∘ g is a retraction of h, since we have (g ∘ h ~ j) → (j⁻¹ ∘ g ∘ h ~ id) by transposing along equivalences. Since h therefore has a section and a retraction, it is an equivalence.

In fact, the above argument shows that if the top map i has a section and the bottom map j has a retraction, then the diagonal filler, and hence all other maps are equivalences.

module _
  {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 : B  X)
  (u : coherence-triangle-maps i h f) (v : coherence-triangle-maps j g h)
  where

  section-diagonal-filler-section-top-square :
    section i  section h
  section-diagonal-filler-section-top-square =
    section-right-map-triangle i h f u

  section-diagonal-filler-is-equiv-top-is-equiv-bottom-square :
    is-equiv i  section h
  section-diagonal-filler-is-equiv-top-is-equiv-bottom-square H =
    section-diagonal-filler-section-top-square (section-is-equiv H)

  map-section-diagonal-filler-is-equiv-top-is-equiv-bottom-square :
    is-equiv i  X  B
  map-section-diagonal-filler-is-equiv-top-is-equiv-bottom-square H =
    map-section h
      ( section-diagonal-filler-is-equiv-top-is-equiv-bottom-square H)

  is-section-section-diagonal-filler-is-equiv-top-is-equiv-bottom-square :
    (H : is-equiv i) 
    is-section h
      ( map-section-diagonal-filler-is-equiv-top-is-equiv-bottom-square H)
  is-section-section-diagonal-filler-is-equiv-top-is-equiv-bottom-square H =
    is-section-map-section h
      ( section-diagonal-filler-is-equiv-top-is-equiv-bottom-square H)

  retraction-diagonal-filler-retraction-bottom-square :
    retraction j  retraction h
  retraction-diagonal-filler-retraction-bottom-square =
    retraction-top-map-triangle j g h v

  retraction-diagonal-filler-is-equiv-top-is-equiv-bottom-square :
    is-equiv j  retraction h
  retraction-diagonal-filler-is-equiv-top-is-equiv-bottom-square K =
    retraction-diagonal-filler-retraction-bottom-square (retraction-is-equiv K)

  map-retraction-diagonal-filler-is-equiv-top-is-equiv-bottom-square :
    is-equiv j  X  B
  map-retraction-diagonal-filler-is-equiv-top-is-equiv-bottom-square K =
    map-retraction h
      ( retraction-diagonal-filler-is-equiv-top-is-equiv-bottom-square K)

  is-retraction-retraction-diagonal-fller-is-equiv-top-is-equiv-bottom-square :
    (K : is-equiv j) 
    is-retraction h
      ( map-retraction-diagonal-filler-is-equiv-top-is-equiv-bottom-square K)
  is-retraction-retraction-diagonal-fller-is-equiv-top-is-equiv-bottom-square
    K =
    is-retraction-map-retraction h
      ( retraction-diagonal-filler-is-equiv-top-is-equiv-bottom-square K)

  is-equiv-diagonal-filler-section-top-retraction-bottom-square :
    section i  retraction j  is-equiv h
  pr1 (is-equiv-diagonal-filler-section-top-retraction-bottom-square H K) =
    section-diagonal-filler-section-top-square H
  pr2 (is-equiv-diagonal-filler-section-top-retraction-bottom-square H K) =
    retraction-diagonal-filler-retraction-bottom-square K

  is-equiv-diagonal-filler-is-equiv-top-is-equiv-bottom-square :
    is-equiv i  is-equiv j  is-equiv h
  is-equiv-diagonal-filler-is-equiv-top-is-equiv-bottom-square H K =
    is-equiv-diagonal-filler-section-top-retraction-bottom-square
      ( section-is-equiv H)
      ( retraction-is-equiv K)

  is-equiv-left-is-equiv-top-is-equiv-bottom-square :
    is-equiv i  is-equiv j  is-equiv f
  is-equiv-left-is-equiv-top-is-equiv-bottom-square H K =
    is-equiv-top-map-triangle i h f u
      ( is-equiv-diagonal-filler-is-equiv-top-is-equiv-bottom-square H K)
      ( H)

  is-equiv-right-is-equiv-top-is-equiv-bottom-square :
    is-equiv i  is-equiv j  is-equiv g
  is-equiv-right-is-equiv-top-is-equiv-bottom-square H K =
    is-equiv-right-map-triangle j g h v K
      ( is-equiv-diagonal-filler-is-equiv-top-is-equiv-bottom-square H K)

  is-equiv-triple-comp :
    is-equiv i  is-equiv j  is-equiv (g  h  f)
  is-equiv-triple-comp H K =
    is-equiv-comp g
      ( h  f)
      ( is-equiv-comp h f
        ( is-equiv-left-is-equiv-top-is-equiv-bottom-square H K)
        ( is-equiv-diagonal-filler-is-equiv-top-is-equiv-bottom-square H K))
      ( is-equiv-right-is-equiv-top-is-equiv-bottom-square H K)

Being an equivalence is closed under homotopies

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

  equiv-is-equiv-htpy :
    { f g : A  B}  (f ~ g) 
    is-equiv f  is-equiv g
  equiv-is-equiv-htpy {f} {g} H =
    equiv-iff-is-prop
      ( is-property-is-equiv f)
      ( is-property-is-equiv g)
      ( is-equiv-htpy f (inv-htpy H))
      ( is-equiv-htpy g H)

The groupoid laws for equivalences

Composition of equivalences is associative

associative-comp-equiv :
  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4} 
  (e : A  B) (f : B  C) (g : C  D) 
  ((g ∘e f) ∘e e)  (g ∘e (f ∘e e))
associative-comp-equiv e f g = eq-equiv-eq-map-equiv refl

Unit laws for composition of equivalences

module _
  {l1 l2 : Level} {X : UU l1} {Y : UU l2}
  where

  left-unit-law-equiv : (e : X  Y)  (id-equiv ∘e e)  e
  left-unit-law-equiv e = eq-equiv-eq-map-equiv refl

  right-unit-law-equiv : (e : X  Y)  (e ∘e id-equiv)  e
  right-unit-law-equiv e = eq-equiv-eq-map-equiv refl

A coherence law for the unit laws for composition of equivalences

coh-unit-laws-equiv :
  {l : Level} {X : UU l} 
  left-unit-law-equiv (id-equiv {A = X}) 
  right-unit-law-equiv (id-equiv {A = X})
coh-unit-laws-equiv = ap eq-equiv-eq-map-equiv refl

Inverse laws for composition of equivalences

module _
  {l1 l2 : Level} {X : UU l1} {Y : UU l2}
  where

  left-inverse-law-equiv : (e : X  Y)  ((inv-equiv e) ∘e e)  id-equiv
  left-inverse-law-equiv e =
    eq-htpy-equiv (is-retraction-map-inv-is-equiv (is-equiv-map-equiv e))

  right-inverse-law-equiv : (e : X  Y)  (e ∘e (inv-equiv e))  id-equiv
  right-inverse-law-equiv e =
    eq-htpy-equiv (is-section-map-inv-is-equiv (is-equiv-map-equiv e))

inv-equiv is a fibered involution on equivalences

module _
  {l1 l2 : Level} {X : UU l1} {Y : UU l2}
  where

  inv-inv-equiv : (e : X  Y)  (inv-equiv (inv-equiv e))  e
  inv-inv-equiv e = eq-equiv-eq-map-equiv refl

  inv-inv-equiv' : (e : Y  X)  (inv-equiv (inv-equiv e))  e
  inv-inv-equiv' e = eq-equiv-eq-map-equiv refl

  is-equiv-inv-equiv : is-equiv (inv-equiv {A = X} {B = Y})
  is-equiv-inv-equiv =
    is-equiv-is-invertible
      ( inv-equiv)
      ( inv-inv-equiv')
      ( inv-inv-equiv)

  equiv-inv-equiv : (X  Y)  (Y  X)
  pr1 equiv-inv-equiv = inv-equiv
  pr2 equiv-inv-equiv = is-equiv-inv-equiv

Taking the inverse equivalence distributes over composition

module _
  {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} {Z : UU l3}
  where

  distributive-inv-comp-equiv :
    (e : X  Y) (f : Y  Z) 
    (inv-equiv (f ∘e e))  ((inv-equiv e) ∘e (inv-equiv f))
  distributive-inv-comp-equiv e f =
    eq-htpy-equiv
      ( λ x 
        map-eq-transpose-equiv-inv
          ( f ∘e e)
          ( ( ap  g  map-equiv g x) (inv (right-inverse-law-equiv f))) 
            ( ap
              ( λ g  map-equiv (f ∘e (g ∘e (inv-equiv f))) x)
              ( inv (right-inverse-law-equiv e)))))

  distributive-map-inv-comp-equiv :
    (e : X  Y) (f : Y  Z) 
    map-inv-equiv (f ∘e e)  map-inv-equiv e  map-inv-equiv f
  distributive-map-inv-comp-equiv e f =
    ap map-equiv (distributive-inv-comp-equiv e f)

Postcomposition of equivalences by an equivalence is an equivalence

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

  is-retraction-postcomp-equiv-inv-equiv :
    (f : B  C) (e : A  B)  inv-equiv f ∘e (f ∘e e)  e
  is-retraction-postcomp-equiv-inv-equiv f e =
    eq-htpy-equiv  x  is-retraction-map-inv-equiv f (map-equiv e x))

  is-section-postcomp-equiv-inv-equiv :
    (f : B  C) (e : A  C)  f ∘e (inv-equiv f ∘e e)  e
  is-section-postcomp-equiv-inv-equiv f e =
    eq-htpy-equiv  x  is-section-map-inv-equiv f (map-equiv e x))

  is-equiv-postcomp-equiv-equiv :
    (f : B  C)  is-equiv  (e : A  B)  f ∘e e)
  is-equiv-postcomp-equiv-equiv f =
    is-equiv-is-invertible
      ( inv-equiv f ∘e_)
      ( is-section-postcomp-equiv-inv-equiv f)
      ( is-retraction-postcomp-equiv-inv-equiv f)

equiv-postcomp-equiv :
  {l1 l2 l3 : Level} {B : UU l2} {C : UU l3} 
  (f : B  C)  (A : UU l1)  (A  B)  (A  C)
pr1 (equiv-postcomp-equiv f A) = f ∘e_
pr2 (equiv-postcomp-equiv f A) = is-equiv-postcomp-equiv-equiv f

Precomposition of equivalences by an equivalence is an equivalence

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

  is-retraction-precomp-equiv-inv-equiv :
    (e : A  B) (f : B  C)  (f ∘e e) ∘e inv-equiv e  f
  is-retraction-precomp-equiv-inv-equiv e f =
    eq-htpy-equiv  x  ap (map-equiv f) (is-section-map-inv-equiv e x))

  is-section-precomp-equiv-inv-equiv :
    (e : A  B) (f : A  C)  (f ∘e inv-equiv e) ∘e e  f
  is-section-precomp-equiv-inv-equiv e f =
    eq-htpy-equiv  x  ap (map-equiv f) (is-retraction-map-inv-equiv e x))

  is-equiv-precomp-equiv-equiv :
    (e : A  B)  is-equiv  (f : B  C)  f ∘e e)
  is-equiv-precomp-equiv-equiv e =
    is-equiv-is-invertible
      ( _∘e inv-equiv e)
      ( is-section-precomp-equiv-inv-equiv e)
      ( is-retraction-precomp-equiv-inv-equiv e)

equiv-precomp-equiv :
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} 
  (A  B)  (C : UU l3)  (B  C)  (A  C)
pr1 (equiv-precomp-equiv e C) = _∘e e
pr2 (equiv-precomp-equiv e C) = is-equiv-precomp-equiv-equiv e

Computing transport in the type of equivalences

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

  tr-equiv-type :
    {x y : A} (p : x  y) (e : B x  C x) 
    tr  x  B x  C x) p e  equiv-tr C p ∘e e ∘e equiv-tr B (inv p)
  tr-equiv-type refl e = eq-htpy-equiv refl-htpy

A cospan in which one of the legs is an equivalence is a pullback if and only if the corresponding map on the cone is an equivalence

module _
  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3}
  {X : UU l4} (f : A  X) (g : B  X) (c : cone f g C)
  where

  abstract
    is-equiv-vertical-map-is-pullback :
      is-equiv g  is-pullback f g c  is-equiv (vertical-map-cone f g c)
    is-equiv-vertical-map-is-pullback is-equiv-g pb =
      is-equiv-is-contr-map
        ( is-trunc-vertical-map-is-pullback neg-two-𝕋 f g c pb
          ( is-contr-map-is-equiv is-equiv-g))

  abstract
    is-pullback-is-equiv-vertical-maps :
      is-equiv g  is-equiv (vertical-map-cone f g c)  is-pullback f g c
    is-pullback-is-equiv-vertical-maps is-equiv-g is-equiv-p =
      is-pullback-is-fiberwise-equiv-map-fiber-vertical-map-cone f g c
        ( λ a 
          is-equiv-is-contr
            ( map-fiber-vertical-map-cone f g c a)
            ( is-contr-map-is-equiv is-equiv-p a)
            ( is-contr-map-is-equiv is-equiv-g (f a)))

module _
  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3}
  {X : UU l4} (f : A  X) (g : B  X) (c : cone f g C)
  where

  abstract
    is-equiv-horizontal-map-is-pullback :
      is-equiv f  is-pullback f g c  is-equiv (horizontal-map-cone f g c)
    is-equiv-horizontal-map-is-pullback is-equiv-f pb =
      is-equiv-is-contr-map
        ( is-trunc-horizontal-map-is-pullback neg-two-𝕋 f g c pb
          ( is-contr-map-is-equiv is-equiv-f))

  abstract
    is-pullback-is-equiv-horizontal-maps :
      is-equiv f  is-equiv (horizontal-map-cone f g c)  is-pullback f g c
    is-pullback-is-equiv-horizontal-maps is-equiv-f is-equiv-q =
      is-pullback-swap-cone' f g c
        ( is-pullback-is-equiv-vertical-maps g f
          ( swap-cone f g c)
          ( is-equiv-f)
          ( is-equiv-q))

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