Identity systems

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

Created on 2022-01-26.
Last modified on 2023-09-12.

module foundation.identity-systems where
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.fundamental-theorem-of-identity-types
open import foundation.universe-levels

open import foundation-core.contractible-types
open import foundation-core.equivalences
open import foundation-core.identity-types
open import foundation-core.sections
open import foundation-core.transport-along-identifications


A (unary) identity system on a type A equipped with a point a : A consists of a type family B over A equipped with a point b : B a that satisfies an induction principle analogous to the induction principle of the identity type at a. The dependent universal property of identity types also follows for identity systems.


The predicate of being an identity system

ev-refl-identity-system :
  {l1 l2 l3 : Level} {A : UU l1} {B : A  UU l2} {a : A} (b : B a)
  {P : (x : A) (y : B x)  UU l3} 
  ((x : A) (y : B x)  P x y)  P a b
ev-refl-identity-system b f = f _ b

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

  is-identity-system : UU (l1  l2  lsuc l)
  is-identity-system =
    (P : (x : A) (y : B x)  UU l)  section (ev-refl-identity-system b {P})


A type family over A is an identity system if and only if its total space is contractible

In foundation.torsorial-type-families we will start calling type families with contractible total space torsorial.

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

    is-identity-system-is-torsorial :
      (H : is-contr (Σ A B)) 
      {l : Level}  is-identity-system l B a b
    pr1 (is-identity-system-is-torsorial H P) p x y =
        ( fam-Σ P)
        ( eq-is-contr H)
        ( p)
    pr2 (is-identity-system-is-torsorial H P) p =
        ( λ t  tr (fam-Σ P) t p)
        ( eq-is-contr'
          ( is-prop-is-contr H (pair a b) (pair a b))
          ( eq-is-contr H)
          ( refl))

    is-torsorial-is-identity-system :
      ({l : Level}  is-identity-system l B a b)  is-contr (Σ A B)
    pr1 (pr1 (is-torsorial-is-identity-system H)) = a
    pr2 (pr1 (is-torsorial-is-identity-system H)) = b
    pr2 (is-torsorial-is-identity-system H) (pair x y) =
      pr1 (H  x' y'  (pair a b)  (pair x' y'))) refl x y

    fundamental-theorem-id-is-identity-system :
      ({l : Level}  is-identity-system l B a b) 
      (f : (x : A)  a  x  B x)  (x : A)  is-equiv (f x)
    fundamental-theorem-id-is-identity-system H f =
        ( is-torsorial-is-identity-system H)
        ( f)

Recent changes