Large transitive 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-transitive-globular-types where
Imports
open import foundation.universe-levels open import structured-types.large-globular-types open import structured-types.transitive-globular-types
Idea
A
large transitive globular type¶
is a large globular type A
equipped with a binary operator
- * - : (𝑛+1)-Cell A y z → (𝑛+1)-Cell A x y → (𝑛+1)-Cell A x z
at every level .
Definition
The structure transitivitiy on a large globular type
record is-transitive-large-globular-structure {α : Level → Level} {β : Level → Level → Level} {A : (l : Level) → UU (α l)} (G : large-globular-structure β A) : UUω where field comp-1-cell-is-transitive-large-globular-structure : {l1 l2 l3 : Level} {x : A l1} {y : A l2} {z : A l3} → 1-cell-large-globular-structure G y z → 1-cell-large-globular-structure G x y → 1-cell-large-globular-structure G x z is-transitive-globular-structure-1-cell-is-transitive-large-globular-structure : {l1 l2 : Level} (x : A l1) (y : A l2) → is-transitive-globular-structure ( globular-structure-1-cell-large-globular-structure G x y) open is-transitive-large-globular-structure public module _ {α : Level → Level} {β : Level → Level → Level} {A : (l : Level) → UU (α l)} {G : large-globular-structure β A} (r : is-transitive-large-globular-structure G) where comp-2-cell-is-transitive-large-globular-structure : {l1 l2 : Level} {x : A l1} {y : A l2} {f g h : 1-cell-large-globular-structure G x y} → 2-cell-large-globular-structure G g h → 2-cell-large-globular-structure G f g → 2-cell-large-globular-structure G f h comp-2-cell-is-transitive-large-globular-structure {x = x} {y} = comp-1-cell-is-transitive-globular-structure ( is-transitive-globular-structure-1-cell-is-transitive-large-globular-structure ( r) ( x) ( y)) comp-3-cell-is-transitive-large-globular-structure : {l1 l2 : Level} {x : A l1} {y : A l2} {f g : 1-cell-large-globular-structure G x y} {H K L : 2-cell-large-globular-structure G f g} → 3-cell-large-globular-structure G K L → 3-cell-large-globular-structure G H K → 3-cell-large-globular-structure G H L comp-3-cell-is-transitive-large-globular-structure {x = x} {y} = comp-2-cell-is-transitive-globular-structure ( is-transitive-globular-structure-1-cell-is-transitive-large-globular-structure ( r) ( x) ( y))
The type of transitive globular structures on a large type
record large-transitive-globular-structure {α : Level → Level} (β : Level → Level → Level) (A : (l : Level) → UU (α l)) : UUω where field large-globular-structure-large-transitive-globular-structure : large-globular-structure β A is-transitive-large-globular-structure-large-transitive-globular-structure : is-transitive-large-globular-structure ( large-globular-structure-large-transitive-globular-structure) open large-transitive-globular-structure public
The type of large transitive globular types
record Large-Transitive-Globular-Type (α : Level → Level) (β : Level → Level → Level) : UUω where field 0-cell-Large-Transitive-Globular-Type : (l : Level) → UU (α l) transitive-globular-structure-0-cell-Large-Transitive-Globular-Type : large-transitive-globular-structure ( β) ( 0-cell-Large-Transitive-Globular-Type) open Large-Transitive-Globular-Type public
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).