Reflexive globular types
Content created by Fredrik Bakke, Egbert Rijke and Vojtěch Štěpančík.
Created on 2024-03-20.
Last modified on 2024-09-03.
{-# OPTIONS --guardedness #-} module structured-types.reflexive-globular-types where
Imports
open import foundation.binary-relations open import foundation.dependent-pair-types open import foundation.identity-types open import foundation.universe-levels open import structured-types.globular-types
Idea
A globular type is
reflexive¶
if every -cell x
comes with a choice of -cell from x
to x
.
Definition
Reflexivity structure on a globular structure
record is-reflexive-globular-structure {l1 l2 : Level} {A : UU l1} (G : globular-structure l2 A) : UU (l1 ⊔ l2) where coinductive field is-reflexive-1-cell-is-reflexive-globular-structure : is-reflexive (1-cell-globular-structure G) is-reflexive-globular-structure-1-cell-is-reflexive-globular-structure : (x y : A) → is-reflexive-globular-structure ( globular-structure-1-cell-globular-structure G x y) open is-reflexive-globular-structure public module _ {l1 l2 : Level} {A : UU l1} {G : globular-structure l2 A} (r : is-reflexive-globular-structure G) where refl-1-cell-is-reflexive-globular-structure : {x : A} → 1-cell-globular-structure G x x refl-1-cell-is-reflexive-globular-structure {x} = is-reflexive-1-cell-is-reflexive-globular-structure r x refl-2-cell-is-reflexive-globular-structure : {x y : A} {f : 1-cell-globular-structure G x y} → 2-cell-globular-structure G f f refl-2-cell-is-reflexive-globular-structure {x} {y} {f} = is-reflexive-1-cell-is-reflexive-globular-structure ( is-reflexive-globular-structure-1-cell-is-reflexive-globular-structure ( r) ( x) ( y)) ( f) is-reflexive-globular-structure-2-cell-is-reflexive-globular-structure : {x y : A} (f g : 1-cell-globular-structure G x y) → is-reflexive-globular-structure ( globular-structure-2-cell-globular-structure G f g) is-reflexive-globular-structure-2-cell-is-reflexive-globular-structure { x} {y} = is-reflexive-globular-structure-1-cell-is-reflexive-globular-structure ( is-reflexive-globular-structure-1-cell-is-reflexive-globular-structure ( r) ( x) ( y)) refl-3-cell-is-reflexive-globular-structure : {x y : A} {f g : 1-cell-globular-structure G x y} {H : 2-cell-globular-structure G f g} → 3-cell-globular-structure G H H refl-3-cell-is-reflexive-globular-structure {x} {y} {f} {g} {H} = is-reflexive-1-cell-is-reflexive-globular-structure ( is-reflexive-globular-structure-2-cell-is-reflexive-globular-structure ( f) ( g)) ( H)
The type of reflexive globular structures
reflexive-globular-structure : {l1 : Level} (l2 : Level) (A : UU l1) → UU (l1 ⊔ lsuc l2) reflexive-globular-structure l2 A = Σ (globular-structure l2 A) (is-reflexive-globular-structure)
Reflexivity structure on a globular type
module _ {l1 l2 : Level} (G : Globular-Type l1 l2) where is-reflexive-Globular-Type : UU (l1 ⊔ l2) is-reflexive-Globular-Type = is-reflexive-globular-structure (globular-structure-0-cell-Globular-Type G)
Reflexive globular types
record Reflexive-Globular-Type (l1 l2 : Level) : UU (lsuc l1 ⊔ lsuc l2) where field globular-type-Reflexive-Globular-Type : Globular-Type l1 l2 0-cell-Reflexive-Globular-Type : UU l1 0-cell-Reflexive-Globular-Type = 0-cell-Globular-Type globular-type-Reflexive-Globular-Type 1-cell-Reflexive-Globular-Type : 0-cell-Reflexive-Globular-Type → 0-cell-Reflexive-Globular-Type → UU l2 1-cell-Reflexive-Globular-Type = 1-cell-Globular-Type globular-type-Reflexive-Globular-Type 2-cell-Reflexive-Globular-Type : {x x' : 0-cell-Reflexive-Globular-Type} (y y' : 1-cell-Reflexive-Globular-Type x x') → UU l2 2-cell-Reflexive-Globular-Type = 2-cell-Globular-Type globular-type-Reflexive-Globular-Type globular-structure-Reflexive-Globular-Type : globular-structure l2 0-cell-Reflexive-Globular-Type globular-structure-Reflexive-Globular-Type = globular-structure-0-cell-Globular-Type ( globular-type-Reflexive-Globular-Type) field refl-Reflexive-Globular-Type : is-reflexive-globular-structure globular-structure-Reflexive-Globular-Type refl-0-cell-Reflexive-Globular-Type : {x : 0-cell-Reflexive-Globular-Type} → 1-cell-Reflexive-Globular-Type x x refl-0-cell-Reflexive-Globular-Type = is-reflexive-1-cell-is-reflexive-globular-structure ( refl-Reflexive-Globular-Type) ( _) 1-cell-globular-type-Reflexive-Globular-Type : (x y : 0-cell-Reflexive-Globular-Type) → Globular-Type l2 l2 1-cell-globular-type-Reflexive-Globular-Type = 1-cell-globular-type-Globular-Type globular-type-Reflexive-Globular-Type 1-cell-reflexive-globular-type-Reflexive-Globular-Type : (x y : 0-cell-Reflexive-Globular-Type) → Reflexive-Globular-Type l2 l2 globular-type-Reflexive-Globular-Type ( 1-cell-reflexive-globular-type-Reflexive-Globular-Type x y) = 1-cell-globular-type-Reflexive-Globular-Type x y refl-Reflexive-Globular-Type ( 1-cell-reflexive-globular-type-Reflexive-Globular-Type x y) = is-reflexive-globular-structure-1-cell-is-reflexive-globular-structure ( refl-Reflexive-Globular-Type) ( x) ( y) open Reflexive-Globular-Type public
Examples
The reflexive globular structure on a type given by its identity types
is-reflexive-globular-structure-Id : {l : Level} (A : UU l) → is-reflexive-globular-structure (globular-structure-Id A) is-reflexive-globular-structure-Id A = λ where .is-reflexive-1-cell-is-reflexive-globular-structure x → refl .is-reflexive-globular-structure-1-cell-is-reflexive-globular-structure x y → is-reflexive-globular-structure-Id (x = y)
Recent changes
- 2024-09-03. Egbert Rijke. Some infrastructure for dependent globular types (#1176).
- 2024-06-16. Fredrik Bakke and Vojtěch Štěpančík. Noncoherent wild higher precategories (#1099).
- 2024-03-20. Fredrik Bakke. Globular types (#1084).