The wild category of types
Content created by Fredrik Bakke and Vojtěch Štěpančík.
Created on 2024-06-16.
Last modified on 2024-06-16.
{-# OPTIONS --guardedness #-} module foundation.wild-category-of-types where
Imports
open import foundation.dependent-pair-types open import foundation.fundamental-theorem-of-identity-types open import foundation.homotopies open import foundation.isomorphisms-of-sets open import foundation.sets open import foundation.strictly-involutive-identity-types open import foundation.universe-levels open import foundation-core.contractible-types open import foundation-core.equivalences open import foundation-core.function-types open import foundation-core.functoriality-dependent-pair-types open import foundation-core.identity-types open import structured-types.globular-types open import structured-types.large-globular-types open import structured-types.large-reflexive-globular-types open import structured-types.large-transitive-globular-types open import structured-types.reflexive-globular-types open import structured-types.transitive-globular-types open import wild-category-theory.isomorphisms-in-noncoherent-large-wild-higher-precategories open import wild-category-theory.isomorphisms-in-noncoherent-wild-higher-precategories open import wild-category-theory.noncoherent-large-wild-higher-precategories open import wild-category-theory.noncoherent-wild-higher-precategories
Idea
The wild category of types¶ consists of types and functions and homotopies.
Definitions
The globular structure on dependent function types
globular-structure-Π : {l1 l2 : Level} {A : UU l1} {B : A → UU l2} → globular-structure (l1 ⊔ l2) ((x : A) → B x) globular-structure-Π = λ where .1-cell-globular-structure → _~_ .globular-structure-1-cell-globular-structure f g → globular-structure-Π is-reflexive-globular-structure-Π : {l1 l2 : Level} {A : UU l1} {B : A → UU l2} → is-reflexive-globular-structure (globular-structure-Π {A = A} {B}) is-reflexive-globular-structure-Π = λ where .is-reflexive-1-cell-is-reflexive-globular-structure f → refl-htpy .is-reflexive-globular-structure-1-cell-is-reflexive-globular-structure f g → is-reflexive-globular-structure-Π is-transitive-globular-structure-Π : {l1 l2 : Level} {A : UU l1} {B : A → UU l2} → is-transitive-globular-structure (globular-structure-Π {A = A} {B}) is-transitive-globular-structure-Π = λ where .comp-1-cell-is-transitive-globular-structure H K → K ∙h H .is-transitive-globular-structure-1-cell-is-transitive-globular-structure H K → is-transitive-globular-structure-Π
The large globular structure on types
large-globular-structure-Type : large-globular-structure (_⊔_) (λ l → UU l) large-globular-structure-Type = λ where .1-cell-large-globular-structure X Y → (X → Y) .globular-structure-1-cell-large-globular-structure X Y → globular-structure-Π is-reflexive-large-globular-structure-Type : is-reflexive-large-globular-structure large-globular-structure-Type is-reflexive-large-globular-structure-Type = λ where .is-reflexive-1-cell-is-reflexive-large-globular-structure X → id .is-reflexive-globular-structure-1-cell-is-reflexive-large-globular-structure X Y → is-reflexive-globular-structure-Π is-transitive-large-globular-structure-Type : is-transitive-large-globular-structure large-globular-structure-Type is-transitive-large-globular-structure-Type = λ where .comp-1-cell-is-transitive-large-globular-structure g f → g ∘ f .is-transitive-globular-structure-1-cell-is-transitive-large-globular-structure X Y → is-transitive-globular-structure-Π
The noncoherent large wild higher precategory of types
Type-Noncoherent-Large-Wild-Higher-Precategory : Noncoherent-Large-Wild-Higher-Precategory lsuc (_⊔_) Type-Noncoherent-Large-Wild-Higher-Precategory = λ where .obj-Noncoherent-Large-Wild-Higher-Precategory l → UU l .hom-globular-structure-Noncoherent-Large-Wild-Higher-Precategory → large-globular-structure-Type .id-hom-globular-structure-Noncoherent-Large-Wild-Higher-Precategory → is-reflexive-large-globular-structure-Type .comp-hom-globular-structure-Noncoherent-Large-Wild-Higher-Precategory → is-transitive-large-globular-structure-Type
Recent changes
- 2024-06-16. Fredrik Bakke and Vojtěch Štěpančík. Noncoherent wild higher precategories (#1099).