The wild category of types
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 foundation.wild-category-of-types where
Imports
open import foundation.dependent-pair-types open import foundation.fundamental-theorem-of-identity-types open import foundation.globular-type-of-functions 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 globular-types.globular-types open import globular-types.large-globular-types open import globular-types.large-reflexive-globular-types open import globular-types.large-transitive-globular-types open import globular-types.reflexive-globular-types open import globular-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 large globular type of types
Type-Large-Globular-Type : Large-Globular-Type lsuc (_⊔_) 0-cell-Large-Globular-Type Type-Large-Globular-Type l = UU l 1-cell-globular-type-Large-Globular-Type Type-Large-Globular-Type A B = function-type-Globular-Type A B is-reflexive-Type-Large-Globular-Type : is-reflexive-Large-Globular-Type Type-Large-Globular-Type refl-1-cell-is-reflexive-Large-Globular-Type is-reflexive-Type-Large-Globular-Type X = id is-reflexive-1-cell-globular-type-is-reflexive-Large-Globular-Type is-reflexive-Type-Large-Globular-Type = is-reflexive-function-type-Globular-Type Type-Large-Reflexive-Globular-Type : Large-Reflexive-Globular-Type lsuc (_⊔_) large-globular-type-Large-Reflexive-Globular-Type Type-Large-Reflexive-Globular-Type = Type-Large-Globular-Type is-reflexive-Large-Reflexive-Globular-Type Type-Large-Reflexive-Globular-Type = is-reflexive-Type-Large-Globular-Type is-transitive-Type-Large-Globular-Type : is-transitive-Large-Globular-Type Type-Large-Globular-Type comp-1-cell-is-transitive-Large-Globular-Type is-transitive-Type-Large-Globular-Type g f = g ∘ f is-transitive-1-cell-globular-type-is-transitive-Large-Globular-Type is-transitive-Type-Large-Globular-Type = is-transitive-function-type-Globular-Type Type-Large-Transitive-Globular-Type : Large-Transitive-Globular-Type lsuc (_⊔_) large-globular-type-Large-Transitive-Globular-Type Type-Large-Transitive-Globular-Type = Type-Large-Globular-Type is-transitive-Large-Transitive-Globular-Type Type-Large-Transitive-Globular-Type = is-transitive-Type-Large-Globular-Type
The noncoherent large wild higher precategory of types
Type-Noncoherent-Large-Wild-Higher-Precategory : Noncoherent-Large-Wild-Higher-Precategory lsuc (_⊔_) large-globular-type-Noncoherent-Large-Wild-Higher-Precategory Type-Noncoherent-Large-Wild-Higher-Precategory = Type-Large-Globular-Type id-structure-Noncoherent-Large-Wild-Higher-Precategory Type-Noncoherent-Large-Wild-Higher-Precategory = is-reflexive-Type-Large-Globular-Type comp-structure-Noncoherent-Large-Wild-Higher-Precategory Type-Noncoherent-Large-Wild-Higher-Precategory = is-transitive-Type-Large-Globular-Type
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-06-16. Fredrik Bakke and Vojtěch Štěpančík. Noncoherent wild higher precategories (#1099).