Large reflexive globular types
Content created by Fredrik Bakke and Vojtěch Štěpančík.
Created on 2024-03-20.
Last modified on 2024-06-16.
{-# OPTIONS --guardedness #-} module structured-types.large-reflexive-globular-types where
Imports
open import foundation.large-binary-relations open import foundation.universe-levels open import structured-types.large-globular-types open import structured-types.reflexive-globular-types
Idea
A large globular type is
reflexive¶
if every -cell x
comes with a choice of -cell from x
to x
.
Definition
Reflexivity structure on a large globular structure
record is-reflexive-large-globular-structure {α : Level → Level} {β : Level → Level → Level} {A : (l : Level) → UU (α l)} (G : large-globular-structure β A) : UUω where field is-reflexive-1-cell-is-reflexive-large-globular-structure : is-reflexive-Large-Relation A (1-cell-large-globular-structure G) is-reflexive-globular-structure-1-cell-is-reflexive-large-globular-structure : {l1 l2 : Level} (x : A l1) (y : A l2) → is-reflexive-globular-structure ( globular-structure-1-cell-large-globular-structure G x y) open is-reflexive-large-globular-structure public module _ {α : Level → Level} {β : Level → Level → Level} {A : (l : Level) → UU (α l)} {G : large-globular-structure β A} (r : is-reflexive-large-globular-structure G) where refl-1-cell-is-reflexive-large-globular-structure : {l : Level} {x : A l} → 1-cell-large-globular-structure G x x refl-1-cell-is-reflexive-large-globular-structure {x = x} = is-reflexive-1-cell-is-reflexive-large-globular-structure r x refl-2-cell-is-reflexive-large-globular-structure : {l1 l2 : Level} {x : A l1} {y : A l2} {f : 1-cell-large-globular-structure G x y} → 2-cell-large-globular-structure G f f refl-2-cell-is-reflexive-large-globular-structure {x = x} {y} {f} = is-reflexive-1-cell-is-reflexive-globular-structure ( is-reflexive-globular-structure-1-cell-is-reflexive-large-globular-structure ( r) ( x) ( y)) ( f) refl-3-cell-is-reflexive-large-globular-structure : {l1 l2 : Level} {x : A l1} {y : A l2} {f g : 1-cell-large-globular-structure G x y} → {H : 2-cell-large-globular-structure G f g} → 3-cell-large-globular-structure G H H refl-3-cell-is-reflexive-large-globular-structure {x = x} {y} = refl-2-cell-is-reflexive-globular-structure ( is-reflexive-globular-structure-1-cell-is-reflexive-large-globular-structure ( r) ( x) ( y))
Recent changes
- 2024-06-16. Fredrik Bakke and Vojtěch Štěpančík. Noncoherent wild higher precategories (#1099).
- 2024-03-20. Fredrik Bakke. Globular types (#1084).