Identity systems
Content created by Egbert Rijke, Fredrik Bakke, Jonathan Prieto-Cubides and Raymond Baker.
Created on 2022-01-26.
Last modified on 2024-01-31.
module foundation.identity-systems where
Imports
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.families-of-equivalences open import foundation-core.identity-types open import foundation-core.propositions 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 abstract is-identity-system-is-torsorial : (H : is-torsorial B) → is-identity-system B a b pr1 (is-identity-system-is-torsorial H P) p x y = tr ( fam-Σ P) ( eq-is-contr H) ( p) pr2 (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-torsorial-is-identity-system : is-identity-system B a b → is-torsorial 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) (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)
External links
- Identity systems at 1lab
- identity system at Lab
Recent changes
- 2024-01-31. Fredrik Bakke and Egbert Rijke. Transport-split and preunivalent type families (#1013).
- 2024-01-14. Fredrik Bakke. Exponentiating retracts of maps (#989).
- 2023-12-05. Raymond Baker and Egbert Rijke. Universal property of fibers (#944).
- 2023-11-24. Egbert Rijke. Refactor precomposition (#937).
- 2023-11-24. Fredrik Bakke. The orbit category of a group (#935).