# Identity systems

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

Created on 2022-01-26.

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)