This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

Identity systems

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

open import foundation-core.contractible-types
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.identity-types
open import foundation-core.propositions
open import foundation-core.retractions
open import foundation-core.sections
open import foundation-core.torsorial-type-families
open import foundation-core.transport-along-identifications

Idea

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.

Definitions

Evaluating at the base point

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 {a = a} b f = f a b

The predicate of being an identity system with respect to a universe level

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

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

The predicate of being an identity system

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

  is-identity-system : UUω
  is-identity-system = {l : Level} → is-identity-system-Level l B a b

Properties

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

  map-section-is-identity-system-is-torsorial :
    is-torsorial B →
    {l3 : Level} (P : (x : A) (y : B x) → UU l3) →
    P a b → (x : A) (y : B x) → P x y
  map-section-is-identity-system-is-torsorial H P p x y =
    tr (fam-Σ P) (eq-is-contr H) p

  is-section-map-section-is-identity-system-is-torsorial :
    (H : is-torsorial B) →
    {l3 : Level} (P : (x : A) (y : B x) → UU l3) →
    is-section
      ( ev-refl-identity-system b)
      ( map-section-is-identity-system-is-torsorial H P)
  is-section-map-section-is-identity-system-is-torsorial H P p =
    ap
      ( λ t → tr (fam-Σ P) t p)
      ( eq-is-contr'
        ( is-prop-is-contr H (a , b) (a , b))
        ( eq-is-contr H)
        ( refl))

  abstract
    is-identity-system-is-torsorial :
      is-torsorial B → is-identity-system B a b
    is-identity-system-is-torsorial H P =
      ( map-section-is-identity-system-is-torsorial H P ,
        is-section-map-section-is-identity-system-is-torsorial H P)

  abstract
    is-torsorial-is-identity-system :
      is-identity-system B a b → is-torsorial B
    pr1 (is-torsorial-is-identity-system H) = (a , b)
    pr2 (is-torsorial-is-identity-system H) (x , y) =
      pr1 (H (λ x' y' → (a , b) ＝ (x' , y'))) refl x y

  abstract
    fundamental-theorem-id-is-identity-system :
      is-identity-system B a b →
      (f : (x : A) → a ＝ x → B x) → is-fiberwise-equiv f
    fundamental-theorem-id-is-identity-system H =
      fundamental-theorem-id (is-torsorial-is-identity-system H)