The fundamental theorem of identity types

Content created by Egbert Rijke, Fredrik Bakke, Jonathan Prieto-Cubides and Raymond Baker.

Created on 2022-01-26.
Last modified on 2024-04-17.

module foundation.fundamental-theorem-of-identity-types where
Imports 
open import foundation.dependent-pair-types
open import foundation.universe-levels

open import foundation-core.contractible-types
open import foundation-core.equivalences
open import foundation-core.families-of-equivalences
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.retractions
open import foundation-core.retracts-of-types
open import foundation-core.sections
open import foundation-core.torsorial-type-families

Idea

The fundamental theorem of identity types provides a way to characterize identity types. It uses the fact that a family of maps f : (x : A) → a ＝ x → B x is a family of equivalences if and only if it induces an equivalence Σ A (Id a) → Σ A B on total spaces. Note that the total space Σ A (Id a) is contractible. Therefore, any map Σ A (Id a) → Σ A B is an equivalence if and only if Σ A B is contractible. Type families B of which the total space Σ A B is contractible are also called torsorial. The statement of the fundamental theorem of identity types is therefore:

Fundamental theorem of identity types. Consider a type family B over a type A, and consider an element a : A. Then the following are logically equivalent:

  1. Any family of maps f : (x : A) → a ＝ x → B x is a family of equivalences.
  2. The type family B is torsorial.

Theorem

The fundamental theorem of identity types

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

  abstract
    fundamental-theorem-id :
      is-torsorial B → (f : (x : A) → a ＝ x → B x) → is-fiberwise-equiv f
    fundamental-theorem-id is-contr-AB f =
      is-fiberwise-equiv-is-equiv-tot
        ( is-equiv-is-contr (tot f) (is-torsorial-Id a) is-contr-AB)

  abstract
    fundamental-theorem-id' :
      (f : (x : A) → a ＝ x → B x) → is-fiberwise-equiv f → is-torsorial B
    fundamental-theorem-id' f is-fiberwise-equiv-f =
      is-contr-is-equiv'
        ( Σ A (Id a))
        ( tot f)
        ( is-equiv-tot-is-fiberwise-equiv is-fiberwise-equiv-f)
        ( is-torsorial-Id a)

Corollaries

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

  abstract
    fundamental-theorem-id-J :
      is-torsorial B → is-fiberwise-equiv (ind-Id a (λ x p → B x) b)
    fundamental-theorem-id-J is-contr-AB =
      fundamental-theorem-id is-contr-AB (ind-Id a (λ x p → B x) b)

  abstract
    fundamental-theorem-id-J' :
      is-fiberwise-equiv (ind-Id a (λ x p → B x) b) → is-torsorial B
    fundamental-theorem-id-J' H =
      is-contr-is-equiv'
        ( Σ A (Id a))
        ( tot (ind-Id a (λ x p → B x) b))
        ( is-equiv-tot-is-fiberwise-equiv H)
        ( is-torsorial-Id a)

Retracts of the identity type are equivalent to the identity type

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

  abstract
    fundamental-theorem-id-retraction :
      (i : (x : A) → B x → a ＝ x) →
      ((x : A) → retraction (i x)) →
      is-fiberwise-equiv i
    fundamental-theorem-id-retraction i R =
      is-fiberwise-equiv-is-equiv-tot
        ( is-equiv-is-contr (tot i)
          ( is-contr-retract-of
            ( Σ _ (λ y → a ＝ y))
            ( ( tot i) ,
              ( tot (λ x → pr1 (R x))) ,
              ( ( inv-htpy (preserves-comp-tot i (pr1 ∘ R))) ∙h
                ( tot-htpy (pr2 ∘ R)) ∙h
                ( tot-id B)))
            ( is-torsorial-Id a))
          ( is-torsorial-Id a))

    fundamental-theorem-id-retract :
      (R : (x : A) → (B x) retract-of (a ＝ x)) →
      is-fiberwise-equiv (inclusion-retract ∘ R)
    fundamental-theorem-id-retract R =
      fundamental-theorem-id-retraction
        ( inclusion-retract ∘ R)
        ( retraction-retract ∘ R)

The fundamental theorem of identity types, using sections

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

  abstract
    fundamental-theorem-id-section :
      (f : (x : A) → a ＝ x → B x) →
      ((x : A) → section (f x)) →
      is-fiberwise-equiv f
    fundamental-theorem-id-section f section-f x =
      is-equiv-is-equiv-section
        ( f x)
        ( section-f x)
        ( fundamental-theorem-id-retraction
          ( a)
          ( λ x → map-section (f x) (section-f x))
          ( λ x → (f x , is-section-map-section (f x) (section-f x)))
          ( x))

See also

Recent changes