Colax functors between large noncoherent wild higher precategories
Content created by Egbert Rijke, Fredrik Bakke and Vojtěch Štěpančík.
Created on 2024-06-16.
Last modified on 2024-12-03.
{-# OPTIONS --guardedness #-} module wild-category-theory.colax-functors-noncoherent-large-wild-higher-precategories where
Imports
open import foundation.dependent-pair-types open import foundation.function-types open import foundation.identity-types open import foundation.universe-levels open import globular-types.globular-maps open import globular-types.globular-types open import globular-types.large-colax-reflexive-globular-maps open import globular-types.large-colax-transitive-globular-maps open import globular-types.large-globular-maps open import wild-category-theory.colax-functors-noncoherent-wild-higher-precategories open import wild-category-theory.maps-noncoherent-large-wild-higher-precategories open import wild-category-theory.maps-noncoherent-wild-higher-precategories open import wild-category-theory.noncoherent-large-wild-higher-precategories open import wild-category-theory.noncoherent-wild-higher-precategories
Idea
A
colax functor¶
f
between
noncoherent large wild higher precategories
𝒜
and ℬ
is a
map of noncoherent large wild higher precategories
that preserves identity morphisms and composition colaxly. This means that for
every -morphism f
in 𝒜
, where we take -morphisms to be objects, there
is an -morphism
Fₙ₊₁ (id-hom 𝒜 f) ⇒ id-hom ℬ (Fₙ f)
in ℬ
, and for every pair of composable -morphisms g
after f
in 𝒜
,
there is an -morphism
Fₙ₊₁ (g ∘ f) ⇒ (Fₙ₊₁ g) ∘ (Fₙ₊₁ f)
in ℬ
.
Definitions
The predicate on maps between large noncoherent wild higher precategories of preserving the identity structure
preserves-id-structure-map-Noncoherent-Large-Wild-Higher-Precategory : {α1 α2 γ : Level → Level} {β1 β2 : Level → Level → Level} (𝒜 : Noncoherent-Large-Wild-Higher-Precategory α1 β1) (ℬ : Noncoherent-Large-Wild-Higher-Precategory α2 β2) (F : map-Noncoherent-Large-Wild-Higher-Precategory γ 𝒜 ℬ) → UUω preserves-id-structure-map-Noncoherent-Large-Wild-Higher-Precategory 𝒜 ℬ F = is-colax-reflexive-large-globular-map ( large-reflexive-globular-type-Noncoherent-Large-Wild-Higher-Precategory 𝒜) ( large-reflexive-globular-type-Noncoherent-Large-Wild-Higher-Precategory ℬ) ( F)
The predicate on maps between large noncoherent wild higher precategories of preserving the composition structure
preserves-comp-structure-map-Noncoherent-Large-Wild-Higher-Precategory : {α1 α2 γ : Level → Level} {β1 β2 : Level → Level → Level} (𝒜 : Noncoherent-Large-Wild-Higher-Precategory α1 β1) (ℬ : Noncoherent-Large-Wild-Higher-Precategory α2 β2) (F : map-Noncoherent-Large-Wild-Higher-Precategory γ 𝒜 ℬ) → UUω preserves-comp-structure-map-Noncoherent-Large-Wild-Higher-Precategory 𝒜 ℬ F = is-colax-transitive-large-globular-map ( large-transitive-globular-type-Noncoherent-Large-Wild-Higher-Precategory 𝒜) ( large-transitive-globular-type-Noncoherent-Large-Wild-Higher-Precategory ℬ) ( F)
The predicate of being a colax functor between noncoherent wild higher precategories
record is-colax-functor-Noncoherent-Large-Wild-Higher-Precategory {α1 α2 : Level → Level} {β1 β2 : Level → Level → Level} {γ : Level → Level} (𝒜 : Noncoherent-Large-Wild-Higher-Precategory α1 β1) (ℬ : Noncoherent-Large-Wild-Higher-Precategory α2 β2) (F : map-Noncoherent-Large-Wild-Higher-Precategory γ 𝒜 ℬ) : UUω where constructor make-is-colax-functor-Noncoherent-Large-Wild-Higher-Precategory field preserves-id-structure-is-colax-functor-Noncoherent-Large-Wild-Higher-Precategory : preserves-id-structure-map-Noncoherent-Large-Wild-Higher-Precategory ( 𝒜) ( ℬ) ( F) field preserves-comp-structure-is-colax-functor-Noncoherent-Large-Wild-Higher-Precategory : preserves-comp-structure-map-Noncoherent-Large-Wild-Higher-Precategory ( 𝒜) ( ℬ) ( F) preserves-id-hom-is-colax-functor-Noncoherent-Large-Wild-Higher-Precategory : {l : Level} (x : obj-Noncoherent-Large-Wild-Higher-Precategory 𝒜 l) → 2-hom-Noncoherent-Large-Wild-Higher-Precategory ℬ ( hom-map-Noncoherent-Large-Wild-Higher-Precategory 𝒜 ℬ F ( id-hom-Noncoherent-Large-Wild-Higher-Precategory 𝒜 {x = x})) ( id-hom-Noncoherent-Large-Wild-Higher-Precategory ℬ { x = obj-map-Noncoherent-Large-Wild-Higher-Precategory 𝒜 ℬ F x}) preserves-id-hom-is-colax-functor-Noncoherent-Large-Wild-Higher-Precategory = preserves-refl-1-cell-is-colax-reflexive-large-globular-map preserves-id-structure-is-colax-functor-Noncoherent-Large-Wild-Higher-Precategory preserves-id-structure-hom-is-colax-functor-Noncoherent-Large-Wild-Higher-Precategory : {l1 l2 : Level} {x : obj-Noncoherent-Large-Wild-Higher-Precategory 𝒜 l1} {y : obj-Noncoherent-Large-Wild-Higher-Precategory 𝒜 l2} → preserves-id-structure-map-Noncoherent-Wild-Higher-Precategory ( hom-noncoherent-wild-higher-precategory-Noncoherent-Large-Wild-Higher-Precategory 𝒜 x y) ( hom-noncoherent-wild-higher-precategory-Noncoherent-Large-Wild-Higher-Precategory ℬ _ _) ( 1-cell-globular-map-large-globular-map F) preserves-id-structure-hom-is-colax-functor-Noncoherent-Large-Wild-Higher-Precategory = is-colax-reflexive-1-cell-globular-map-is-colax-reflexive-large-globular-map preserves-id-structure-is-colax-functor-Noncoherent-Large-Wild-Higher-Precategory preserves-comp-hom-is-colax-functor-Noncoherent-Large-Wild-Higher-Precategory : {l1 l2 l3 : Level} {x : obj-Noncoherent-Large-Wild-Higher-Precategory 𝒜 l1} {y : obj-Noncoherent-Large-Wild-Higher-Precategory 𝒜 l2} {z : obj-Noncoherent-Large-Wild-Higher-Precategory 𝒜 l3} (g : hom-Noncoherent-Large-Wild-Higher-Precategory 𝒜 y z) (f : hom-Noncoherent-Large-Wild-Higher-Precategory 𝒜 x y) → 2-hom-Noncoherent-Large-Wild-Higher-Precategory ℬ ( hom-map-Noncoherent-Large-Wild-Higher-Precategory 𝒜 ℬ F ( comp-hom-Noncoherent-Large-Wild-Higher-Precategory 𝒜 g f)) ( comp-hom-Noncoherent-Large-Wild-Higher-Precategory ℬ ( hom-map-Noncoherent-Large-Wild-Higher-Precategory 𝒜 ℬ F g) ( hom-map-Noncoherent-Large-Wild-Higher-Precategory 𝒜 ℬ F f)) preserves-comp-hom-is-colax-functor-Noncoherent-Large-Wild-Higher-Precategory = preserves-comp-1-cell-is-colax-transitive-large-globular-map preserves-comp-structure-is-colax-functor-Noncoherent-Large-Wild-Higher-Precategory preserves-comp-structure-hom-is-colax-functor-Noncoherent-Large-Wild-Higher-Precategory : {l1 l2 : Level} {x : obj-Noncoherent-Large-Wild-Higher-Precategory 𝒜 l1} {y : obj-Noncoherent-Large-Wild-Higher-Precategory 𝒜 l2} → preserves-comp-structure-map-Noncoherent-Wild-Higher-Precategory ( hom-noncoherent-wild-higher-precategory-Noncoherent-Large-Wild-Higher-Precategory 𝒜 x y) ( hom-noncoherent-wild-higher-precategory-Noncoherent-Large-Wild-Higher-Precategory ℬ _ _) ( 1-cell-globular-map-large-globular-map F) preserves-comp-structure-hom-is-colax-functor-Noncoherent-Large-Wild-Higher-Precategory = is-colax-transitive-1-cell-globular-map-is-colax-transitive-large-globular-map preserves-comp-structure-is-colax-functor-Noncoherent-Large-Wild-Higher-Precategory is-colax-functor-hom-is-colax-functor-map-Noncoherent-Large-Wild-Higher-Precategory : {l1 l2 : Level} {x : obj-Noncoherent-Large-Wild-Higher-Precategory 𝒜 l1} {y : obj-Noncoherent-Large-Wild-Higher-Precategory 𝒜 l2} → is-colax-functor-Noncoherent-Wild-Higher-Precategory ( hom-noncoherent-wild-higher-precategory-Noncoherent-Large-Wild-Higher-Precategory 𝒜 x y) ( hom-noncoherent-wild-higher-precategory-Noncoherent-Large-Wild-Higher-Precategory ℬ _ _) ( 1-cell-globular-map-large-globular-map F) is-colax-functor-hom-is-colax-functor-map-Noncoherent-Large-Wild-Higher-Precategory = make-is-colax-functor-Noncoherent-Wild-Higher-Precategory preserves-id-structure-hom-is-colax-functor-Noncoherent-Large-Wild-Higher-Precategory preserves-comp-structure-hom-is-colax-functor-Noncoherent-Large-Wild-Higher-Precategory open is-colax-functor-Noncoherent-Large-Wild-Higher-Precategory public
The type of colax functors between noncoherent wild higher precategories
record colax-functor-Noncoherent-Large-Wild-Higher-Precategory {α1 α2 : Level → Level} {β1 β2 : Level → Level → Level} (δ : Level → Level) (𝒜 : Noncoherent-Large-Wild-Higher-Precategory α1 β1) (ℬ : Noncoherent-Large-Wild-Higher-Precategory α2 β2) : UUω where constructor make-colax-functor-Noncoherent-Large-Wild-Higher-Precategory
The underlying large globular map of a colax functor:
field map-colax-functor-Noncoherent-Large-Wild-Higher-Precategory : map-Noncoherent-Large-Wild-Higher-Precategory δ 𝒜 ℬ obj-colax-functor-Noncoherent-Large-Wild-Higher-Precategory : {l : Level} → obj-Noncoherent-Large-Wild-Higher-Precategory 𝒜 l → obj-Noncoherent-Large-Wild-Higher-Precategory ℬ (δ l) obj-colax-functor-Noncoherent-Large-Wild-Higher-Precategory = obj-map-Noncoherent-Large-Wild-Higher-Precategory 𝒜 ℬ ( map-colax-functor-Noncoherent-Large-Wild-Higher-Precategory) hom-colax-functor-Noncoherent-Large-Wild-Higher-Precategory : {l1 l2 : Level} {x : obj-Noncoherent-Large-Wild-Higher-Precategory 𝒜 l1} {y : obj-Noncoherent-Large-Wild-Higher-Precategory 𝒜 l2} → hom-Noncoherent-Large-Wild-Higher-Precategory 𝒜 x y → hom-Noncoherent-Large-Wild-Higher-Precategory ℬ ( obj-colax-functor-Noncoherent-Large-Wild-Higher-Precategory x) ( obj-colax-functor-Noncoherent-Large-Wild-Higher-Precategory y) hom-colax-functor-Noncoherent-Large-Wild-Higher-Precategory = hom-map-Noncoherent-Large-Wild-Higher-Precategory 𝒜 ℬ map-colax-functor-Noncoherent-Large-Wild-Higher-Precategory 2-hom-colax-functor-Noncoherent-Large-Wild-Higher-Precategory : {l1 l2 : Level} {x : obj-Noncoherent-Large-Wild-Higher-Precategory 𝒜 l1} {y : obj-Noncoherent-Large-Wild-Higher-Precategory 𝒜 l2} {f g : hom-Noncoherent-Large-Wild-Higher-Precategory 𝒜 x y} → 2-hom-Noncoherent-Large-Wild-Higher-Precategory 𝒜 f g → 2-hom-Noncoherent-Large-Wild-Higher-Precategory ℬ ( hom-colax-functor-Noncoherent-Large-Wild-Higher-Precategory f) ( hom-colax-functor-Noncoherent-Large-Wild-Higher-Precategory g) 2-hom-colax-functor-Noncoherent-Large-Wild-Higher-Precategory = 2-hom-map-Noncoherent-Large-Wild-Higher-Precategory 𝒜 ℬ map-colax-functor-Noncoherent-Large-Wild-Higher-Precategory hom-globular-map-colax-functor-Noncoherent-Large-Wild-Higher-Precategory : {l1 l2 : Level} {x : obj-Noncoherent-Large-Wild-Higher-Precategory 𝒜 l1} {y : obj-Noncoherent-Large-Wild-Higher-Precategory 𝒜 l2} → globular-map ( hom-globular-type-Noncoherent-Large-Wild-Higher-Precategory 𝒜 x y) ( hom-globular-type-Noncoherent-Large-Wild-Higher-Precategory ℬ ( obj-colax-functor-Noncoherent-Large-Wild-Higher-Precategory x) ( obj-colax-functor-Noncoherent-Large-Wild-Higher-Precategory y)) hom-globular-map-colax-functor-Noncoherent-Large-Wild-Higher-Precategory = hom-globular-map-map-Noncoherent-Large-Wild-Higher-Precategory 𝒜 ℬ ( map-colax-functor-Noncoherent-Large-Wild-Higher-Precategory) field is-colax-functor-colax-functor-Noncoherent-Large-Wild-Higher-Precategory : is-colax-functor-Noncoherent-Large-Wild-Higher-Precategory 𝒜 ℬ ( map-colax-functor-Noncoherent-Large-Wild-Higher-Precategory)
Preservation of the identity structure:
preserves-id-structure-colax-functor-Noncoherent-Large-Wild-Higher-Precategory : preserves-id-structure-map-Noncoherent-Large-Wild-Higher-Precategory 𝒜 ℬ map-colax-functor-Noncoherent-Large-Wild-Higher-Precategory preserves-id-structure-colax-functor-Noncoherent-Large-Wild-Higher-Precategory = preserves-id-structure-is-colax-functor-Noncoherent-Large-Wild-Higher-Precategory is-colax-functor-colax-functor-Noncoherent-Large-Wild-Higher-Precategory colax-reflexive-map-colax-functor-Noncoherent-Large-Wild-Higher-Precategory : large-colax-reflexive-globular-map δ ( large-reflexive-globular-type-Noncoherent-Large-Wild-Higher-Precategory 𝒜) ( large-reflexive-globular-type-Noncoherent-Large-Wild-Higher-Precategory ℬ) colax-reflexive-map-colax-functor-Noncoherent-Large-Wild-Higher-Precategory = make-large-colax-reflexive-globular-map map-colax-functor-Noncoherent-Large-Wild-Higher-Precategory preserves-id-structure-colax-functor-Noncoherent-Large-Wild-Higher-Precategory preserves-id-hom-colax-functor-Noncoherent-Large-Wild-Higher-Precategory : {l : Level} (x : obj-Noncoherent-Large-Wild-Higher-Precategory 𝒜 l) → 2-hom-Noncoherent-Large-Wild-Higher-Precategory ℬ ( hom-colax-functor-Noncoherent-Large-Wild-Higher-Precategory ( id-hom-Noncoherent-Large-Wild-Higher-Precategory 𝒜 {x = x})) ( id-hom-Noncoherent-Large-Wild-Higher-Precategory ℬ { x = obj-colax-functor-Noncoherent-Large-Wild-Higher-Precategory x}) preserves-id-hom-colax-functor-Noncoherent-Large-Wild-Higher-Precategory = preserves-id-hom-is-colax-functor-Noncoherent-Large-Wild-Higher-Precategory ( is-colax-functor-colax-functor-Noncoherent-Large-Wild-Higher-Precategory) preserves-id-structure-hom-colax-functor-Noncoherent-Large-Wild-Higher-Precategory : {l1 l2 : Level} {x : obj-Noncoherent-Large-Wild-Higher-Precategory 𝒜 l1} {y : obj-Noncoherent-Large-Wild-Higher-Precategory 𝒜 l2} → preserves-id-structure-map-Noncoherent-Wild-Higher-Precategory ( hom-noncoherent-wild-higher-precategory-Noncoherent-Large-Wild-Higher-Precategory 𝒜 x y) ( hom-noncoherent-wild-higher-precategory-Noncoherent-Large-Wild-Higher-Precategory ℬ _ _) ( 1-cell-globular-map-large-globular-map map-colax-functor-Noncoherent-Large-Wild-Higher-Precategory) preserves-id-structure-hom-colax-functor-Noncoherent-Large-Wild-Higher-Precategory = preserves-id-structure-hom-is-colax-functor-Noncoherent-Large-Wild-Higher-Precategory is-colax-functor-colax-functor-Noncoherent-Large-Wild-Higher-Precategory
Preservation of the composition structure:
preserves-comp-structure-colax-functor-Noncoherent-Large-Wild-Higher-Precategory : preserves-comp-structure-map-Noncoherent-Large-Wild-Higher-Precategory 𝒜 ℬ map-colax-functor-Noncoherent-Large-Wild-Higher-Precategory preserves-comp-structure-colax-functor-Noncoherent-Large-Wild-Higher-Precategory = preserves-comp-structure-is-colax-functor-Noncoherent-Large-Wild-Higher-Precategory is-colax-functor-colax-functor-Noncoherent-Large-Wild-Higher-Precategory colax-transitive-map-colax-functor-Noncoherent-Large-Wild-Higher-Precategory : large-colax-transitive-globular-map δ ( large-transitive-globular-type-Noncoherent-Large-Wild-Higher-Precategory 𝒜) ( large-transitive-globular-type-Noncoherent-Large-Wild-Higher-Precategory ℬ) large-globular-map-large-colax-transitive-globular-map colax-transitive-map-colax-functor-Noncoherent-Large-Wild-Higher-Precategory = map-colax-functor-Noncoherent-Large-Wild-Higher-Precategory is-colax-transitive-large-colax-transitive-globular-map colax-transitive-map-colax-functor-Noncoherent-Large-Wild-Higher-Precategory = preserves-comp-structure-colax-functor-Noncoherent-Large-Wild-Higher-Precategory preserves-comp-hom-colax-functor-Noncoherent-Large-Wild-Higher-Precategory : {l1 l2 l3 : Level} {x : obj-Noncoherent-Large-Wild-Higher-Precategory 𝒜 l1} {y : obj-Noncoherent-Large-Wild-Higher-Precategory 𝒜 l2} {z : obj-Noncoherent-Large-Wild-Higher-Precategory 𝒜 l3} (g : hom-Noncoherent-Large-Wild-Higher-Precategory 𝒜 y z) (f : hom-Noncoherent-Large-Wild-Higher-Precategory 𝒜 x y) → 2-hom-Noncoherent-Large-Wild-Higher-Precategory ℬ ( hom-colax-functor-Noncoherent-Large-Wild-Higher-Precategory ( comp-hom-Noncoherent-Large-Wild-Higher-Precategory 𝒜 g f)) ( comp-hom-Noncoherent-Large-Wild-Higher-Precategory ℬ ( hom-colax-functor-Noncoherent-Large-Wild-Higher-Precategory g) ( hom-colax-functor-Noncoherent-Large-Wild-Higher-Precategory f)) preserves-comp-hom-colax-functor-Noncoherent-Large-Wild-Higher-Precategory = preserves-comp-hom-is-colax-functor-Noncoherent-Large-Wild-Higher-Precategory ( is-colax-functor-colax-functor-Noncoherent-Large-Wild-Higher-Precategory) preserves-comp-structure-hom-colax-functor-Noncoherent-Large-Wild-Higher-Precategory : {l1 l2 : Level} {x : obj-Noncoherent-Large-Wild-Higher-Precategory 𝒜 l1} {y : obj-Noncoherent-Large-Wild-Higher-Precategory 𝒜 l2} → preserves-comp-structure-map-Noncoherent-Wild-Higher-Precategory ( hom-noncoherent-wild-higher-precategory-Noncoherent-Large-Wild-Higher-Precategory 𝒜 x y) ( hom-noncoherent-wild-higher-precategory-Noncoherent-Large-Wild-Higher-Precategory ℬ _ _) ( 1-cell-globular-map-large-globular-map map-colax-functor-Noncoherent-Large-Wild-Higher-Precategory) preserves-comp-structure-hom-colax-functor-Noncoherent-Large-Wild-Higher-Precategory = preserves-comp-structure-hom-is-colax-functor-Noncoherent-Large-Wild-Higher-Precategory is-colax-functor-colax-functor-Noncoherent-Large-Wild-Higher-Precategory
The globular map on hom-types is again a colax functor:
is-colax-functor-hom-colax-functor-colax-functor-Noncoherent-Large-Wild-Higher-Precategory : {l1 l2 : Level} {x : obj-Noncoherent-Large-Wild-Higher-Precategory 𝒜 l1} {y : obj-Noncoherent-Large-Wild-Higher-Precategory 𝒜 l2} → is-colax-functor-Noncoherent-Wild-Higher-Precategory ( hom-noncoherent-wild-higher-precategory-Noncoherent-Large-Wild-Higher-Precategory ( 𝒜) ( x) ( y)) ( hom-noncoherent-wild-higher-precategory-Noncoherent-Large-Wild-Higher-Precategory ( ℬ) ( obj-colax-functor-Noncoherent-Large-Wild-Higher-Precategory x) ( obj-colax-functor-Noncoherent-Large-Wild-Higher-Precategory y)) ( hom-globular-map-colax-functor-Noncoherent-Large-Wild-Higher-Precategory) is-colax-functor-hom-colax-functor-colax-functor-Noncoherent-Large-Wild-Higher-Precategory = make-is-colax-functor-Noncoherent-Wild-Higher-Precategory preserves-id-structure-hom-colax-functor-Noncoherent-Large-Wild-Higher-Precategory preserves-comp-structure-hom-colax-functor-Noncoherent-Large-Wild-Higher-Precategory hom-colax-functor-colax-functor-Noncoherent-Large-Wild-Higher-Precategory : {l1 l2 : Level} (x : obj-Noncoherent-Large-Wild-Higher-Precategory 𝒜 l1) (y : obj-Noncoherent-Large-Wild-Higher-Precategory 𝒜 l2) → colax-functor-Noncoherent-Wild-Higher-Precategory ( hom-noncoherent-wild-higher-precategory-Noncoherent-Large-Wild-Higher-Precategory ( 𝒜) ( x) ( y)) ( hom-noncoherent-wild-higher-precategory-Noncoherent-Large-Wild-Higher-Precategory ( ℬ) ( obj-colax-functor-Noncoherent-Large-Wild-Higher-Precategory x) ( obj-colax-functor-Noncoherent-Large-Wild-Higher-Precategory y)) hom-colax-functor-colax-functor-Noncoherent-Large-Wild-Higher-Precategory x y = hom-globular-map-colax-functor-Noncoherent-Large-Wild-Higher-Precategory , is-colax-functor-hom-colax-functor-colax-functor-Noncoherent-Large-Wild-Higher-Precategory open colax-functor-Noncoherent-Large-Wild-Higher-Precategory public
The identity colax functor on a noncoherent large wild higher precategory
module _ {α : Level → Level} {β : Level → Level → Level} (𝒜 : Noncoherent-Large-Wild-Higher-Precategory α β) where preserves-id-structure-id-colax-functor-Noncoherent-Large-Wild-Higher-Precatory : preserves-id-structure-map-Noncoherent-Large-Wild-Higher-Precategory 𝒜 𝒜 ( id-map-Noncoherent-Large-Wild-Higher-Precategory 𝒜) preserves-id-structure-id-colax-functor-Noncoherent-Large-Wild-Higher-Precatory = is-colax-reflexive-id-large-colax-reflexive-globular-map ( large-reflexive-globular-type-Noncoherent-Large-Wild-Higher-Precategory 𝒜) preserves-comp-structure-id-colax-functor-Noncoherent-Large-Wild-Higher-Precategory : preserves-comp-structure-map-Noncoherent-Large-Wild-Higher-Precategory 𝒜 𝒜 ( id-map-Noncoherent-Large-Wild-Higher-Precategory 𝒜) preserves-comp-1-cell-is-colax-transitive-large-globular-map preserves-comp-structure-id-colax-functor-Noncoherent-Large-Wild-Higher-Precategory g f = id-2-hom-Noncoherent-Large-Wild-Higher-Precategory 𝒜 _ is-colax-transitive-1-cell-globular-map-is-colax-transitive-large-globular-map preserves-comp-structure-id-colax-functor-Noncoherent-Large-Wild-Higher-Precategory = preserves-comp-structure-id-colax-functor-Noncoherent-Wild-Higher-Precategory ( hom-noncoherent-wild-higher-precategory-Noncoherent-Large-Wild-Higher-Precategory 𝒜 _ _) is-colax-functor-id-colax-functor-Noncoherent-Large-Wild-Higher-Precategory : is-colax-functor-Noncoherent-Large-Wild-Higher-Precategory 𝒜 𝒜 ( id-map-Noncoherent-Large-Wild-Higher-Precategory 𝒜) is-colax-functor-id-colax-functor-Noncoherent-Large-Wild-Higher-Precategory = make-is-colax-functor-Noncoherent-Large-Wild-Higher-Precategory preserves-id-structure-id-colax-functor-Noncoherent-Large-Wild-Higher-Precatory preserves-comp-structure-id-colax-functor-Noncoherent-Large-Wild-Higher-Precategory id-colax-functor-Noncoherent-Large-Wild-Higher-Precategory : colax-functor-Noncoherent-Large-Wild-Higher-Precategory (λ l → l) 𝒜 𝒜 map-colax-functor-Noncoherent-Large-Wild-Higher-Precategory id-colax-functor-Noncoherent-Large-Wild-Higher-Precategory = id-map-Noncoherent-Large-Wild-Higher-Precategory 𝒜 is-colax-functor-colax-functor-Noncoherent-Large-Wild-Higher-Precategory id-colax-functor-Noncoherent-Large-Wild-Higher-Precategory = is-colax-functor-id-colax-functor-Noncoherent-Large-Wild-Higher-Precategory
Composition of colax functors between noncoherent wild higher precategories
module _ {α1 α2 α3 : Level → Level} {β1 β2 β3 : Level → Level → Level} {δ1 δ2 : Level → Level} {𝒜 : Noncoherent-Large-Wild-Higher-Precategory α1 β1} {ℬ : Noncoherent-Large-Wild-Higher-Precategory α2 β2} {𝒞 : Noncoherent-Large-Wild-Higher-Precategory α3 β3} (G : colax-functor-Noncoherent-Large-Wild-Higher-Precategory δ2 ℬ 𝒞) (F : colax-functor-Noncoherent-Large-Wild-Higher-Precategory δ1 𝒜 ℬ) where map-comp-colax-functor-Noncoherent-Large-Wild-Higher-Precategory : map-Noncoherent-Large-Wild-Higher-Precategory (λ l → δ2 (δ1 l)) 𝒜 𝒞 map-comp-colax-functor-Noncoherent-Large-Wild-Higher-Precategory = comp-map-Noncoherent-Large-Wild-Higher-Precategory 𝒜 ℬ 𝒞 ( map-colax-functor-Noncoherent-Large-Wild-Higher-Precategory G) ( map-colax-functor-Noncoherent-Large-Wild-Higher-Precategory F) preserves-id-structure-comp-colax-functor-Noncoherent-Large-Wild-Higher-Precategory : preserves-id-structure-map-Noncoherent-Large-Wild-Higher-Precategory 𝒜 𝒞 map-comp-colax-functor-Noncoherent-Large-Wild-Higher-Precategory preserves-refl-1-cell-is-colax-reflexive-large-globular-map preserves-id-structure-comp-colax-functor-Noncoherent-Large-Wild-Higher-Precategory x = comp-2-hom-Noncoherent-Large-Wild-Higher-Precategory 𝒞 ( preserves-id-hom-colax-functor-Noncoherent-Large-Wild-Higher-Precategory ( G) ( _)) ( 2-hom-colax-functor-Noncoherent-Large-Wild-Higher-Precategory G ( preserves-id-hom-colax-functor-Noncoherent-Large-Wild-Higher-Precategory ( F) ( _))) is-colax-reflexive-1-cell-globular-map-is-colax-reflexive-large-globular-map preserves-id-structure-comp-colax-functor-Noncoherent-Large-Wild-Higher-Precategory = preserves-id-structure-comp-colax-functor-Noncoherent-Wild-Higher-Precategory ( hom-noncoherent-wild-higher-precategory-Noncoherent-Large-Wild-Higher-Precategory 𝒜 _ _) ( hom-noncoherent-wild-higher-precategory-Noncoherent-Large-Wild-Higher-Precategory ℬ _ _) ( hom-noncoherent-wild-higher-precategory-Noncoherent-Large-Wild-Higher-Precategory 𝒞 _ _) ( hom-colax-functor-colax-functor-Noncoherent-Large-Wild-Higher-Precategory G _ _) ( hom-colax-functor-colax-functor-Noncoherent-Large-Wild-Higher-Precategory F _ _) preserves-comp-structure-comp-colax-functor-Noncoherent-Large-Wild-Higher-Precategory : preserves-comp-structure-map-Noncoherent-Large-Wild-Higher-Precategory 𝒜 𝒞 map-comp-colax-functor-Noncoherent-Large-Wild-Higher-Precategory preserves-comp-structure-comp-colax-functor-Noncoherent-Large-Wild-Higher-Precategory = is-colax-transitive-comp-large-colax-transitive-globular-map ( large-transitive-globular-type-Noncoherent-Large-Wild-Higher-Precategory 𝒜) ( large-transitive-globular-type-Noncoherent-Large-Wild-Higher-Precategory ℬ) ( large-transitive-globular-type-Noncoherent-Large-Wild-Higher-Precategory 𝒞) ( colax-transitive-map-colax-functor-Noncoherent-Large-Wild-Higher-Precategory G) ( colax-transitive-map-colax-functor-Noncoherent-Large-Wild-Higher-Precategory F) is-colax-functor-comp-colax-functor-Noncoherent-Large-Wild-Precategory : is-colax-functor-Noncoherent-Large-Wild-Higher-Precategory 𝒜 𝒞 map-comp-colax-functor-Noncoherent-Large-Wild-Higher-Precategory is-colax-functor-comp-colax-functor-Noncoherent-Large-Wild-Precategory = make-is-colax-functor-Noncoherent-Large-Wild-Higher-Precategory preserves-id-structure-comp-colax-functor-Noncoherent-Large-Wild-Higher-Precategory preserves-comp-structure-comp-colax-functor-Noncoherent-Large-Wild-Higher-Precategory comp-colax-functor-Noncoherent-Large-Wild-Precategory : colax-functor-Noncoherent-Large-Wild-Higher-Precategory ( λ l → δ2 (δ1 l)) ( 𝒜) ( 𝒞) comp-colax-functor-Noncoherent-Large-Wild-Precategory = make-colax-functor-Noncoherent-Large-Wild-Higher-Precategory map-comp-colax-functor-Noncoherent-Large-Wild-Higher-Precategory is-colax-functor-comp-colax-functor-Noncoherent-Large-Wild-Precategory
Recent changes
- 2024-12-03. Egbert Rijke. Hofmann-Streicher universes for graphs and globular types (#1196).
- 2024-11-17. Egbert Rijke. chore: Moving files about globular types to a new namespace (#1223).
- 2024-07-10. Fredrik Bakke. chore: Fix some typos in the
wild-category-theory
module (#1158). - 2024-06-16. Fredrik Bakke and Vojtěch Štěpančík. Noncoherent wild higher precategories (#1099).