The fundamental theorem of identity types

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

Created on 2022-01-26.

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))