diff --git a/references.bib b/references.bib index 97fa0e6300..b721d14724 100644 --- a/references.bib +++ b/references.bib @@ -40,7 +40,7 @@ @misc{Anel24 @article{AL19, title = {Displayed Categories}, - author = {Ahrens, Benedikt and {{LeFanu}} Lumsdaine, Peter}, + author = {Ahrens, Benedikt and LeFanu Lumsdaine, Peter}, doi = {10.23638/LMCS-15(1:20)2019}, journal = {{Logical Methods in Computer Science}}, volume = {15}, @@ -55,14 +55,14 @@ @article{AL19 } @misc{Awodey22, - author = {{Awodey}, Steve}, - title = "{On Hofmann-Streicher universes}", - keywords = {Mathematics - Category Theory, Mathematics - Logic}, - year = 2022, - month = may, -archivePrefix = {arXiv}, - eprint = {2205.10917}, - primaryClass = {math.CT} + author = {Awodey, Steve}, + title = {{On Hofmann-Streicher universes}}, + keywords = {Mathematics - Category Theory, Mathematics - Logic}, + year = 2022, + month = may, + archiveprefix = {arXiv}, + eprint = {2205.10917}, + primaryclass = {math.CT} } @online{BCDE21, @@ -167,6 +167,22 @@ @article{Cantor1890/91 langid = {german} } +@article{Cheng07, + title = {An ω-Category with All {{Duals}} Is an ω-Groupoid}, + author = {Cheng, Eugenia}, + date = {2007-08-01}, + year = {2007}, + month = {08}, + journal = {Applied Categorical Structures}, + volume = {15}, + number = {4}, + pages = {439--453}, + issn = {1572-9095}, + doi = {10.1007/s10485-007-9081-8}, + abstract = {We make a definition of ω-precategory which should underlie any definition of weak ω-category. We make a precise definition of pseudo-invertible cells in this setting. We show that in an ω-precategory with all weak duals, every cell is pseudo-invertible. We deduce that in any “sensible” theory of ω-categories, an ω-category with all weak duals is an ω-groupoid. We discuss various examples and open questions involving higher-dimensional tangles and cobordisms.}, + langid = {english} +} + @unpublished{Cisinski24, title = {Formalization of higher categories}, author = {Denis-Charles Cisinski, Bastiaan Cnossen, Kim Nguyen and Tashi Walde}, @@ -566,21 +582,21 @@ @online{oeis date = {1996}, citeas = {OEIS}, url = {https://oeis.org}, - howpublished = {website}, + howpublished = {website} } @phdthesis{Qui16, - title = {Lawvere–Tierney sheafification in Homotopy Type Theory}, - author = {Quirin, Kevin}, - url = {https://kevinquirin.github.io/thesis/main.pdf}, - year = {2016}, - month = dec, - number = {2016EMNA0298}, - school = {École des Mines de Nantes}, + title = {Lawvere–Tierney sheafification in Homotopy Type Theory}, + author = {Quirin, Kevin}, + url = {https://kevinquirin.github.io/thesis/main.pdf}, + year = {2016}, + month = dec, + number = {2016EMNA0298}, + school = {École des Mines de Nantes}, abstract = {The main goal of this thesis is to define an extension of Gödel not-not translation to all truncated types, in the setting of homotopy type theory. This goal will use some existing theories, like Lawvere–Tierney sheaves theory in toposes, we will adapt in the setting of homotopy type theory. In particular, we will define a Lawvere–Tierney sheafification functor, which is the main theorem presented in this thesis. - To define it, we will need some concepts, either already defined in type theory, either not existing yet. In particular, we will define a theory of colimits over graphs as well as their truncated version, and the notion of truncated modalities, based on the existing definition of modalities. - Almost all the result presented in this thesis are formalized with the proof assistant Coq together with the library [HoTT/Coq].}, - langid = {english} + To define it, we will need some concepts, either already defined in type theory, either not existing yet. In particular, we will define a theory of colimits over graphs as well as their truncated version, and the notion of truncated modalities, based on the existing definition of modalities. + Almost all the result presented in this thesis are formalized with the proof assistant Coq together with the library [HoTT/Coq].}, + langid = {english} } @book{Rie17, diff --git a/src/foundation/globular-type-of-dependent-functions.lagda.md b/src/foundation/globular-type-of-dependent-functions.lagda.md index 6e46926464..c620d17ec1 100644 --- a/src/foundation/globular-type-of-dependent-functions.lagda.md +++ b/src/foundation/globular-type-of-dependent-functions.lagda.md @@ -33,10 +33,10 @@ globular structure on dependent function types. The globular type of dependent functions of a type family `B` over `A` is [reflexive](globular-types.reflexive-globular-types.md) and [transitive](globular-types.transitive-globular-types.md), so it is a -[noncoherent wild higher precategory](wild-category-theory.noncoherent-wild-higher-precategories.md). +[noncoherent ω-precategory](wild-category-theory.noncoherent-omega-precategories.md). The structures defined in this file are used to define the -[noncoherent large wild higher precategory of types](foundation.wild-category-of-types.md). +[wild category of types](foundation.wild-category-of-types.md). ## Definitions diff --git a/src/foundation/globular-type-of-functions.lagda.md b/src/foundation/globular-type-of-functions.lagda.md index 8680a71da9..41533c9aee 100644 --- a/src/foundation/globular-type-of-functions.lagda.md +++ b/src/foundation/globular-type-of-functions.lagda.md @@ -34,10 +34,10 @@ functions in terms of the The globular type of functions of a type family `B` over `A` is [reflexive](globular-types.reflexive-globular-types.md) and [transitive](globular-types.transitive-globular-types.md), so it is a -[noncoherent wild higher precategory](wild-category-theory.noncoherent-wild-higher-precategories.md). +[noncoherent ω-precategory](wild-category-theory.noncoherent-omega-precategories.md). The structures defined in this file are used to define the -[noncoherent large wild higher precategory of types](foundation.wild-category-of-types.md). +[large category of types](foundation.wild-category-of-types.md). ## Definitions diff --git a/src/foundation/wild-category-of-types.lagda.md b/src/foundation/wild-category-of-types.lagda.md index cf698e1a0f..60277a29a4 100644 --- a/src/foundation/wild-category-of-types.lagda.md +++ b/src/foundation/wild-category-of-types.lagda.md @@ -31,10 +31,8 @@ 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 +open import wild-category-theory.noncoherent-large-omega-precategories +open import wild-category-theory.noncoherent-omega-precategories ``` @@ -42,7 +40,7 @@ open import wild-category-theory.noncoherent-wild-higher-precategories ## Idea The -{{#concept "wild category of types" Agda=Type-Noncoherent-Large-Wild-Higher-Precategory}} +{{#concept "wild category of types" Agda=Type-Noncoherent-Large-ω-Precategory}} consists of types and [functions](foundation.dependent-function-types.md) and [homotopies](foundation-core.homotopies.md). @@ -92,18 +90,18 @@ is-transitive-Large-Transitive-Globular-Type is-transitive-Type-Large-Globular-Type ``` -### The noncoherent large wild higher precategory of types +### The noncoherent large ω-precategory of types ```agda -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-Noncoherent-Large-ω-Precategory : + Noncoherent-Large-ω-Precategory lsuc (_⊔_) +large-globular-type-Noncoherent-Large-ω-Precategory + Type-Noncoherent-Large-ω-Precategory = Type-Large-Globular-Type -id-structure-Noncoherent-Large-Wild-Higher-Precategory - Type-Noncoherent-Large-Wild-Higher-Precategory = +id-structure-Noncoherent-Large-ω-Precategory + Type-Noncoherent-Large-ω-Precategory = is-reflexive-Type-Large-Globular-Type -comp-structure-Noncoherent-Large-Wild-Higher-Precategory - Type-Noncoherent-Large-Wild-Higher-Precategory = +comp-structure-Noncoherent-Large-ω-Precategory + Type-Noncoherent-Large-ω-Precategory = is-transitive-Type-Large-Globular-Type ``` diff --git a/src/globular-types/reflexive-globular-types.lagda.md b/src/globular-types/reflexive-globular-types.lagda.md index c77e42f90d..8eec1e2951 100644 --- a/src/globular-types/reflexive-globular-types.lagda.md +++ b/src/globular-types/reflexive-globular-types.lagda.md @@ -327,6 +327,6 @@ module _ - [Colax reflexive globular maps](globular-types.colax-reflexive-globular-maps.md) - [Lax reflexive globular maps](globular-types.lax-reflexive-globular-maps.md) - [Reflexive globular maps](globular-types.reflexive-globular-maps.md) -- [Noncoherent wild higher precategories](wild-category-theory.noncoherent-wild-higher-precategories.md) +- [Noncoherent ω-precategories](wild-category-theory.noncoherent-omega-precategories.md) are globular types that are both reflexive and [transitive](globular-types.transitive-globular-types.md). diff --git a/src/globular-types/transitive-globular-types.lagda.md b/src/globular-types/transitive-globular-types.lagda.md index 8e50b2014f..368bad45fc 100644 --- a/src/globular-types/transitive-globular-types.lagda.md +++ b/src/globular-types/transitive-globular-types.lagda.md @@ -324,6 +324,6 @@ module _ ## See also - [Composition structure on globular types](globular-types.composition-structure-globular-types.md) -- [Noncoherent wild higher precategories](wild-category-theory.noncoherent-wild-higher-precategories.md) +- [Noncoherent ω-precategories](wild-category-theory.noncoherent-omega-precategories.md) are globular types that are both [reflexive](globular-types.reflexive-globular-types.md) and transitive. diff --git a/src/structured-types/wild-category-of-pointed-types.lagda.md b/src/structured-types/wild-category-of-pointed-types.lagda.md index a226d2cc41..3ff1429d27 100644 --- a/src/structured-types/wild-category-of-pointed-types.lagda.md +++ b/src/structured-types/wild-category-of-pointed-types.lagda.md @@ -32,8 +32,8 @@ open import structured-types.pointed-maps open import structured-types.pointed-types open import structured-types.uniform-pointed-homotopies -open import wild-category-theory.noncoherent-large-wild-higher-precategories -open import wild-category-theory.noncoherent-wild-higher-precategories +open import wild-category-theory.noncoherent-large-omega-precategories +open import wild-category-theory.noncoherent-omega-precategories ``` @@ -41,7 +41,7 @@ open import wild-category-theory.noncoherent-wild-higher-precategories ## Idea The -{{#concept "wild category of pointed types" Agda=uniform-pointed-type-Noncoherent-Large-Wild-Higher-Precategory Agda=pointed-type-Noncoherent-Large-Wild-Higher-Precategory}} +{{#concept "wild category of pointed types" Agda=uniform-pointed-type-Noncoherent-Large-ω-Precategory Agda=pointed-type-Noncoherent-Large-ω-Precategory}} consists of [pointed types](structured-types.pointed-types.md), [pointed functions](structured-types.pointed-maps.md), and [pointed homotopies](structured-types.pointed-homotopies.md). @@ -57,7 +57,7 @@ the higher cells are [identities](foundation-core.identity-types.md). ## Definitions -### The noncoherent large wild higher precategory of pointed types, pointed maps, and uniform pointed homotopies +### The noncoherent large ω-precategory of pointed types, pointed maps, and uniform pointed homotopies #### The large globular type of pointed types, pointed maps, and uniform pointed homotopies @@ -160,23 +160,23 @@ is-transitive-1-cell-globular-type-is-transitive-Large-Globular-Type is-transitive-uniform-pointed-Π-Globular-Type _ _ ``` -#### The noncoherent large wild higher precategory of pointed types, pointed maps, and uniform pointed homotopies +#### The noncoherent large ω-precategory of pointed types, pointed maps, and uniform pointed homotopies ```agda -uniform-pointed-type-Noncoherent-Large-Wild-Higher-Precategory : - Noncoherent-Large-Wild-Higher-Precategory lsuc (_⊔_) -large-globular-type-Noncoherent-Large-Wild-Higher-Precategory - uniform-pointed-type-Noncoherent-Large-Wild-Higher-Precategory = +uniform-pointed-type-Noncoherent-Large-ω-Precategory : + Noncoherent-Large-ω-Precategory lsuc (_⊔_) +large-globular-type-Noncoherent-Large-ω-Precategory + uniform-pointed-type-Noncoherent-Large-ω-Precategory = uniform-pointed-type-Large-Globular-Type -id-structure-Noncoherent-Large-Wild-Higher-Precategory - uniform-pointed-type-Noncoherent-Large-Wild-Higher-Precategory = +id-structure-Noncoherent-Large-ω-Precategory + uniform-pointed-type-Noncoherent-Large-ω-Precategory = id-structure-uniform-pointed-type-Large-Globular-Type -comp-structure-Noncoherent-Large-Wild-Higher-Precategory - uniform-pointed-type-Noncoherent-Large-Wild-Higher-Precategory = +comp-structure-Noncoherent-Large-ω-Precategory + uniform-pointed-type-Noncoherent-Large-ω-Precategory = comp-structure-uniform-pointed-type-Large-Globular-Type ``` -### The noncoherent large wild higher precategory of pointed types, pointed maps, and nonuniform homotopies +### The noncoherent large ω-precategory of pointed types, pointed maps, and nonuniform homotopies #### The large globular type of pointed types, pointed maps, and nonuniform pointed homotopies @@ -326,19 +326,19 @@ is-transitive-1-cell-globular-type-is-transitive-Large-Globular-Type is-transitive-pointed-map-Globular-Type _ _ ``` -#### The noncoherent large wild higher precategory of pointed types, pointed maps, and nonuniform pointed homotopies +#### The noncoherent large ω-precategory of pointed types, pointed maps, and nonuniform pointed homotopies ```agda -pointed-type-Noncoherent-Large-Wild-Higher-Precategory : - Noncoherent-Large-Wild-Higher-Precategory lsuc (_⊔_) -large-globular-type-Noncoherent-Large-Wild-Higher-Precategory - pointed-type-Noncoherent-Large-Wild-Higher-Precategory = +pointed-type-Noncoherent-Large-ω-Precategory : + Noncoherent-Large-ω-Precategory lsuc (_⊔_) +large-globular-type-Noncoherent-Large-ω-Precategory + pointed-type-Noncoherent-Large-ω-Precategory = pointed-type-Large-Globular-Type -id-structure-Noncoherent-Large-Wild-Higher-Precategory - pointed-type-Noncoherent-Large-Wild-Higher-Precategory = +id-structure-Noncoherent-Large-ω-Precategory + pointed-type-Noncoherent-Large-ω-Precategory = is-reflexive-pointed-type-Large-Globular-Type -comp-structure-Noncoherent-Large-Wild-Higher-Precategory - pointed-type-Noncoherent-Large-Wild-Higher-Precategory = +comp-structure-Noncoherent-Large-ω-Precategory + pointed-type-Noncoherent-Large-ω-Precategory = is-transitive-pointed-type-Large-Globular-Type ``` diff --git a/src/wild-category-theory.lagda.md b/src/wild-category-theory.lagda.md index 63cf266e2d..72cf1254d2 100644 --- a/src/wild-category-theory.lagda.md +++ b/src/wild-category-theory.lagda.md @@ -13,12 +13,12 @@ ```agda module wild-category-theory where -open import wild-category-theory.colax-functors-noncoherent-large-wild-higher-precategories public -open import wild-category-theory.colax-functors-noncoherent-wild-higher-precategories public -open import wild-category-theory.isomorphisms-in-noncoherent-large-wild-higher-precategories public -open import wild-category-theory.isomorphisms-in-noncoherent-wild-higher-precategories public -open import wild-category-theory.maps-noncoherent-large-wild-higher-precategories public -open import wild-category-theory.maps-noncoherent-wild-higher-precategories public -open import wild-category-theory.noncoherent-large-wild-higher-precategories public -open import wild-category-theory.noncoherent-wild-higher-precategories public +open import wild-category-theory.coinductive-isomorphisms-in-noncoherent-large-omega-precategories public +open import wild-category-theory.coinductive-isomorphisms-in-noncoherent-omega-precategories public +open import wild-category-theory.colax-functors-noncoherent-large-omega-precategories public +open import wild-category-theory.colax-functors-noncoherent-omega-precategories public +open import wild-category-theory.maps-noncoherent-large-omega-precategories public +open import wild-category-theory.maps-noncoherent-omega-precategories public +open import wild-category-theory.noncoherent-large-omega-precategories public +open import wild-category-theory.noncoherent-omega-precategories public ``` diff --git a/src/wild-category-theory/coinductive-isomorphisms-in-noncoherent-large-omega-precategories.lagda.md b/src/wild-category-theory/coinductive-isomorphisms-in-noncoherent-large-omega-precategories.lagda.md new file mode 100644 index 0000000000..303c5653ac --- /dev/null +++ b/src/wild-category-theory/coinductive-isomorphisms-in-noncoherent-large-omega-precategories.lagda.md @@ -0,0 +1,249 @@ +# Coinductive isomorphisms in noncoherent large ω-precategories + +```agda +{-# OPTIONS --guardedness #-} + +module wild-category-theory.coinductive-isomorphisms-in-noncoherent-large-omega-precategories where +``` + +
Imports + +```agda +open import foundation.dependent-pair-types +open import foundation.universe-levels + +open import wild-category-theory.coinductive-isomorphisms-in-noncoherent-omega-precategories +open import wild-category-theory.noncoherent-large-omega-precategories +``` + +
+ +## Idea + +Consider a +[noncoherent large ω-precategory](wild-category-theory.noncoherent-large-omega-precategories.md) +`𝒞`. A +{{#concept "coinductive isomorphism" Disambiguation="in noncoherent large ω-precategories" Agda=is-coinductive-iso-Noncoherent-Large-ω-Precategory}} +in `𝒞` is a morphism `f : x → y` in `𝒞` [equipped](foundation.structure.md) with + +- a morphism `s : 𝒞₁ y x` +- a $2$-morphism `η : 𝒞₂ id (f ∘ s)` +- a witness that `η` is itself a coinductive isomorphism +- another morphism `r : 𝒞₁ y x` +- a $2$-morphism `ε : 𝒞₂ (r ∘ f) id` +- a witness that `ε` is a coinductive isomorphism. + +Thus, the specified data is a commuting diagram of the form + +```text + y ========= y + \ ~⇓η ∧ \ + s \ /f \ r + ∨ / ~⇓ε ∨ + x ========= x +``` + +where `η` and `ε` again are coinductive isomorphisms in their respective +hom-ω-categories. + +> **Disclaimer.** We do not assert that the proposed definition of a coinductive +> isomorphism is fully coherent, and thus it may be subject to change in the +> future. + +While a noncoherent ω-precategory is the most general setting that allows us to +_define_ coinductive isomorphisms, the missing coherences obstruct us from +showing many of the expected properties. For example, we cannot show that all +identities are coinductive isomorphisms or that coinductive isomorphisms +compose. + +The concept of coinductive isomorphisms in ω-categories is strictly weaker than +the concept of _isomorphisms_. Indeed, the coindutive nature of this concept +allows us, in an informal sense, to indefinitely postpone constructing a witness +that `s` or `r` are "proper" inverses to `f`. To take an example, consider the +ω-category of spans and higher spans. In this ω-category every morphism is a +coinductive isomorphism since every morphism is a biadjoint, but not every +morphism is an isomorphism. Moreover, this ω-category is univalent with respect +to isomorphisms, but not with respect to all coinductive isomorphisms. More +generally, every morphism in an "ω-catgory with duals" is a coinductive +isomorphism {{#cite Cheng07}}. + +## Definitions + +### The predicate on morphisms of being coinductive isomorphisms + +```agda +record + is-coinductive-iso-Noncoherent-Large-ω-Precategory + {α : Level → Level} {β : Level → Level → Level} + (𝒞 : Noncoherent-Large-ω-Precategory α β) + {l1 : Level} {x : obj-Noncoherent-Large-ω-Precategory 𝒞 l1} + {l2 : Level} {y : obj-Noncoherent-Large-ω-Precategory 𝒞 l2} + (f : hom-Noncoherent-Large-ω-Precategory 𝒞 x y) + : UU (β l1 l1 ⊔ β l2 l1 ⊔ β l2 l2) + where + field + hom-section-is-coinductive-iso-Noncoherent-Large-ω-Precategory : + hom-Noncoherent-Large-ω-Precategory 𝒞 y x + + unit-is-coinductive-iso-Noncoherent-Large-ω-Precategory : + 2-hom-Noncoherent-Large-ω-Precategory 𝒞 + ( id-hom-Noncoherent-Large-ω-Precategory 𝒞) + ( comp-hom-Noncoherent-Large-ω-Precategory 𝒞 + ( f) + ( hom-section-is-coinductive-iso-Noncoherent-Large-ω-Precategory)) + + is-coinductive-iso-unit-is-coinductive-iso-Noncoherent-Large-ω-Precategory : + is-coinductive-iso-Noncoherent-ω-Precategory + ( hom-noncoherent-ω-precategory-Noncoherent-Large-ω-Precategory + ( 𝒞) + ( y) + ( y)) + ( unit-is-coinductive-iso-Noncoherent-Large-ω-Precategory) + + hom-retraction-is-coinductive-iso-Noncoherent-Large-ω-Precategory : + hom-Noncoherent-Large-ω-Precategory 𝒞 y x + + counit-is-coinductive-iso-Noncoherent-Large-ω-Precategory : + 2-hom-Noncoherent-Large-ω-Precategory 𝒞 + ( comp-hom-Noncoherent-Large-ω-Precategory 𝒞 + ( hom-retraction-is-coinductive-iso-Noncoherent-Large-ω-Precategory) + ( f)) + ( id-hom-Noncoherent-Large-ω-Precategory 𝒞) + + is-coinductive-iso-counit-is-coinductive-iso-Noncoherent-Large-ω-Precategory : + is-coinductive-iso-Noncoherent-ω-Precategory + ( hom-noncoherent-ω-precategory-Noncoherent-Large-ω-Precategory + ( 𝒞) + ( x) + ( x)) + ( counit-is-coinductive-iso-Noncoherent-Large-ω-Precategory) + +open is-coinductive-iso-Noncoherent-Large-ω-Precategory public +``` + +### Coinductive isomorphisms in a noncoherent large ω-precategory + +```agda +coinductive-iso-Noncoherent-Large-ω-Precategory : + {α : Level → Level} {β : Level → Level → Level} + (𝒞 : Noncoherent-Large-ω-Precategory α β) + {l1 : Level} (x : obj-Noncoherent-Large-ω-Precategory 𝒞 l1) + {l2 : Level} (y : obj-Noncoherent-Large-ω-Precategory 𝒞 l2) → + UU (β l1 l1 ⊔ β l1 l2 ⊔ β l2 l1 ⊔ β l2 l2) +coinductive-iso-Noncoherent-Large-ω-Precategory 𝒞 x y = + Σ ( hom-Noncoherent-Large-ω-Precategory 𝒞 x y) + ( is-coinductive-iso-Noncoherent-Large-ω-Precategory 𝒞) +``` + +### Components of a coinductive isomorphism in a noncoherent large ω-precategory + +```agda +module _ + {α : Level → Level} {β : Level → Level → Level} + {𝒞 : Noncoherent-Large-ω-Precategory α β} + {l1 : Level} {x : obj-Noncoherent-Large-ω-Precategory 𝒞 l1} + {l2 : Level} {y : obj-Noncoherent-Large-ω-Precategory 𝒞 l2} + (f : coinductive-iso-Noncoherent-Large-ω-Precategory 𝒞 x y) + where + + hom-coinductive-iso-Noncoherent-Large-ω-Precategory : + hom-Noncoherent-Large-ω-Precategory 𝒞 x y + hom-coinductive-iso-Noncoherent-Large-ω-Precategory = pr1 f + + is-coinductive-iso-hom-coinductive-iso-Noncoherent-Large-ω-Precategory : + is-coinductive-iso-Noncoherent-Large-ω-Precategory 𝒞 + ( hom-coinductive-iso-Noncoherent-Large-ω-Precategory) + is-coinductive-iso-hom-coinductive-iso-Noncoherent-Large-ω-Precategory = pr2 f + + hom-section-coinductive-iso-Noncoherent-Large-ω-Precategory : + hom-Noncoherent-Large-ω-Precategory 𝒞 y x + hom-section-coinductive-iso-Noncoherent-Large-ω-Precategory = + hom-section-is-coinductive-iso-Noncoherent-Large-ω-Precategory + ( is-coinductive-iso-hom-coinductive-iso-Noncoherent-Large-ω-Precategory) + + unit-coinductive-iso-Noncoherent-Large-ω-Precategory : + 2-hom-Noncoherent-Large-ω-Precategory 𝒞 + ( id-hom-Noncoherent-Large-ω-Precategory 𝒞) + ( comp-hom-Noncoherent-Large-ω-Precategory 𝒞 + ( hom-coinductive-iso-Noncoherent-Large-ω-Precategory) + ( hom-section-coinductive-iso-Noncoherent-Large-ω-Precategory)) + unit-coinductive-iso-Noncoherent-Large-ω-Precategory = + unit-is-coinductive-iso-Noncoherent-Large-ω-Precategory + ( is-coinductive-iso-hom-coinductive-iso-Noncoherent-Large-ω-Precategory) + + is-coinductive-iso-unit-coinductive-iso-Noncoherent-Large-ω-Precategory : + is-coinductive-iso-Noncoherent-ω-Precategory + ( hom-noncoherent-ω-precategory-Noncoherent-Large-ω-Precategory + ( 𝒞) + ( y) + ( y)) + ( unit-coinductive-iso-Noncoherent-Large-ω-Precategory) + is-coinductive-iso-unit-coinductive-iso-Noncoherent-Large-ω-Precategory = + is-coinductive-iso-unit-is-coinductive-iso-Noncoherent-Large-ω-Precategory + ( is-coinductive-iso-hom-coinductive-iso-Noncoherent-Large-ω-Precategory) + + coinductive-iso-unit-coinductive-iso-Noncoherent-Large-ω-Precategory : + coinductive-iso-Noncoherent-ω-Precategory + ( hom-noncoherent-ω-precategory-Noncoherent-Large-ω-Precategory + ( 𝒞) + ( y) + ( y)) + ( id-hom-Noncoherent-Large-ω-Precategory 𝒞) + ( comp-hom-Noncoherent-Large-ω-Precategory 𝒞 + ( hom-coinductive-iso-Noncoherent-Large-ω-Precategory) + ( hom-section-coinductive-iso-Noncoherent-Large-ω-Precategory)) + pr1 coinductive-iso-unit-coinductive-iso-Noncoherent-Large-ω-Precategory = + unit-coinductive-iso-Noncoherent-Large-ω-Precategory + pr2 coinductive-iso-unit-coinductive-iso-Noncoherent-Large-ω-Precategory = + is-coinductive-iso-unit-coinductive-iso-Noncoherent-Large-ω-Precategory + + hom-retraction-coinductive-iso-Noncoherent-Large-ω-Precategory : + hom-Noncoherent-Large-ω-Precategory 𝒞 y x + hom-retraction-coinductive-iso-Noncoherent-Large-ω-Precategory = + hom-retraction-is-coinductive-iso-Noncoherent-Large-ω-Precategory + ( is-coinductive-iso-hom-coinductive-iso-Noncoherent-Large-ω-Precategory) + + counit-coinductive-iso-Noncoherent-Large-ω-Precategory : + 2-hom-Noncoherent-Large-ω-Precategory 𝒞 + ( comp-hom-Noncoherent-Large-ω-Precategory 𝒞 + ( hom-retraction-coinductive-iso-Noncoherent-Large-ω-Precategory) + ( hom-coinductive-iso-Noncoherent-Large-ω-Precategory)) + ( id-hom-Noncoherent-Large-ω-Precategory 𝒞) + counit-coinductive-iso-Noncoherent-Large-ω-Precategory = + counit-is-coinductive-iso-Noncoherent-Large-ω-Precategory + ( is-coinductive-iso-hom-coinductive-iso-Noncoherent-Large-ω-Precategory) + + is-coinductive-iso-counit-coinductive-iso-Noncoherent-Large-ω-Precategory : + is-coinductive-iso-Noncoherent-ω-Precategory + ( hom-noncoherent-ω-precategory-Noncoherent-Large-ω-Precategory + ( 𝒞) + ( x) + ( x)) + ( counit-coinductive-iso-Noncoherent-Large-ω-Precategory) + is-coinductive-iso-counit-coinductive-iso-Noncoherent-Large-ω-Precategory = + is-coinductive-iso-counit-is-coinductive-iso-Noncoherent-Large-ω-Precategory + ( is-coinductive-iso-hom-coinductive-iso-Noncoherent-Large-ω-Precategory) + + coinductive-iso-counit-coinductive-iso-Noncoherent-Large-ω-Precategory : + coinductive-iso-Noncoherent-ω-Precategory + ( hom-noncoherent-ω-precategory-Noncoherent-Large-ω-Precategory + ( 𝒞) + ( x) + ( x)) + ( comp-hom-Noncoherent-Large-ω-Precategory 𝒞 + ( hom-retraction-coinductive-iso-Noncoherent-Large-ω-Precategory) + ( hom-coinductive-iso-Noncoherent-Large-ω-Precategory)) + ( id-hom-Noncoherent-Large-ω-Precategory 𝒞) + pr1 coinductive-iso-counit-coinductive-iso-Noncoherent-Large-ω-Precategory = + counit-coinductive-iso-Noncoherent-Large-ω-Precategory + pr2 coinductive-iso-counit-coinductive-iso-Noncoherent-Large-ω-Precategory = + is-coinductive-iso-counit-coinductive-iso-Noncoherent-Large-ω-Precategory +``` + +## See also + +- [Coinductive isomorphisms in noncoherent ω-precategories](wild-category-theory.coinductive-isomorphisms-in-noncoherent-omega-precategories.md) + +## References + +{{#bibliography}} diff --git a/src/wild-category-theory/coinductive-isomorphisms-in-noncoherent-omega-precategories.lagda.md b/src/wild-category-theory/coinductive-isomorphisms-in-noncoherent-omega-precategories.lagda.md new file mode 100644 index 0000000000..c2494822ea --- /dev/null +++ b/src/wild-category-theory/coinductive-isomorphisms-in-noncoherent-omega-precategories.lagda.md @@ -0,0 +1,243 @@ +# Coinductive isomorphisms in noncoherent ω-precategories + +```agda +{-# OPTIONS --guardedness #-} + +module wild-category-theory.coinductive-isomorphisms-in-noncoherent-omega-precategories where +``` + +
Imports + +```agda +open import foundation.dependent-pair-types +open import foundation.universe-levels + +open import wild-category-theory.noncoherent-omega-precategories +``` + +
+ +## Idea + +Consider a +[noncoherent ω-precategory](wild-category-theory.noncoherent-omega-precategories.md) +`𝒞`. A +{{#concept "coinductive isomorphism" Disambiguation="in noncoherent ω-precategories" Agda=is-coinductive-iso-Noncoherent-ω-Precategory}} +in `𝒞` is a morphism `f : 𝒞₁ x y` [equipped](foundation.structure.md) with, +coinductively, + +- a morphism `s : 𝒞₁ y x` +- a $2$-morphism `η : 𝒞₂ id (f ∘ s)` +- a witness that `η` is itself a coinductive isomorphism +- another morphism `r : 𝒞₁ y x` +- a $2$-morphism `ε : 𝒞₂ (r ∘ f) id` +- a witness that `ε` is a coinductive isomorphism. + +Thus, the specified data is a commuting diagram of the form + +```text + y ========= y + \ ~⇓η ∧ \ + s \ /f \ r + ∨ / ~⇓ε ∨ + x ========= x +``` + +where `η` and `ε` again are coinductive isomorphisms in their respective +hom-ω-categories. + +> **Disclaimer.** We do not assert that the proposed definition of a coinductive +> isomorphism is fully coherent, and thus it may be subject to change in the +> future. + +While a noncoherent ω-precategory is the most general setting that allows us to +_define_ coinductive isomorphisms, the missing coherences obstruct us from +showing many of the expected properties. For example, we cannot show that all +identities are coinductive isomorphisms or that coinductive isomorphisms +compose. + +The concept of coinductive isomorphisms in ω-categories is strictly weaker than +the concept of _isomorphisms_. Indeed, the coindutive nature of this concept +allows us, in an informal sense, to indefinitely postpone constructing a witness +that `s` or `r` are "proper" inverses to `f`. To take an example, consider the +ω-category of spans and higher spans. In this ω-category every morphism is a +coinductive isomorphism since every morphism is a biadjoint, but not every +morphism is an isomorphism. Moreover, this ω-category is univalent with respect +to isomorphisms, but not with respect to all coinductive isomorphisms. More +generally, every morphism in an "ω-catgory with duals" is a coinductive +isomorphism {{#cite Cheng07}}. + +## Definitions + +### The predicate on morphisms of being coinductive isomorphisms + +```agda +record + is-coinductive-iso-Noncoherent-ω-Precategory + {l1 l2 : Level} (𝒞 : Noncoherent-ω-Precategory l1 l2) + {x y : obj-Noncoherent-ω-Precategory 𝒞} + (f : hom-Noncoherent-ω-Precategory 𝒞 x y) : UU l2 + where + coinductive + field + hom-section-is-coinductive-iso-Noncoherent-ω-Precategory : + hom-Noncoherent-ω-Precategory 𝒞 y x + + unit-is-coinductive-iso-Noncoherent-ω-Precategory : + 2-hom-Noncoherent-ω-Precategory 𝒞 + ( id-hom-Noncoherent-ω-Precategory 𝒞) + ( comp-hom-Noncoherent-ω-Precategory 𝒞 + ( f) + ( hom-section-is-coinductive-iso-Noncoherent-ω-Precategory)) + + is-coinductive-iso-unit-is-coinductive-iso-Noncoherent-ω-Precategory : + is-coinductive-iso-Noncoherent-ω-Precategory + ( hom-noncoherent-ω-precategory-Noncoherent-ω-Precategory + ( 𝒞) + ( y) + ( y)) + ( unit-is-coinductive-iso-Noncoherent-ω-Precategory) + + hom-retraction-is-coinductive-iso-Noncoherent-ω-Precategory : + hom-Noncoherent-ω-Precategory 𝒞 y x + + counit-is-coinductive-iso-Noncoherent-ω-Precategory : + 2-hom-Noncoherent-ω-Precategory 𝒞 + ( comp-hom-Noncoherent-ω-Precategory 𝒞 + ( hom-retraction-is-coinductive-iso-Noncoherent-ω-Precategory) + ( f)) + ( id-hom-Noncoherent-ω-Precategory 𝒞) + + is-coinductive-iso-counit-is-coinductive-iso-Noncoherent-ω-Precategory : + is-coinductive-iso-Noncoherent-ω-Precategory + ( hom-noncoherent-ω-precategory-Noncoherent-ω-Precategory + ( 𝒞) + ( x) + ( x)) + ( counit-is-coinductive-iso-Noncoherent-ω-Precategory) + +open is-coinductive-iso-Noncoherent-ω-Precategory public +``` + +### Coinductive isomorphisms in a noncoherent ω-precategory + +```agda +coinductive-iso-Noncoherent-ω-Precategory : + {l1 l2 : Level} (𝒞 : Noncoherent-ω-Precategory l1 l2) + (x y : obj-Noncoherent-ω-Precategory 𝒞) → + UU l2 +coinductive-iso-Noncoherent-ω-Precategory 𝒞 x y = + Σ ( hom-Noncoherent-ω-Precategory 𝒞 x y) + ( is-coinductive-iso-Noncoherent-ω-Precategory 𝒞) +``` + +### Components of a coinductive isomorphism in a noncoherent ω-precategory + +```agda +module _ + {l1 l2 : Level} {𝒞 : Noncoherent-ω-Precategory l1 l2} + {x y : obj-Noncoherent-ω-Precategory 𝒞} + (f : coinductive-iso-Noncoherent-ω-Precategory 𝒞 x y) + where + + hom-coinductive-iso-Noncoherent-ω-Precategory : + hom-Noncoherent-ω-Precategory 𝒞 x y + hom-coinductive-iso-Noncoherent-ω-Precategory = pr1 f + + is-coinductive-iso-hom-coinductive-iso-Noncoherent-ω-Precategory : + is-coinductive-iso-Noncoherent-ω-Precategory 𝒞 + ( hom-coinductive-iso-Noncoherent-ω-Precategory) + is-coinductive-iso-hom-coinductive-iso-Noncoherent-ω-Precategory = pr2 f + + hom-section-coinductive-iso-Noncoherent-ω-Precategory : + hom-Noncoherent-ω-Precategory 𝒞 y x + hom-section-coinductive-iso-Noncoherent-ω-Precategory = + hom-section-is-coinductive-iso-Noncoherent-ω-Precategory + ( is-coinductive-iso-hom-coinductive-iso-Noncoherent-ω-Precategory) + + unit-coinductive-iso-Noncoherent-ω-Precategory : + 2-hom-Noncoherent-ω-Precategory 𝒞 + ( id-hom-Noncoherent-ω-Precategory 𝒞) + ( comp-hom-Noncoherent-ω-Precategory 𝒞 + ( hom-coinductive-iso-Noncoherent-ω-Precategory) + ( hom-section-coinductive-iso-Noncoherent-ω-Precategory)) + unit-coinductive-iso-Noncoherent-ω-Precategory = + unit-is-coinductive-iso-Noncoherent-ω-Precategory + ( is-coinductive-iso-hom-coinductive-iso-Noncoherent-ω-Precategory) + + is-coinductive-iso-unit-coinductive-iso-Noncoherent-ω-Precategory : + is-coinductive-iso-Noncoherent-ω-Precategory + ( hom-noncoherent-ω-precategory-Noncoherent-ω-Precategory + ( 𝒞) + ( y) + ( y)) + ( unit-coinductive-iso-Noncoherent-ω-Precategory) + is-coinductive-iso-unit-coinductive-iso-Noncoherent-ω-Precategory = + is-coinductive-iso-unit-is-coinductive-iso-Noncoherent-ω-Precategory + ( is-coinductive-iso-hom-coinductive-iso-Noncoherent-ω-Precategory) + + coinductive-iso-unit-coinductive-iso-Noncoherent-ω-Precategory : + coinductive-iso-Noncoherent-ω-Precategory + ( hom-noncoherent-ω-precategory-Noncoherent-ω-Precategory + ( 𝒞) + ( y) + ( y)) + ( id-hom-Noncoherent-ω-Precategory 𝒞) + ( comp-hom-Noncoherent-ω-Precategory 𝒞 + ( hom-coinductive-iso-Noncoherent-ω-Precategory) + ( hom-section-coinductive-iso-Noncoherent-ω-Precategory)) + pr1 coinductive-iso-unit-coinductive-iso-Noncoherent-ω-Precategory = + unit-coinductive-iso-Noncoherent-ω-Precategory + pr2 coinductive-iso-unit-coinductive-iso-Noncoherent-ω-Precategory = + is-coinductive-iso-unit-coinductive-iso-Noncoherent-ω-Precategory + + hom-retraction-coinductive-iso-Noncoherent-ω-Precategory : + hom-Noncoherent-ω-Precategory 𝒞 y x + hom-retraction-coinductive-iso-Noncoherent-ω-Precategory = + hom-retraction-is-coinductive-iso-Noncoherent-ω-Precategory + ( is-coinductive-iso-hom-coinductive-iso-Noncoherent-ω-Precategory) + + counit-coinductive-iso-Noncoherent-ω-Precategory : + 2-hom-Noncoherent-ω-Precategory 𝒞 + ( comp-hom-Noncoherent-ω-Precategory 𝒞 + ( hom-retraction-coinductive-iso-Noncoherent-ω-Precategory) + ( hom-coinductive-iso-Noncoherent-ω-Precategory)) + ( id-hom-Noncoherent-ω-Precategory 𝒞) + counit-coinductive-iso-Noncoherent-ω-Precategory = + counit-is-coinductive-iso-Noncoherent-ω-Precategory + ( is-coinductive-iso-hom-coinductive-iso-Noncoherent-ω-Precategory) + + is-coinductive-iso-counit-coinductive-iso-Noncoherent-ω-Precategory : + is-coinductive-iso-Noncoherent-ω-Precategory + ( hom-noncoherent-ω-precategory-Noncoherent-ω-Precategory + ( 𝒞) + ( x) + ( x)) + ( counit-coinductive-iso-Noncoherent-ω-Precategory) + is-coinductive-iso-counit-coinductive-iso-Noncoherent-ω-Precategory = + is-coinductive-iso-counit-is-coinductive-iso-Noncoherent-ω-Precategory + ( is-coinductive-iso-hom-coinductive-iso-Noncoherent-ω-Precategory) + + coinductive-iso-counit-coinductive-iso-Noncoherent-ω-Precategory : + coinductive-iso-Noncoherent-ω-Precategory + ( hom-noncoherent-ω-precategory-Noncoherent-ω-Precategory + ( 𝒞) + ( x) + ( x)) + ( comp-hom-Noncoherent-ω-Precategory 𝒞 + ( hom-retraction-coinductive-iso-Noncoherent-ω-Precategory) + ( hom-coinductive-iso-Noncoherent-ω-Precategory)) + ( id-hom-Noncoherent-ω-Precategory 𝒞) + pr1 coinductive-iso-counit-coinductive-iso-Noncoherent-ω-Precategory = + counit-coinductive-iso-Noncoherent-ω-Precategory + pr2 coinductive-iso-counit-coinductive-iso-Noncoherent-ω-Precategory = + is-coinductive-iso-counit-coinductive-iso-Noncoherent-ω-Precategory +``` + +## See also + +- [Coinductive isomorphisms in noncoherent large ω-precategories](wild-category-theory.coinductive-isomorphisms-in-noncoherent-large-omega-precategories.md) + +## References + +{{#bibliography}} diff --git a/src/wild-category-theory/colax-functors-noncoherent-large-omega-precategories.lagda.md b/src/wild-category-theory/colax-functors-noncoherent-large-omega-precategories.lagda.md new file mode 100644 index 0000000000..714375f4a2 --- /dev/null +++ b/src/wild-category-theory/colax-functors-noncoherent-large-omega-precategories.lagda.md @@ -0,0 +1,552 @@ +# Colax functors between large noncoherent ω-precategories + +```agda +{-# OPTIONS --guardedness #-} + +module wild-category-theory.colax-functors-noncoherent-large-omega-precategories where +``` + +
Imports + +```agda +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-omega-precategories +open import wild-category-theory.maps-noncoherent-large-omega-precategories +open import wild-category-theory.maps-noncoherent-omega-precategories +open import wild-category-theory.noncoherent-large-omega-precategories +open import wild-category-theory.noncoherent-omega-precategories +``` + +
+ +## Idea + +A +{{#concept "colax functor" Disambiguation="between noncoherent large ω-precategories" Agda=colax-functor-Noncoherent-Large-ω-Precategory}} +`f` between +[noncoherent large ω-precategories](wild-category-theory.noncoherent-large-omega-precategories.md) +`𝒜` and `ℬ` is a +[map of noncoherent large ω-precategories](wild-category-theory.maps-noncoherent-large-omega-precategories.md) +that preserves identity morphisms and composition _colaxly_. This means that for +every $n$-morphism `f` in `𝒜`, where we take $0$-morphisms to be objects, there +is an $(n+1)$-morphism + +```text + Fₙ₊₁ (id-hom 𝒜 f) ⇒ id-hom ℬ (Fₙ f) +``` + +in `ℬ`, and for every pair of composable $(n+1)$-morphisms `g` after `f` in `𝒜`, +there is an $(n+2)$-morphism + +```text + Fₙ₊₁ (g ∘ f) ⇒ (Fₙ₊₁ g) ∘ (Fₙ₊₁ f) +``` + +in `ℬ`. + +## Definitions + +### The predicate on maps between large noncoherent ω-precategories of preserving the identity structure + +```agda +preserves-id-structure-map-Noncoherent-Large-ω-Precategory : + {α1 α2 γ : Level → Level} + {β1 β2 : Level → Level → Level} + (𝒜 : Noncoherent-Large-ω-Precategory α1 β1) + (ℬ : Noncoherent-Large-ω-Precategory α2 β2) + (F : map-Noncoherent-Large-ω-Precategory γ 𝒜 ℬ) → UUω +preserves-id-structure-map-Noncoherent-Large-ω-Precategory 𝒜 ℬ F = + is-colax-reflexive-large-globular-map + ( large-reflexive-globular-type-Noncoherent-Large-ω-Precategory + 𝒜) + ( large-reflexive-globular-type-Noncoherent-Large-ω-Precategory + ℬ) + ( F) +``` + +### The predicate on maps between large noncoherent ω-precategories of preserving the composition structure + +```agda +preserves-comp-structure-map-Noncoherent-Large-ω-Precategory : + {α1 α2 γ : Level → Level} + {β1 β2 : Level → Level → Level} + (𝒜 : Noncoherent-Large-ω-Precategory α1 β1) + (ℬ : Noncoherent-Large-ω-Precategory α2 β2) + (F : map-Noncoherent-Large-ω-Precategory γ 𝒜 ℬ) → UUω +preserves-comp-structure-map-Noncoherent-Large-ω-Precategory 𝒜 ℬ F = + is-colax-transitive-large-globular-map + ( large-transitive-globular-type-Noncoherent-Large-ω-Precategory + 𝒜) + ( large-transitive-globular-type-Noncoherent-Large-ω-Precategory + ℬ) + ( F) +``` + +### The predicate of being a colax functor between noncoherent ω-precategories + +```agda +record + is-colax-functor-Noncoherent-Large-ω-Precategory + {α1 α2 : Level → Level} + {β1 β2 : Level → Level → Level} + {γ : Level → Level} + (𝒜 : Noncoherent-Large-ω-Precategory α1 β1) + (ℬ : Noncoherent-Large-ω-Precategory α2 β2) + (F : map-Noncoherent-Large-ω-Precategory γ 𝒜 ℬ) : UUω + where + + constructor + make-is-colax-functor-Noncoherent-Large-ω-Precategory + + field + preserves-id-structure-is-colax-functor-Noncoherent-Large-ω-Precategory : + preserves-id-structure-map-Noncoherent-Large-ω-Precategory + ( 𝒜) + ( ℬ) + ( F) + + field + preserves-comp-structure-is-colax-functor-Noncoherent-Large-ω-Precategory : + preserves-comp-structure-map-Noncoherent-Large-ω-Precategory + ( 𝒜) + ( ℬ) + ( F) + + preserves-id-hom-is-colax-functor-Noncoherent-Large-ω-Precategory : + {l : Level} + (x : obj-Noncoherent-Large-ω-Precategory 𝒜 l) → + 2-hom-Noncoherent-Large-ω-Precategory ℬ + ( hom-map-Noncoherent-Large-ω-Precategory 𝒜 ℬ F + ( id-hom-Noncoherent-Large-ω-Precategory 𝒜 {x = x})) + ( id-hom-Noncoherent-Large-ω-Precategory ℬ + { x = obj-map-Noncoherent-Large-ω-Precategory 𝒜 ℬ F x}) + preserves-id-hom-is-colax-functor-Noncoherent-Large-ω-Precategory = + preserves-refl-1-cell-is-colax-reflexive-large-globular-map + preserves-id-structure-is-colax-functor-Noncoherent-Large-ω-Precategory + + preserves-id-structure-hom-is-colax-functor-Noncoherent-Large-ω-Precategory : + {l1 l2 : Level} + {x : obj-Noncoherent-Large-ω-Precategory 𝒜 l1} + {y : obj-Noncoherent-Large-ω-Precategory 𝒜 l2} → + preserves-id-structure-map-Noncoherent-ω-Precategory + ( hom-noncoherent-ω-precategory-Noncoherent-Large-ω-Precategory + 𝒜 x y) + ( hom-noncoherent-ω-precategory-Noncoherent-Large-ω-Precategory + ℬ _ _) + ( 1-cell-globular-map-large-globular-map F) + preserves-id-structure-hom-is-colax-functor-Noncoherent-Large-ω-Precategory = + is-colax-reflexive-1-cell-globular-map-is-colax-reflexive-large-globular-map + preserves-id-structure-is-colax-functor-Noncoherent-Large-ω-Precategory + + preserves-comp-hom-is-colax-functor-Noncoherent-Large-ω-Precategory : + {l1 l2 l3 : Level} + {x : obj-Noncoherent-Large-ω-Precategory 𝒜 l1} + {y : obj-Noncoherent-Large-ω-Precategory 𝒜 l2} + {z : obj-Noncoherent-Large-ω-Precategory 𝒜 l3} + (g : hom-Noncoherent-Large-ω-Precategory 𝒜 y z) + (f : hom-Noncoherent-Large-ω-Precategory 𝒜 x y) → + 2-hom-Noncoherent-Large-ω-Precategory ℬ + ( hom-map-Noncoherent-Large-ω-Precategory 𝒜 ℬ F + ( comp-hom-Noncoherent-Large-ω-Precategory 𝒜 g f)) + ( comp-hom-Noncoherent-Large-ω-Precategory ℬ + ( hom-map-Noncoherent-Large-ω-Precategory 𝒜 ℬ F g) + ( hom-map-Noncoherent-Large-ω-Precategory 𝒜 ℬ F f)) + preserves-comp-hom-is-colax-functor-Noncoherent-Large-ω-Precategory = + preserves-comp-1-cell-is-colax-transitive-large-globular-map + preserves-comp-structure-is-colax-functor-Noncoherent-Large-ω-Precategory + + preserves-comp-structure-hom-is-colax-functor-Noncoherent-Large-ω-Precategory : + {l1 l2 : Level} + {x : obj-Noncoherent-Large-ω-Precategory 𝒜 l1} + {y : obj-Noncoherent-Large-ω-Precategory 𝒜 l2} → + preserves-comp-structure-map-Noncoherent-ω-Precategory + ( hom-noncoherent-ω-precategory-Noncoherent-Large-ω-Precategory + 𝒜 x y) + ( hom-noncoherent-ω-precategory-Noncoherent-Large-ω-Precategory + ℬ _ _) + ( 1-cell-globular-map-large-globular-map F) + preserves-comp-structure-hom-is-colax-functor-Noncoherent-Large-ω-Precategory = + is-colax-transitive-1-cell-globular-map-is-colax-transitive-large-globular-map + preserves-comp-structure-is-colax-functor-Noncoherent-Large-ω-Precategory + + is-colax-functor-hom-is-colax-functor-map-Noncoherent-Large-ω-Precategory : + {l1 l2 : Level} + {x : obj-Noncoherent-Large-ω-Precategory 𝒜 l1} + {y : obj-Noncoherent-Large-ω-Precategory 𝒜 l2} → + is-colax-functor-Noncoherent-ω-Precategory + ( hom-noncoherent-ω-precategory-Noncoherent-Large-ω-Precategory + 𝒜 x y) + ( hom-noncoherent-ω-precategory-Noncoherent-Large-ω-Precategory + ℬ _ _) + ( 1-cell-globular-map-large-globular-map F) + is-colax-functor-hom-is-colax-functor-map-Noncoherent-Large-ω-Precategory = + make-is-colax-functor-Noncoherent-ω-Precategory + preserves-id-structure-hom-is-colax-functor-Noncoherent-Large-ω-Precategory + preserves-comp-structure-hom-is-colax-functor-Noncoherent-Large-ω-Precategory + +open is-colax-functor-Noncoherent-Large-ω-Precategory public +``` + +### The type of colax functors between noncoherent ω-precategories + +```agda +record + colax-functor-Noncoherent-Large-ω-Precategory + {α1 α2 : Level → Level} + {β1 β2 : Level → Level → Level} + (δ : Level → Level) + (𝒜 : Noncoherent-Large-ω-Precategory α1 β1) + (ℬ : Noncoherent-Large-ω-Precategory α2 β2) : UUω + where + + constructor + make-colax-functor-Noncoherent-Large-ω-Precategory +``` + +The underlying large globular map of a colax functor: + +```agda + field + map-colax-functor-Noncoherent-Large-ω-Precategory : + map-Noncoherent-Large-ω-Precategory δ 𝒜 ℬ + + obj-colax-functor-Noncoherent-Large-ω-Precategory : + {l : Level} → + obj-Noncoherent-Large-ω-Precategory 𝒜 l → + obj-Noncoherent-Large-ω-Precategory ℬ (δ l) + obj-colax-functor-Noncoherent-Large-ω-Precategory = + obj-map-Noncoherent-Large-ω-Precategory 𝒜 ℬ + ( map-colax-functor-Noncoherent-Large-ω-Precategory) + + hom-colax-functor-Noncoherent-Large-ω-Precategory : + {l1 l2 : Level} + {x : obj-Noncoherent-Large-ω-Precategory 𝒜 l1} + {y : obj-Noncoherent-Large-ω-Precategory 𝒜 l2} → + hom-Noncoherent-Large-ω-Precategory 𝒜 x y → + hom-Noncoherent-Large-ω-Precategory ℬ + ( obj-colax-functor-Noncoherent-Large-ω-Precategory x) + ( obj-colax-functor-Noncoherent-Large-ω-Precategory y) + hom-colax-functor-Noncoherent-Large-ω-Precategory = + hom-map-Noncoherent-Large-ω-Precategory 𝒜 ℬ + map-colax-functor-Noncoherent-Large-ω-Precategory + + 2-hom-colax-functor-Noncoherent-Large-ω-Precategory : + {l1 l2 : Level} + {x : obj-Noncoherent-Large-ω-Precategory 𝒜 l1} + {y : obj-Noncoherent-Large-ω-Precategory 𝒜 l2} + {f g : hom-Noncoherent-Large-ω-Precategory 𝒜 x y} → + 2-hom-Noncoherent-Large-ω-Precategory 𝒜 f g → + 2-hom-Noncoherent-Large-ω-Precategory ℬ + ( hom-colax-functor-Noncoherent-Large-ω-Precategory f) + ( hom-colax-functor-Noncoherent-Large-ω-Precategory g) + 2-hom-colax-functor-Noncoherent-Large-ω-Precategory = + 2-hom-map-Noncoherent-Large-ω-Precategory 𝒜 ℬ + map-colax-functor-Noncoherent-Large-ω-Precategory + + hom-globular-map-colax-functor-Noncoherent-Large-ω-Precategory : + {l1 l2 : Level} + {x : obj-Noncoherent-Large-ω-Precategory 𝒜 l1} + {y : obj-Noncoherent-Large-ω-Precategory 𝒜 l2} → + globular-map + ( hom-globular-type-Noncoherent-Large-ω-Precategory 𝒜 x y) + ( hom-globular-type-Noncoherent-Large-ω-Precategory ℬ + ( obj-colax-functor-Noncoherent-Large-ω-Precategory x) + ( obj-colax-functor-Noncoherent-Large-ω-Precategory y)) + hom-globular-map-colax-functor-Noncoherent-Large-ω-Precategory = + hom-globular-map-map-Noncoherent-Large-ω-Precategory 𝒜 ℬ + ( map-colax-functor-Noncoherent-Large-ω-Precategory) + + field + is-colax-functor-colax-functor-Noncoherent-Large-ω-Precategory : + is-colax-functor-Noncoherent-Large-ω-Precategory 𝒜 ℬ + ( map-colax-functor-Noncoherent-Large-ω-Precategory) +``` + +Preservation of the identity structure: + +```agda + preserves-id-structure-colax-functor-Noncoherent-Large-ω-Precategory : + preserves-id-structure-map-Noncoherent-Large-ω-Precategory 𝒜 ℬ + map-colax-functor-Noncoherent-Large-ω-Precategory + preserves-id-structure-colax-functor-Noncoherent-Large-ω-Precategory = + preserves-id-structure-is-colax-functor-Noncoherent-Large-ω-Precategory + is-colax-functor-colax-functor-Noncoherent-Large-ω-Precategory + + colax-reflexive-map-colax-functor-Noncoherent-Large-ω-Precategory : + large-colax-reflexive-globular-map δ + ( large-reflexive-globular-type-Noncoherent-Large-ω-Precategory + 𝒜) + ( large-reflexive-globular-type-Noncoherent-Large-ω-Precategory + ℬ) + colax-reflexive-map-colax-functor-Noncoherent-Large-ω-Precategory = + make-large-colax-reflexive-globular-map + map-colax-functor-Noncoherent-Large-ω-Precategory + preserves-id-structure-colax-functor-Noncoherent-Large-ω-Precategory + + preserves-id-hom-colax-functor-Noncoherent-Large-ω-Precategory : + {l : Level} + (x : obj-Noncoherent-Large-ω-Precategory 𝒜 l) → + 2-hom-Noncoherent-Large-ω-Precategory ℬ + ( hom-colax-functor-Noncoherent-Large-ω-Precategory + ( id-hom-Noncoherent-Large-ω-Precategory 𝒜 {x = x})) + ( id-hom-Noncoherent-Large-ω-Precategory ℬ + { x = obj-colax-functor-Noncoherent-Large-ω-Precategory x}) + preserves-id-hom-colax-functor-Noncoherent-Large-ω-Precategory = + preserves-id-hom-is-colax-functor-Noncoherent-Large-ω-Precategory + ( is-colax-functor-colax-functor-Noncoherent-Large-ω-Precategory) + + preserves-id-structure-hom-colax-functor-Noncoherent-Large-ω-Precategory : + {l1 l2 : Level} + {x : obj-Noncoherent-Large-ω-Precategory 𝒜 l1} + {y : obj-Noncoherent-Large-ω-Precategory 𝒜 l2} → + preserves-id-structure-map-Noncoherent-ω-Precategory + ( hom-noncoherent-ω-precategory-Noncoherent-Large-ω-Precategory + 𝒜 x y) + ( hom-noncoherent-ω-precategory-Noncoherent-Large-ω-Precategory + ℬ _ _) + ( 1-cell-globular-map-large-globular-map + map-colax-functor-Noncoherent-Large-ω-Precategory) + preserves-id-structure-hom-colax-functor-Noncoherent-Large-ω-Precategory = + preserves-id-structure-hom-is-colax-functor-Noncoherent-Large-ω-Precategory + is-colax-functor-colax-functor-Noncoherent-Large-ω-Precategory +``` + +Preservation of the composition structure: + +```agda + preserves-comp-structure-colax-functor-Noncoherent-Large-ω-Precategory : + preserves-comp-structure-map-Noncoherent-Large-ω-Precategory 𝒜 ℬ + map-colax-functor-Noncoherent-Large-ω-Precategory + preserves-comp-structure-colax-functor-Noncoherent-Large-ω-Precategory = + preserves-comp-structure-is-colax-functor-Noncoherent-Large-ω-Precategory + is-colax-functor-colax-functor-Noncoherent-Large-ω-Precategory + + colax-transitive-map-colax-functor-Noncoherent-Large-ω-Precategory : + large-colax-transitive-globular-map δ + ( large-transitive-globular-type-Noncoherent-Large-ω-Precategory + 𝒜) + ( large-transitive-globular-type-Noncoherent-Large-ω-Precategory + ℬ) + large-globular-map-large-colax-transitive-globular-map + colax-transitive-map-colax-functor-Noncoherent-Large-ω-Precategory = + map-colax-functor-Noncoherent-Large-ω-Precategory + is-colax-transitive-large-colax-transitive-globular-map + colax-transitive-map-colax-functor-Noncoherent-Large-ω-Precategory = + preserves-comp-structure-colax-functor-Noncoherent-Large-ω-Precategory + + preserves-comp-hom-colax-functor-Noncoherent-Large-ω-Precategory : + {l1 l2 l3 : Level} + {x : obj-Noncoherent-Large-ω-Precategory 𝒜 l1} + {y : obj-Noncoherent-Large-ω-Precategory 𝒜 l2} + {z : obj-Noncoherent-Large-ω-Precategory 𝒜 l3} + (g : hom-Noncoherent-Large-ω-Precategory 𝒜 y z) + (f : hom-Noncoherent-Large-ω-Precategory 𝒜 x y) → + 2-hom-Noncoherent-Large-ω-Precategory ℬ + ( hom-colax-functor-Noncoherent-Large-ω-Precategory + ( comp-hom-Noncoherent-Large-ω-Precategory 𝒜 g f)) + ( comp-hom-Noncoherent-Large-ω-Precategory ℬ + ( hom-colax-functor-Noncoherent-Large-ω-Precategory g) + ( hom-colax-functor-Noncoherent-Large-ω-Precategory f)) + preserves-comp-hom-colax-functor-Noncoherent-Large-ω-Precategory = + preserves-comp-hom-is-colax-functor-Noncoherent-Large-ω-Precategory + ( is-colax-functor-colax-functor-Noncoherent-Large-ω-Precategory) + + preserves-comp-structure-hom-colax-functor-Noncoherent-Large-ω-Precategory : + {l1 l2 : Level} + {x : obj-Noncoherent-Large-ω-Precategory 𝒜 l1} + {y : obj-Noncoherent-Large-ω-Precategory 𝒜 l2} → + preserves-comp-structure-map-Noncoherent-ω-Precategory + ( hom-noncoherent-ω-precategory-Noncoherent-Large-ω-Precategory + 𝒜 x y) + ( hom-noncoherent-ω-precategory-Noncoherent-Large-ω-Precategory + ℬ _ _) + ( 1-cell-globular-map-large-globular-map + map-colax-functor-Noncoherent-Large-ω-Precategory) + preserves-comp-structure-hom-colax-functor-Noncoherent-Large-ω-Precategory = + preserves-comp-structure-hom-is-colax-functor-Noncoherent-Large-ω-Precategory + is-colax-functor-colax-functor-Noncoherent-Large-ω-Precategory +``` + +The globular map on hom-types is again a colax functor: + +```agda + is-colax-functor-hom-colax-functor-colax-functor-Noncoherent-Large-ω-Precategory : + {l1 l2 : Level} + {x : obj-Noncoherent-Large-ω-Precategory 𝒜 l1} + {y : obj-Noncoherent-Large-ω-Precategory 𝒜 l2} → + is-colax-functor-Noncoherent-ω-Precategory + ( hom-noncoherent-ω-precategory-Noncoherent-Large-ω-Precategory + ( 𝒜) + ( x) + ( y)) + ( hom-noncoherent-ω-precategory-Noncoherent-Large-ω-Precategory + ( ℬ) + ( obj-colax-functor-Noncoherent-Large-ω-Precategory x) + ( obj-colax-functor-Noncoherent-Large-ω-Precategory y)) + ( hom-globular-map-colax-functor-Noncoherent-Large-ω-Precategory) + is-colax-functor-hom-colax-functor-colax-functor-Noncoherent-Large-ω-Precategory = + make-is-colax-functor-Noncoherent-ω-Precategory + preserves-id-structure-hom-colax-functor-Noncoherent-Large-ω-Precategory + preserves-comp-structure-hom-colax-functor-Noncoherent-Large-ω-Precategory + + hom-colax-functor-colax-functor-Noncoherent-Large-ω-Precategory : + {l1 l2 : Level} + (x : obj-Noncoherent-Large-ω-Precategory 𝒜 l1) + (y : obj-Noncoherent-Large-ω-Precategory 𝒜 l2) → + colax-functor-Noncoherent-ω-Precategory + ( hom-noncoherent-ω-precategory-Noncoherent-Large-ω-Precategory + ( 𝒜) + ( x) + ( y)) + ( hom-noncoherent-ω-precategory-Noncoherent-Large-ω-Precategory + ( ℬ) + ( obj-colax-functor-Noncoherent-Large-ω-Precategory x) + ( obj-colax-functor-Noncoherent-Large-ω-Precategory y)) + hom-colax-functor-colax-functor-Noncoherent-Large-ω-Precategory + x y = + hom-globular-map-colax-functor-Noncoherent-Large-ω-Precategory , + is-colax-functor-hom-colax-functor-colax-functor-Noncoherent-Large-ω-Precategory + +open colax-functor-Noncoherent-Large-ω-Precategory public +``` + +### The identity colax functor on a noncoherent large ω-precategory + +```agda +module _ + {α : Level → Level} {β : Level → Level → Level} + (𝒜 : Noncoherent-Large-ω-Precategory α β) + where + + preserves-id-structure-id-colax-functor-Noncoherent-Large-ω-Precatory : + preserves-id-structure-map-Noncoherent-Large-ω-Precategory 𝒜 𝒜 + ( id-map-Noncoherent-Large-ω-Precategory 𝒜) + preserves-id-structure-id-colax-functor-Noncoherent-Large-ω-Precatory = + is-colax-reflexive-id-large-colax-reflexive-globular-map + ( large-reflexive-globular-type-Noncoherent-Large-ω-Precategory + 𝒜) + + preserves-comp-structure-id-colax-functor-Noncoherent-Large-ω-Precategory : + preserves-comp-structure-map-Noncoherent-Large-ω-Precategory 𝒜 𝒜 + ( id-map-Noncoherent-Large-ω-Precategory 𝒜) + preserves-comp-1-cell-is-colax-transitive-large-globular-map + preserves-comp-structure-id-colax-functor-Noncoherent-Large-ω-Precategory + g f = + id-2-hom-Noncoherent-Large-ω-Precategory 𝒜 _ + is-colax-transitive-1-cell-globular-map-is-colax-transitive-large-globular-map + preserves-comp-structure-id-colax-functor-Noncoherent-Large-ω-Precategory = + preserves-comp-structure-id-colax-functor-Noncoherent-ω-Precategory + ( hom-noncoherent-ω-precategory-Noncoherent-Large-ω-Precategory + 𝒜 _ _) + + is-colax-functor-id-colax-functor-Noncoherent-Large-ω-Precategory : + is-colax-functor-Noncoherent-Large-ω-Precategory 𝒜 𝒜 + ( id-map-Noncoherent-Large-ω-Precategory 𝒜) + is-colax-functor-id-colax-functor-Noncoherent-Large-ω-Precategory = + make-is-colax-functor-Noncoherent-Large-ω-Precategory + preserves-id-structure-id-colax-functor-Noncoherent-Large-ω-Precatory + preserves-comp-structure-id-colax-functor-Noncoherent-Large-ω-Precategory + + id-colax-functor-Noncoherent-Large-ω-Precategory : + colax-functor-Noncoherent-Large-ω-Precategory (λ l → l) 𝒜 𝒜 + map-colax-functor-Noncoherent-Large-ω-Precategory + id-colax-functor-Noncoherent-Large-ω-Precategory = + id-map-Noncoherent-Large-ω-Precategory 𝒜 + is-colax-functor-colax-functor-Noncoherent-Large-ω-Precategory + id-colax-functor-Noncoherent-Large-ω-Precategory = + is-colax-functor-id-colax-functor-Noncoherent-Large-ω-Precategory +``` + +### Composition of colax functors between noncoherent ω-precategories + +```agda +module _ + {α1 α2 α3 : Level → Level} + {β1 β2 β3 : Level → Level → Level} + {δ1 δ2 : Level → Level} + {𝒜 : Noncoherent-Large-ω-Precategory α1 β1} + {ℬ : Noncoherent-Large-ω-Precategory α2 β2} + {𝒞 : Noncoherent-Large-ω-Precategory α3 β3} + (G : colax-functor-Noncoherent-Large-ω-Precategory δ2 ℬ 𝒞) + (F : colax-functor-Noncoherent-Large-ω-Precategory δ1 𝒜 ℬ) + where + + map-comp-colax-functor-Noncoherent-Large-ω-Precategory : + map-Noncoherent-Large-ω-Precategory (λ l → δ2 (δ1 l)) 𝒜 𝒞 + map-comp-colax-functor-Noncoherent-Large-ω-Precategory = + comp-map-Noncoherent-Large-ω-Precategory 𝒜 ℬ 𝒞 + ( map-colax-functor-Noncoherent-Large-ω-Precategory G) + ( map-colax-functor-Noncoherent-Large-ω-Precategory F) + + preserves-id-structure-comp-colax-functor-Noncoherent-Large-ω-Precategory : + preserves-id-structure-map-Noncoherent-Large-ω-Precategory 𝒜 𝒞 + map-comp-colax-functor-Noncoherent-Large-ω-Precategory + preserves-refl-1-cell-is-colax-reflexive-large-globular-map + preserves-id-structure-comp-colax-functor-Noncoherent-Large-ω-Precategory + x = + comp-2-hom-Noncoherent-Large-ω-Precategory 𝒞 + ( preserves-id-hom-colax-functor-Noncoherent-Large-ω-Precategory + ( G) + ( _)) + ( 2-hom-colax-functor-Noncoherent-Large-ω-Precategory G + ( preserves-id-hom-colax-functor-Noncoherent-Large-ω-Precategory + ( F) + ( _))) + is-colax-reflexive-1-cell-globular-map-is-colax-reflexive-large-globular-map + preserves-id-structure-comp-colax-functor-Noncoherent-Large-ω-Precategory = + preserves-id-structure-comp-colax-functor-Noncoherent-ω-Precategory + ( hom-noncoherent-ω-precategory-Noncoherent-Large-ω-Precategory + 𝒜 _ _) + ( hom-noncoherent-ω-precategory-Noncoherent-Large-ω-Precategory + ℬ _ _) + ( hom-noncoherent-ω-precategory-Noncoherent-Large-ω-Precategory + 𝒞 _ _) + ( hom-colax-functor-colax-functor-Noncoherent-Large-ω-Precategory + G _ _) + ( hom-colax-functor-colax-functor-Noncoherent-Large-ω-Precategory + F _ _) + + preserves-comp-structure-comp-colax-functor-Noncoherent-Large-ω-Precategory : + preserves-comp-structure-map-Noncoherent-Large-ω-Precategory 𝒜 𝒞 + map-comp-colax-functor-Noncoherent-Large-ω-Precategory + preserves-comp-structure-comp-colax-functor-Noncoherent-Large-ω-Precategory = + is-colax-transitive-comp-large-colax-transitive-globular-map + ( large-transitive-globular-type-Noncoherent-Large-ω-Precategory + 𝒜) + ( large-transitive-globular-type-Noncoherent-Large-ω-Precategory + ℬ) + ( large-transitive-globular-type-Noncoherent-Large-ω-Precategory + 𝒞) + ( colax-transitive-map-colax-functor-Noncoherent-Large-ω-Precategory + G) + ( colax-transitive-map-colax-functor-Noncoherent-Large-ω-Precategory + F) + + is-colax-functor-comp-colax-functor-Noncoherent-Large-Wild-Precategory : + is-colax-functor-Noncoherent-Large-ω-Precategory 𝒜 𝒞 + map-comp-colax-functor-Noncoherent-Large-ω-Precategory + is-colax-functor-comp-colax-functor-Noncoherent-Large-Wild-Precategory = + make-is-colax-functor-Noncoherent-Large-ω-Precategory + preserves-id-structure-comp-colax-functor-Noncoherent-Large-ω-Precategory + preserves-comp-structure-comp-colax-functor-Noncoherent-Large-ω-Precategory + + comp-colax-functor-Noncoherent-Large-Wild-Precategory : + colax-functor-Noncoherent-Large-ω-Precategory + ( λ l → δ2 (δ1 l)) + ( 𝒜) + ( 𝒞) + comp-colax-functor-Noncoherent-Large-Wild-Precategory = + make-colax-functor-Noncoherent-Large-ω-Precategory + map-comp-colax-functor-Noncoherent-Large-ω-Precategory + is-colax-functor-comp-colax-functor-Noncoherent-Large-Wild-Precategory +``` diff --git a/src/wild-category-theory/colax-functors-noncoherent-large-wild-higher-precategories.lagda.md b/src/wild-category-theory/colax-functors-noncoherent-large-wild-higher-precategories.lagda.md deleted file mode 100644 index f21f8983d1..0000000000 --- a/src/wild-category-theory/colax-functors-noncoherent-large-wild-higher-precategories.lagda.md +++ /dev/null @@ -1,552 +0,0 @@ -# Colax functors between large noncoherent wild higher precategories - -```agda -{-# OPTIONS --guardedness #-} - -module wild-category-theory.colax-functors-noncoherent-large-wild-higher-precategories where -``` - -
Imports - -```agda -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 -{{#concept "colax functor" Disambiguation="between noncoherent large wild higher precategories" Agda=colax-functor-Noncoherent-Large-Wild-Higher-Precategory}} -`f` between -[noncoherent large wild higher precategories](wild-category-theory.noncoherent-large-wild-higher-precategories.md) -`𝒜` and `ℬ` is a -[map of noncoherent large wild higher precategories](wild-category-theory.maps-noncoherent-large-wild-higher-precategories.md) -that preserves identity morphisms and composition _colaxly_. This means that for -every $n$-morphism `f` in `𝒜`, where we take $0$-morphisms to be objects, there -is an $(n+1)$-morphism - -```text - Fₙ₊₁ (id-hom 𝒜 f) ⇒ id-hom ℬ (Fₙ f) -``` - -in `ℬ`, and for every pair of composable $(n+1)$-morphisms `g` after `f` in `𝒜`, -there is an $(n+2)$-morphism - -```text - Fₙ₊₁ (g ∘ f) ⇒ (Fₙ₊₁ g) ∘ (Fₙ₊₁ f) -``` - -in `ℬ`. - -## Definitions - -### The predicate on maps between large noncoherent wild higher precategories of preserving the identity structure - -```agda -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 - -```agda -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 - -```agda -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 - -```agda -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: - -```agda - 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: - -```agda - 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: - -```agda - 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: - -```agda - 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 - -```agda -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 - -```agda -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 -``` diff --git a/src/wild-category-theory/colax-functors-noncoherent-omega-precategories.lagda.md b/src/wild-category-theory/colax-functors-noncoherent-omega-precategories.lagda.md new file mode 100644 index 0000000000..8bb9dc1251 --- /dev/null +++ b/src/wild-category-theory/colax-functors-noncoherent-omega-precategories.lagda.md @@ -0,0 +1,469 @@ +# Colax functors between noncoherent ω-precategories + +```agda +{-# OPTIONS --guardedness #-} + +module wild-category-theory.colax-functors-noncoherent-omega-precategories where +``` + +
Imports + +```agda +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.colax-reflexive-globular-maps +open import globular-types.colax-transitive-globular-maps +open import globular-types.globular-maps +open import globular-types.globular-types +open import globular-types.reflexive-globular-types + +open import wild-category-theory.maps-noncoherent-omega-precategories +open import wild-category-theory.noncoherent-omega-precategories +``` + +
+ +## Idea + +A +{{#concept "colax functor" Disambiguation="between noncoherent ω-precategories" Agda=colax-functor-Noncoherent-ω-Precategory}} +`F` between +[noncoherent ω-precategories](wild-category-theory.noncoherent-omega-precategories.md) +`𝒜` and `ℬ` is a +[map of noncoherent ω-precategories](wild-category-theory.maps-noncoherent-omega-precategories.md) +which is [colax reflexive](globular-types.colax-reflexive-globular-maps.md) and +[colax transitive](globular-types.colax-transitive-globular-maps.md). This means +that for every $n$-morphism `f` in `𝒜`, where we take $0$-morphisms to be +objects, there is an $(n+1)$-morphism + +```text + Fₙ₊₁ (id-hom 𝒜 f) ⇒ id-hom ℬ (Fₙ f) +``` + +in `ℬ`, and for every pair of composable $(n+1)$-morphisms `g` after `f` in `𝒜`, +there is an $(n+2)$-morphism + +```text + Fₙ₊₁ (g ∘ f) ⇒ (Fₙ₊₁ g) ∘ (Fₙ₊₁ f) +``` + +in `ℬ`. + +## Definitions + +### The predicate on maps on noncoherent ω-precategories of preserving identity structure + +```agda +module _ + {l1 l2 l3 l4 : Level} + (𝒜 : Noncoherent-ω-Precategory l1 l2) + (ℬ : Noncoherent-ω-Precategory l3 l4) + (F : map-Noncoherent-ω-Precategory 𝒜 ℬ) + where + + preserves-id-structure-map-Noncoherent-ω-Precategory : + UU (l1 ⊔ l2 ⊔ l4) + preserves-id-structure-map-Noncoherent-ω-Precategory = + is-colax-reflexive-globular-map + ( reflexive-globular-type-Noncoherent-ω-Precategory 𝒜) + ( reflexive-globular-type-Noncoherent-ω-Precategory ℬ) + ( F) +``` + +### The predicate on maps of noncoherent ω-precategories of preserving composition structure + +```agda +module _ + {l1 l2 l3 l4 : Level} + (𝒜 : Noncoherent-ω-Precategory l1 l2) + (ℬ : Noncoherent-ω-Precategory l3 l4) + (F : map-Noncoherent-ω-Precategory 𝒜 ℬ) + where + + preserves-comp-structure-map-Noncoherent-ω-Precategory : + UU (l1 ⊔ l2 ⊔ l4) + preserves-comp-structure-map-Noncoherent-ω-Precategory = + is-colax-transitive-globular-map + ( transitive-globular-type-Noncoherent-ω-Precategory 𝒜) + ( transitive-globular-type-Noncoherent-ω-Precategory ℬ) + ( F) +``` + +### The predicate of being a colax functor between noncoherent ω-precategories + +```agda +record + is-colax-functor-Noncoherent-ω-Precategory + {l1 l2 l3 l4 : Level} + (𝒜 : Noncoherent-ω-Precategory l1 l2) + (ℬ : Noncoherent-ω-Precategory l3 l4) + (F : map-Noncoherent-ω-Precategory 𝒜 ℬ) : UU (l1 ⊔ l2 ⊔ l4) + where + + constructor make-is-colax-functor-Noncoherent-ω-Precategory + + coinductive + + field + is-reflexive-is-colax-functor-Noncoherent-ω-Precategory : + preserves-id-structure-map-Noncoherent-ω-Precategory 𝒜 ℬ F + + preserves-id-hom-is-colax-functor-Noncoherent-ω-Precategory : + (x : obj-Noncoherent-ω-Precategory 𝒜) → + 2-hom-Noncoherent-ω-Precategory ℬ + ( 1-cell-globular-map F (id-hom-Noncoherent-ω-Precategory 𝒜)) + ( id-hom-Noncoherent-ω-Precategory ℬ) + preserves-id-hom-is-colax-functor-Noncoherent-ω-Precategory = + preserves-refl-1-cell-is-colax-reflexive-globular-map + is-reflexive-is-colax-functor-Noncoherent-ω-Precategory + + is-reflexive-hom-globular-map-is-colax-functor-Noncoherent-ω-Precategory : + {x y : obj-Noncoherent-ω-Precategory 𝒜} → + is-colax-reflexive-globular-map + ( hom-reflexive-globular-type-Noncoherent-ω-Precategory 𝒜 x y) + ( hom-reflexive-globular-type-Noncoherent-ω-Precategory ℬ + ( 0-cell-globular-map F x) + ( 0-cell-globular-map F y)) + ( 1-cell-globular-map-globular-map F) + is-reflexive-hom-globular-map-is-colax-functor-Noncoherent-ω-Precategory = + is-colax-reflexive-1-cell-globular-map-is-colax-reflexive-globular-map + is-reflexive-is-colax-functor-Noncoherent-ω-Precategory + + field + is-transitive-is-colax-functor-Noncoherent-ω-Precategory : + preserves-comp-structure-map-Noncoherent-ω-Precategory 𝒜 ℬ F + + preserves-comp-hom-is-colax-functor-Noncoherent-ω-Precategory : + {x y z : obj-Noncoherent-ω-Precategory 𝒜} + (g : hom-Noncoherent-ω-Precategory 𝒜 y z) + (f : hom-Noncoherent-ω-Precategory 𝒜 x y) → + 2-hom-Noncoherent-ω-Precategory ℬ + ( 1-cell-globular-map F + ( comp-hom-Noncoherent-ω-Precategory 𝒜 g f)) + ( comp-hom-Noncoherent-ω-Precategory ℬ + ( 1-cell-globular-map F g) + ( 1-cell-globular-map F f)) + preserves-comp-hom-is-colax-functor-Noncoherent-ω-Precategory = + preserves-comp-1-cell-is-colax-transitive-globular-map + is-transitive-is-colax-functor-Noncoherent-ω-Precategory + + is-transitive-hom-globular-map-is-colax-functor-Noncoherent-ω-Precategory : + {x y : obj-Noncoherent-ω-Precategory 𝒜} → + is-colax-transitive-globular-map + ( hom-transitive-globular-type-Noncoherent-ω-Precategory 𝒜 x y) + ( hom-transitive-globular-type-Noncoherent-ω-Precategory ℬ + ( 0-cell-globular-map F x) + ( 0-cell-globular-map F y)) + ( 1-cell-globular-map-globular-map F) + is-transitive-hom-globular-map-is-colax-functor-Noncoherent-ω-Precategory = + is-colax-transitive-1-cell-globular-map-is-colax-transitive-globular-map + is-transitive-is-colax-functor-Noncoherent-ω-Precategory + + is-colax-functor-hom-globular-map-is-colax-functor-Noncoherent-ω-Precategory : + {x y : obj-Noncoherent-ω-Precategory 𝒜} → + is-colax-functor-Noncoherent-ω-Precategory + ( hom-noncoherent-ω-precategory-Noncoherent-ω-Precategory + 𝒜 x y) + ( hom-noncoherent-ω-precategory-Noncoherent-ω-Precategory + ( ℬ) + ( 0-cell-globular-map F x) + ( 0-cell-globular-map F y)) + ( 1-cell-globular-map-globular-map F {x} {y}) + is-reflexive-is-colax-functor-Noncoherent-ω-Precategory + is-colax-functor-hom-globular-map-is-colax-functor-Noncoherent-ω-Precategory = + is-reflexive-hom-globular-map-is-colax-functor-Noncoherent-ω-Precategory + is-transitive-is-colax-functor-Noncoherent-ω-Precategory + is-colax-functor-hom-globular-map-is-colax-functor-Noncoherent-ω-Precategory = + is-transitive-hom-globular-map-is-colax-functor-Noncoherent-ω-Precategory + +open is-colax-functor-Noncoherent-ω-Precategory public +``` + +### The type of colax functors between noncoherent ω-precategories + +```agda +colax-functor-Noncoherent-ω-Precategory : + {l1 l2 l3 l4 : Level} + (𝒜 : Noncoherent-ω-Precategory l1 l2) + (ℬ : Noncoherent-ω-Precategory l3 l4) → + UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) +colax-functor-Noncoherent-ω-Precategory 𝒜 ℬ = + Σ ( map-Noncoherent-ω-Precategory 𝒜 ℬ) + ( is-colax-functor-Noncoherent-ω-Precategory 𝒜 ℬ) +``` + +The action of colax functors on objects, morphisms, and higher morphisms: + +```agda +module _ + {l1 l2 l3 l4 : Level} + {𝒜 : Noncoherent-ω-Precategory l1 l2} + {ℬ : Noncoherent-ω-Precategory l3 l4} + (F : colax-functor-Noncoherent-ω-Precategory 𝒜 ℬ) + where + + map-colax-functor-Noncoherent-ω-Precategory : + map-Noncoherent-ω-Precategory 𝒜 ℬ + map-colax-functor-Noncoherent-ω-Precategory = pr1 F + + obj-colax-functor-Noncoherent-ω-Precategory : + obj-Noncoherent-ω-Precategory 𝒜 → + obj-Noncoherent-ω-Precategory ℬ + obj-colax-functor-Noncoherent-ω-Precategory = + 0-cell-globular-map map-colax-functor-Noncoherent-ω-Precategory + + hom-colax-functor-Noncoherent-ω-Precategory : + {x y : obj-Noncoherent-ω-Precategory 𝒜} → + hom-Noncoherent-ω-Precategory 𝒜 x y → + hom-Noncoherent-ω-Precategory ℬ + ( obj-colax-functor-Noncoherent-ω-Precategory x) + ( obj-colax-functor-Noncoherent-ω-Precategory y) + hom-colax-functor-Noncoherent-ω-Precategory = + 1-cell-globular-map map-colax-functor-Noncoherent-ω-Precategory + + hom-globular-map-colax-functor-Noncoherent-ω-Precategory : + {x y : obj-Noncoherent-ω-Precategory 𝒜} → + globular-map + ( hom-globular-type-Noncoherent-ω-Precategory 𝒜 x y) + ( hom-globular-type-Noncoherent-ω-Precategory ℬ + ( obj-colax-functor-Noncoherent-ω-Precategory x) + ( obj-colax-functor-Noncoherent-ω-Precategory y)) + hom-globular-map-colax-functor-Noncoherent-ω-Precategory = + 1-cell-globular-map-globular-map + map-colax-functor-Noncoherent-ω-Precategory + + 2-hom-colax-functor-Noncoherent-ω-Precategory : + {x y : obj-Noncoherent-ω-Precategory 𝒜} + {f g : hom-Noncoherent-ω-Precategory 𝒜 x y} → + 2-hom-Noncoherent-ω-Precategory 𝒜 f g → + 2-hom-Noncoherent-ω-Precategory ℬ + ( hom-colax-functor-Noncoherent-ω-Precategory f) + ( hom-colax-functor-Noncoherent-ω-Precategory g) + 2-hom-colax-functor-Noncoherent-ω-Precategory = + 2-cell-globular-map map-colax-functor-Noncoherent-ω-Precategory + + is-colax-functor-colax-functor-Noncoherent-ω-Precategory : + is-colax-functor-Noncoherent-ω-Precategory 𝒜 ℬ + ( map-colax-functor-Noncoherent-ω-Precategory) + is-colax-functor-colax-functor-Noncoherent-ω-Precategory = pr2 F +``` + +Preservation by colax functors of identity morphisms: + +```agda + preserves-id-hom-colax-functor-Noncoherent-ω-Precategory : + (x : obj-Noncoherent-ω-Precategory 𝒜) → + 2-hom-Noncoherent-ω-Precategory ℬ + ( hom-colax-functor-Noncoherent-ω-Precategory + ( id-hom-Noncoherent-ω-Precategory 𝒜 {x})) + ( id-hom-Noncoherent-ω-Precategory ℬ + { obj-colax-functor-Noncoherent-ω-Precategory x}) + preserves-id-hom-colax-functor-Noncoherent-ω-Precategory = + preserves-id-hom-is-colax-functor-Noncoherent-ω-Precategory + ( is-colax-functor-colax-functor-Noncoherent-ω-Precategory) + + colax-reflexive-globular-map-colax-functor-Noncoherent-ω-Precategory : + colax-reflexive-globular-map + ( reflexive-globular-type-Noncoherent-ω-Precategory 𝒜) + ( reflexive-globular-type-Noncoherent-ω-Precategory ℬ) + colax-reflexive-globular-map-colax-functor-Noncoherent-ω-Precategory = + make-colax-reflexive-globular-map + ( map-colax-functor-Noncoherent-ω-Precategory) + ( is-reflexive-is-colax-functor-Noncoherent-ω-Precategory + is-colax-functor-colax-functor-Noncoherent-ω-Precategory) +``` + +Preservation by colax functors of composition: + +```agda + preserves-comp-hom-colax-functor-Noncoherent-ω-Precategory : + {x y z : obj-Noncoherent-ω-Precategory 𝒜} + (g : hom-Noncoherent-ω-Precategory 𝒜 y z) + (f : hom-Noncoherent-ω-Precategory 𝒜 x y) → + 2-hom-Noncoherent-ω-Precategory ℬ + ( hom-colax-functor-Noncoherent-ω-Precategory + ( comp-hom-Noncoherent-ω-Precategory 𝒜 g f)) + ( comp-hom-Noncoherent-ω-Precategory ℬ + ( hom-colax-functor-Noncoherent-ω-Precategory g) + ( hom-colax-functor-Noncoherent-ω-Precategory f)) + preserves-comp-hom-colax-functor-Noncoherent-ω-Precategory = + preserves-comp-hom-is-colax-functor-Noncoherent-ω-Precategory + ( is-colax-functor-colax-functor-Noncoherent-ω-Precategory) + + colax-transitive-globular-map-colax-functor-Noncoherent-ω-Precategory : + colax-transitive-globular-map + ( transitive-globular-type-Noncoherent-ω-Precategory 𝒜) + ( transitive-globular-type-Noncoherent-ω-Precategory ℬ) + colax-transitive-globular-map-colax-functor-Noncoherent-ω-Precategory = + make-colax-transitive-globular-map + ( map-colax-functor-Noncoherent-ω-Precategory) + ( is-transitive-is-colax-functor-Noncoherent-ω-Precategory + is-colax-functor-colax-functor-Noncoherent-ω-Precategory) +``` + +The induced colax functor on the wild category of morphisms between two objects: + +```agda + hom-colax-functor-colax-functor-Noncoherent-ω-Precategory : + (x y : obj-Noncoherent-ω-Precategory 𝒜) → + colax-functor-Noncoherent-ω-Precategory + ( hom-noncoherent-ω-precategory-Noncoherent-ω-Precategory + ( 𝒜) + ( x) + ( y)) + ( hom-noncoherent-ω-precategory-Noncoherent-ω-Precategory + ( ℬ) + ( obj-colax-functor-Noncoherent-ω-Precategory x) + ( obj-colax-functor-Noncoherent-ω-Precategory y)) + hom-colax-functor-colax-functor-Noncoherent-ω-Precategory x y = + ( hom-globular-map-colax-functor-Noncoherent-ω-Precategory , + is-colax-functor-hom-globular-map-is-colax-functor-Noncoherent-ω-Precategory + is-colax-functor-colax-functor-Noncoherent-ω-Precategory) +``` + +### The identity colax functor on a noncoherent ω-precategory + +```agda +map-id-colax-functor-Noncoherent-ω-Precategory : + {l1 l2 : Level} (𝒜 : Noncoherent-ω-Precategory l1 l2) → + map-Noncoherent-ω-Precategory 𝒜 𝒜 +map-id-colax-functor-Noncoherent-ω-Precategory 𝒜 = + id-map-Noncoherent-ω-Precategory 𝒜 + +preserves-id-structure-id-colax-functor-Noncoherent-ω-Precategory : + {l1 l2 : Level} (𝒜 : Noncoherent-ω-Precategory l1 l2) → + preserves-id-structure-map-Noncoherent-ω-Precategory 𝒜 𝒜 + ( map-id-colax-functor-Noncoherent-ω-Precategory 𝒜) +preserves-id-structure-id-colax-functor-Noncoherent-ω-Precategory 𝒜 = + is-colax-reflexive-id-colax-reflexive-globular-map + ( reflexive-globular-type-Noncoherent-ω-Precategory 𝒜) + +preserves-comp-structure-id-colax-functor-Noncoherent-ω-Precategory : + {l1 l2 : Level} (𝒜 : Noncoherent-ω-Precategory l1 l2) → + preserves-comp-structure-map-Noncoherent-ω-Precategory 𝒜 𝒜 + ( map-id-colax-functor-Noncoherent-ω-Precategory 𝒜) +preserves-comp-1-cell-is-colax-transitive-globular-map + ( preserves-comp-structure-id-colax-functor-Noncoherent-ω-Precategory + 𝒜) + _ _ = + id-2-hom-Noncoherent-ω-Precategory 𝒜 +is-colax-transitive-1-cell-globular-map-is-colax-transitive-globular-map + ( preserves-comp-structure-id-colax-functor-Noncoherent-ω-Precategory + 𝒜) = + preserves-comp-structure-id-colax-functor-Noncoherent-ω-Precategory + ( hom-noncoherent-ω-precategory-Noncoherent-ω-Precategory + ( 𝒜) + ( _) + ( _)) + +is-colax-functor-id-colax-functor-Noncoherent-ω-Precategory : + {l1 l2 : Level} (𝒜 : Noncoherent-ω-Precategory l1 l2) → + is-colax-functor-Noncoherent-ω-Precategory 𝒜 𝒜 + ( map-id-colax-functor-Noncoherent-ω-Precategory 𝒜) +is-colax-functor-id-colax-functor-Noncoherent-ω-Precategory 𝒜 = + make-is-colax-functor-Noncoherent-ω-Precategory + ( preserves-id-structure-id-colax-functor-Noncoherent-ω-Precategory + 𝒜) + ( preserves-comp-structure-id-colax-functor-Noncoherent-ω-Precategory + 𝒜) + +id-colax-functor-Noncoherent-ω-Precategory : + {l1 l2 : Level} (𝒜 : Noncoherent-ω-Precategory l1 l2) → + colax-functor-Noncoherent-ω-Precategory 𝒜 𝒜 +id-colax-functor-Noncoherent-ω-Precategory 𝒜 = + ( id-map-Noncoherent-ω-Precategory 𝒜 , + is-colax-functor-id-colax-functor-Noncoherent-ω-Precategory 𝒜) +``` + +### Composition of colax functors between noncoherent ω-precategories + +```agda +module _ + {l1 l2 l3 l4 l5 l6 : Level} + (𝒜 : Noncoherent-ω-Precategory l1 l2) + (ℬ : Noncoherent-ω-Precategory l3 l4) + (𝒞 : Noncoherent-ω-Precategory l5 l6) + (G : colax-functor-Noncoherent-ω-Precategory ℬ 𝒞) + (F : colax-functor-Noncoherent-ω-Precategory 𝒜 ℬ) + where + + map-comp-colax-functor-Noncoherent-ω-Precategory : + map-Noncoherent-ω-Precategory 𝒜 𝒞 + map-comp-colax-functor-Noncoherent-ω-Precategory = + comp-map-Noncoherent-ω-Precategory 𝒜 ℬ 𝒞 + ( map-colax-functor-Noncoherent-ω-Precategory G) + ( map-colax-functor-Noncoherent-ω-Precategory F) + +preserves-id-structure-comp-colax-functor-Noncoherent-ω-Precategory : + {l1 l2 l3 l4 l5 l6 : Level} + (𝒜 : Noncoherent-ω-Precategory l1 l2) + (ℬ : Noncoherent-ω-Precategory l3 l4) + (𝒞 : Noncoherent-ω-Precategory l5 l6) + (G : colax-functor-Noncoherent-ω-Precategory ℬ 𝒞) + (F : colax-functor-Noncoherent-ω-Precategory 𝒜 ℬ) → + preserves-id-structure-map-Noncoherent-ω-Precategory 𝒜 𝒞 + ( map-comp-colax-functor-Noncoherent-ω-Precategory 𝒜 ℬ 𝒞 G F) +preserves-refl-1-cell-is-colax-reflexive-globular-map + ( preserves-id-structure-comp-colax-functor-Noncoherent-ω-Precategory + 𝒜 ℬ 𝒞 G F) + x = + comp-2-hom-Noncoherent-ω-Precategory 𝒞 + ( preserves-id-hom-colax-functor-Noncoherent-ω-Precategory G _) + ( 2-hom-colax-functor-Noncoherent-ω-Precategory G + ( preserves-id-hom-colax-functor-Noncoherent-ω-Precategory F _)) +is-colax-reflexive-1-cell-globular-map-is-colax-reflexive-globular-map + ( preserves-id-structure-comp-colax-functor-Noncoherent-ω-Precategory + 𝒜 ℬ 𝒞 G F) = + preserves-id-structure-comp-colax-functor-Noncoherent-ω-Precategory + ( hom-noncoherent-ω-precategory-Noncoherent-ω-Precategory + 𝒜 _ _) + ( hom-noncoherent-ω-precategory-Noncoherent-ω-Precategory + ℬ _ _) + ( hom-noncoherent-ω-precategory-Noncoherent-ω-Precategory + 𝒞 _ _) + ( hom-colax-functor-colax-functor-Noncoherent-ω-Precategory + G _ _) + ( hom-colax-functor-colax-functor-Noncoherent-ω-Precategory + F _ _) + +module _ + {l1 l2 l3 l4 l5 l6 : Level} + (𝒜 : Noncoherent-ω-Precategory l1 l2) + (ℬ : Noncoherent-ω-Precategory l3 l4) + (𝒞 : Noncoherent-ω-Precategory l5 l6) + (G : colax-functor-Noncoherent-ω-Precategory ℬ 𝒞) + (F : colax-functor-Noncoherent-ω-Precategory 𝒜 ℬ) + where + + preserves-comp-structure-comp-colax-functor-Noncoherent-ω-Precategory : + preserves-comp-structure-map-Noncoherent-ω-Precategory 𝒜 𝒞 + ( map-comp-colax-functor-Noncoherent-ω-Precategory 𝒜 ℬ 𝒞 G F) + preserves-comp-structure-comp-colax-functor-Noncoherent-ω-Precategory = + is-colax-transitive-comp-colax-transitive-globular-map + ( transitive-globular-type-Noncoherent-ω-Precategory 𝒜) + ( transitive-globular-type-Noncoherent-ω-Precategory ℬ) + ( transitive-globular-type-Noncoherent-ω-Precategory 𝒞) + ( colax-transitive-globular-map-colax-functor-Noncoherent-ω-Precategory + G) + ( colax-transitive-globular-map-colax-functor-Noncoherent-ω-Precategory + F) + + is-colax-functor-comp-colax-functor-Noncoherent-ω-Precategory : + is-colax-functor-Noncoherent-ω-Precategory 𝒜 𝒞 + ( map-comp-colax-functor-Noncoherent-ω-Precategory 𝒜 ℬ 𝒞 G F) + is-colax-functor-comp-colax-functor-Noncoherent-ω-Precategory = + make-is-colax-functor-Noncoherent-ω-Precategory + ( preserves-id-structure-comp-colax-functor-Noncoherent-ω-Precategory + 𝒜 ℬ 𝒞 G F) + ( preserves-comp-structure-comp-colax-functor-Noncoherent-ω-Precategory) + + comp-colax-functor-Noncoherent-ω-Precategory : + colax-functor-Noncoherent-ω-Precategory 𝒜 𝒞 + pr1 comp-colax-functor-Noncoherent-ω-Precategory = + map-comp-colax-functor-Noncoherent-ω-Precategory 𝒜 ℬ 𝒞 G F + pr2 comp-colax-functor-Noncoherent-ω-Precategory = + is-colax-functor-comp-colax-functor-Noncoherent-ω-Precategory +``` diff --git a/src/wild-category-theory/colax-functors-noncoherent-wild-higher-precategories.lagda.md b/src/wild-category-theory/colax-functors-noncoherent-wild-higher-precategories.lagda.md deleted file mode 100644 index 64e54b42f5..0000000000 --- a/src/wild-category-theory/colax-functors-noncoherent-wild-higher-precategories.lagda.md +++ /dev/null @@ -1,469 +0,0 @@ -# Colax functors between noncoherent wild higher precategories - -```agda -{-# OPTIONS --guardedness #-} - -module wild-category-theory.colax-functors-noncoherent-wild-higher-precategories where -``` - -
Imports - -```agda -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.colax-reflexive-globular-maps -open import globular-types.colax-transitive-globular-maps -open import globular-types.globular-maps -open import globular-types.globular-types -open import globular-types.reflexive-globular-types - -open import wild-category-theory.maps-noncoherent-wild-higher-precategories -open import wild-category-theory.noncoherent-wild-higher-precategories -``` - -
- -## Idea - -A -{{#concept "colax functor" Disambiguation="between noncoherent wild higher precategories" Agda=colax-functor-Noncoherent-Wild-Higher-Precategory}} -`F` between -[noncoherent wild higher precategories](wild-category-theory.noncoherent-wild-higher-precategories.md) -`𝒜` and `ℬ` is a -[map of noncoherent wild higher precategories](wild-category-theory.maps-noncoherent-wild-higher-precategories.md) -which is [colax reflexive](globular-types.colax-reflexive-globular-maps.md) and -[colax transitive](globular-types.colax-transitive-globular-maps.md). This means -that for every $n$-morphism `f` in `𝒜`, where we take $0$-morphisms to be -objects, there is an $(n+1)$-morphism - -```text - Fₙ₊₁ (id-hom 𝒜 f) ⇒ id-hom ℬ (Fₙ f) -``` - -in `ℬ`, and for every pair of composable $(n+1)$-morphisms `g` after `f` in `𝒜`, -there is an $(n+2)$-morphism - -```text - Fₙ₊₁ (g ∘ f) ⇒ (Fₙ₊₁ g) ∘ (Fₙ₊₁ f) -``` - -in `ℬ`. - -## Definitions - -### The predicate on maps on noncoherent wild higher precategories of preserving identity structure - -```agda -module _ - {l1 l2 l3 l4 : Level} - (𝒜 : Noncoherent-Wild-Higher-Precategory l1 l2) - (ℬ : Noncoherent-Wild-Higher-Precategory l3 l4) - (F : map-Noncoherent-Wild-Higher-Precategory 𝒜 ℬ) - where - - preserves-id-structure-map-Noncoherent-Wild-Higher-Precategory : - UU (l1 ⊔ l2 ⊔ l4) - preserves-id-structure-map-Noncoherent-Wild-Higher-Precategory = - is-colax-reflexive-globular-map - ( reflexive-globular-type-Noncoherent-Wild-Higher-Precategory 𝒜) - ( reflexive-globular-type-Noncoherent-Wild-Higher-Precategory ℬ) - ( F) -``` - -### The predicate on maps of noncoherent wild higher precategories of preserving composition structure - -```agda -module _ - {l1 l2 l3 l4 : Level} - (𝒜 : Noncoherent-Wild-Higher-Precategory l1 l2) - (ℬ : Noncoherent-Wild-Higher-Precategory l3 l4) - (F : map-Noncoherent-Wild-Higher-Precategory 𝒜 ℬ) - where - - preserves-comp-structure-map-Noncoherent-Wild-Higher-Precategory : - UU (l1 ⊔ l2 ⊔ l4) - preserves-comp-structure-map-Noncoherent-Wild-Higher-Precategory = - is-colax-transitive-globular-map - ( transitive-globular-type-Noncoherent-Wild-Higher-Precategory 𝒜) - ( transitive-globular-type-Noncoherent-Wild-Higher-Precategory ℬ) - ( F) -``` - -### The predicate of being a colax functor between noncoherent wild higher precategories - -```agda -record - is-colax-functor-Noncoherent-Wild-Higher-Precategory - {l1 l2 l3 l4 : Level} - (𝒜 : Noncoherent-Wild-Higher-Precategory l1 l2) - (ℬ : Noncoherent-Wild-Higher-Precategory l3 l4) - (F : map-Noncoherent-Wild-Higher-Precategory 𝒜 ℬ) : UU (l1 ⊔ l2 ⊔ l4) - where - - constructor make-is-colax-functor-Noncoherent-Wild-Higher-Precategory - - coinductive - - field - is-reflexive-is-colax-functor-Noncoherent-Wild-Higher-Precategory : - preserves-id-structure-map-Noncoherent-Wild-Higher-Precategory 𝒜 ℬ F - - preserves-id-hom-is-colax-functor-Noncoherent-Wild-Higher-Precategory : - (x : obj-Noncoherent-Wild-Higher-Precategory 𝒜) → - 2-hom-Noncoherent-Wild-Higher-Precategory ℬ - ( 1-cell-globular-map F (id-hom-Noncoherent-Wild-Higher-Precategory 𝒜)) - ( id-hom-Noncoherent-Wild-Higher-Precategory ℬ) - preserves-id-hom-is-colax-functor-Noncoherent-Wild-Higher-Precategory = - preserves-refl-1-cell-is-colax-reflexive-globular-map - is-reflexive-is-colax-functor-Noncoherent-Wild-Higher-Precategory - - is-reflexive-hom-globular-map-is-colax-functor-Noncoherent-Wild-Higher-Precategory : - {x y : obj-Noncoherent-Wild-Higher-Precategory 𝒜} → - is-colax-reflexive-globular-map - ( hom-reflexive-globular-type-Noncoherent-Wild-Higher-Precategory 𝒜 x y) - ( hom-reflexive-globular-type-Noncoherent-Wild-Higher-Precategory ℬ - ( 0-cell-globular-map F x) - ( 0-cell-globular-map F y)) - ( 1-cell-globular-map-globular-map F) - is-reflexive-hom-globular-map-is-colax-functor-Noncoherent-Wild-Higher-Precategory = - is-colax-reflexive-1-cell-globular-map-is-colax-reflexive-globular-map - is-reflexive-is-colax-functor-Noncoherent-Wild-Higher-Precategory - - field - is-transitive-is-colax-functor-Noncoherent-Wild-Higher-Precategory : - preserves-comp-structure-map-Noncoherent-Wild-Higher-Precategory 𝒜 ℬ F - - preserves-comp-hom-is-colax-functor-Noncoherent-Wild-Higher-Precategory : - {x y z : obj-Noncoherent-Wild-Higher-Precategory 𝒜} - (g : hom-Noncoherent-Wild-Higher-Precategory 𝒜 y z) - (f : hom-Noncoherent-Wild-Higher-Precategory 𝒜 x y) → - 2-hom-Noncoherent-Wild-Higher-Precategory ℬ - ( 1-cell-globular-map F - ( comp-hom-Noncoherent-Wild-Higher-Precategory 𝒜 g f)) - ( comp-hom-Noncoherent-Wild-Higher-Precategory ℬ - ( 1-cell-globular-map F g) - ( 1-cell-globular-map F f)) - preserves-comp-hom-is-colax-functor-Noncoherent-Wild-Higher-Precategory = - preserves-comp-1-cell-is-colax-transitive-globular-map - is-transitive-is-colax-functor-Noncoherent-Wild-Higher-Precategory - - is-transitive-hom-globular-map-is-colax-functor-Noncoherent-Wild-Higher-Precategory : - {x y : obj-Noncoherent-Wild-Higher-Precategory 𝒜} → - is-colax-transitive-globular-map - ( hom-transitive-globular-type-Noncoherent-Wild-Higher-Precategory 𝒜 x y) - ( hom-transitive-globular-type-Noncoherent-Wild-Higher-Precategory ℬ - ( 0-cell-globular-map F x) - ( 0-cell-globular-map F y)) - ( 1-cell-globular-map-globular-map F) - is-transitive-hom-globular-map-is-colax-functor-Noncoherent-Wild-Higher-Precategory = - is-colax-transitive-1-cell-globular-map-is-colax-transitive-globular-map - is-transitive-is-colax-functor-Noncoherent-Wild-Higher-Precategory - - is-colax-functor-hom-globular-map-is-colax-functor-Noncoherent-Wild-Higher-Precategory : - {x y : obj-Noncoherent-Wild-Higher-Precategory 𝒜} → - is-colax-functor-Noncoherent-Wild-Higher-Precategory - ( hom-noncoherent-wild-higher-precategory-Noncoherent-Wild-Higher-Precategory - 𝒜 x y) - ( hom-noncoherent-wild-higher-precategory-Noncoherent-Wild-Higher-Precategory - ( ℬ) - ( 0-cell-globular-map F x) - ( 0-cell-globular-map F y)) - ( 1-cell-globular-map-globular-map F {x} {y}) - is-reflexive-is-colax-functor-Noncoherent-Wild-Higher-Precategory - is-colax-functor-hom-globular-map-is-colax-functor-Noncoherent-Wild-Higher-Precategory = - is-reflexive-hom-globular-map-is-colax-functor-Noncoherent-Wild-Higher-Precategory - is-transitive-is-colax-functor-Noncoherent-Wild-Higher-Precategory - is-colax-functor-hom-globular-map-is-colax-functor-Noncoherent-Wild-Higher-Precategory = - is-transitive-hom-globular-map-is-colax-functor-Noncoherent-Wild-Higher-Precategory - -open is-colax-functor-Noncoherent-Wild-Higher-Precategory public -``` - -### The type of colax functors between noncoherent wild higher precategories - -```agda -colax-functor-Noncoherent-Wild-Higher-Precategory : - {l1 l2 l3 l4 : Level} - (𝒜 : Noncoherent-Wild-Higher-Precategory l1 l2) - (ℬ : Noncoherent-Wild-Higher-Precategory l3 l4) → - UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) -colax-functor-Noncoherent-Wild-Higher-Precategory 𝒜 ℬ = - Σ ( map-Noncoherent-Wild-Higher-Precategory 𝒜 ℬ) - ( is-colax-functor-Noncoherent-Wild-Higher-Precategory 𝒜 ℬ) -``` - -The action of colax functors on objects, morphisms, and higher morphisms: - -```agda -module _ - {l1 l2 l3 l4 : Level} - {𝒜 : Noncoherent-Wild-Higher-Precategory l1 l2} - {ℬ : Noncoherent-Wild-Higher-Precategory l3 l4} - (F : colax-functor-Noncoherent-Wild-Higher-Precategory 𝒜 ℬ) - where - - map-colax-functor-Noncoherent-Wild-Higher-Precategory : - map-Noncoherent-Wild-Higher-Precategory 𝒜 ℬ - map-colax-functor-Noncoherent-Wild-Higher-Precategory = pr1 F - - obj-colax-functor-Noncoherent-Wild-Higher-Precategory : - obj-Noncoherent-Wild-Higher-Precategory 𝒜 → - obj-Noncoherent-Wild-Higher-Precategory ℬ - obj-colax-functor-Noncoherent-Wild-Higher-Precategory = - 0-cell-globular-map map-colax-functor-Noncoherent-Wild-Higher-Precategory - - hom-colax-functor-Noncoherent-Wild-Higher-Precategory : - {x y : obj-Noncoherent-Wild-Higher-Precategory 𝒜} → - hom-Noncoherent-Wild-Higher-Precategory 𝒜 x y → - hom-Noncoherent-Wild-Higher-Precategory ℬ - ( obj-colax-functor-Noncoherent-Wild-Higher-Precategory x) - ( obj-colax-functor-Noncoherent-Wild-Higher-Precategory y) - hom-colax-functor-Noncoherent-Wild-Higher-Precategory = - 1-cell-globular-map map-colax-functor-Noncoherent-Wild-Higher-Precategory - - hom-globular-map-colax-functor-Noncoherent-Wild-Higher-Precategory : - {x y : obj-Noncoherent-Wild-Higher-Precategory 𝒜} → - globular-map - ( hom-globular-type-Noncoherent-Wild-Higher-Precategory 𝒜 x y) - ( hom-globular-type-Noncoherent-Wild-Higher-Precategory ℬ - ( obj-colax-functor-Noncoherent-Wild-Higher-Precategory x) - ( obj-colax-functor-Noncoherent-Wild-Higher-Precategory y)) - hom-globular-map-colax-functor-Noncoherent-Wild-Higher-Precategory = - 1-cell-globular-map-globular-map - map-colax-functor-Noncoherent-Wild-Higher-Precategory - - 2-hom-colax-functor-Noncoherent-Wild-Higher-Precategory : - {x y : obj-Noncoherent-Wild-Higher-Precategory 𝒜} - {f g : hom-Noncoherent-Wild-Higher-Precategory 𝒜 x y} → - 2-hom-Noncoherent-Wild-Higher-Precategory 𝒜 f g → - 2-hom-Noncoherent-Wild-Higher-Precategory ℬ - ( hom-colax-functor-Noncoherent-Wild-Higher-Precategory f) - ( hom-colax-functor-Noncoherent-Wild-Higher-Precategory g) - 2-hom-colax-functor-Noncoherent-Wild-Higher-Precategory = - 2-cell-globular-map map-colax-functor-Noncoherent-Wild-Higher-Precategory - - is-colax-functor-colax-functor-Noncoherent-Wild-Higher-Precategory : - is-colax-functor-Noncoherent-Wild-Higher-Precategory 𝒜 ℬ - ( map-colax-functor-Noncoherent-Wild-Higher-Precategory) - is-colax-functor-colax-functor-Noncoherent-Wild-Higher-Precategory = pr2 F -``` - -Preservation by colax functors of identity morphisms: - -```agda - preserves-id-hom-colax-functor-Noncoherent-Wild-Higher-Precategory : - (x : obj-Noncoherent-Wild-Higher-Precategory 𝒜) → - 2-hom-Noncoherent-Wild-Higher-Precategory ℬ - ( hom-colax-functor-Noncoherent-Wild-Higher-Precategory - ( id-hom-Noncoherent-Wild-Higher-Precategory 𝒜 {x})) - ( id-hom-Noncoherent-Wild-Higher-Precategory ℬ - { obj-colax-functor-Noncoherent-Wild-Higher-Precategory x}) - preserves-id-hom-colax-functor-Noncoherent-Wild-Higher-Precategory = - preserves-id-hom-is-colax-functor-Noncoherent-Wild-Higher-Precategory - ( is-colax-functor-colax-functor-Noncoherent-Wild-Higher-Precategory) - - colax-reflexive-globular-map-colax-functor-Noncoherent-Wild-Higher-Precategory : - colax-reflexive-globular-map - ( reflexive-globular-type-Noncoherent-Wild-Higher-Precategory 𝒜) - ( reflexive-globular-type-Noncoherent-Wild-Higher-Precategory ℬ) - colax-reflexive-globular-map-colax-functor-Noncoherent-Wild-Higher-Precategory = - make-colax-reflexive-globular-map - ( map-colax-functor-Noncoherent-Wild-Higher-Precategory) - ( is-reflexive-is-colax-functor-Noncoherent-Wild-Higher-Precategory - is-colax-functor-colax-functor-Noncoherent-Wild-Higher-Precategory) -``` - -Preservation by colax functors of composition: - -```agda - preserves-comp-hom-colax-functor-Noncoherent-Wild-Higher-Precategory : - {x y z : obj-Noncoherent-Wild-Higher-Precategory 𝒜} - (g : hom-Noncoherent-Wild-Higher-Precategory 𝒜 y z) - (f : hom-Noncoherent-Wild-Higher-Precategory 𝒜 x y) → - 2-hom-Noncoherent-Wild-Higher-Precategory ℬ - ( hom-colax-functor-Noncoherent-Wild-Higher-Precategory - ( comp-hom-Noncoherent-Wild-Higher-Precategory 𝒜 g f)) - ( comp-hom-Noncoherent-Wild-Higher-Precategory ℬ - ( hom-colax-functor-Noncoherent-Wild-Higher-Precategory g) - ( hom-colax-functor-Noncoherent-Wild-Higher-Precategory f)) - preserves-comp-hom-colax-functor-Noncoherent-Wild-Higher-Precategory = - preserves-comp-hom-is-colax-functor-Noncoherent-Wild-Higher-Precategory - ( is-colax-functor-colax-functor-Noncoherent-Wild-Higher-Precategory) - - colax-transitive-globular-map-colax-functor-Noncoherent-Wild-Higher-Precategory : - colax-transitive-globular-map - ( transitive-globular-type-Noncoherent-Wild-Higher-Precategory 𝒜) - ( transitive-globular-type-Noncoherent-Wild-Higher-Precategory ℬ) - colax-transitive-globular-map-colax-functor-Noncoherent-Wild-Higher-Precategory = - make-colax-transitive-globular-map - ( map-colax-functor-Noncoherent-Wild-Higher-Precategory) - ( is-transitive-is-colax-functor-Noncoherent-Wild-Higher-Precategory - is-colax-functor-colax-functor-Noncoherent-Wild-Higher-Precategory) -``` - -The induced colax functor on the wild category of morphisms between two objects: - -```agda - hom-colax-functor-colax-functor-Noncoherent-Wild-Higher-Precategory : - (x y : obj-Noncoherent-Wild-Higher-Precategory 𝒜) → - colax-functor-Noncoherent-Wild-Higher-Precategory - ( hom-noncoherent-wild-higher-precategory-Noncoherent-Wild-Higher-Precategory - ( 𝒜) - ( x) - ( y)) - ( hom-noncoherent-wild-higher-precategory-Noncoherent-Wild-Higher-Precategory - ( ℬ) - ( obj-colax-functor-Noncoherent-Wild-Higher-Precategory x) - ( obj-colax-functor-Noncoherent-Wild-Higher-Precategory y)) - hom-colax-functor-colax-functor-Noncoherent-Wild-Higher-Precategory x y = - ( hom-globular-map-colax-functor-Noncoherent-Wild-Higher-Precategory , - is-colax-functor-hom-globular-map-is-colax-functor-Noncoherent-Wild-Higher-Precategory - is-colax-functor-colax-functor-Noncoherent-Wild-Higher-Precategory) -``` - -### The identity colax functor on a noncoherent wild higher precategory - -```agda -map-id-colax-functor-Noncoherent-Wild-Higher-Precategory : - {l1 l2 : Level} (𝒜 : Noncoherent-Wild-Higher-Precategory l1 l2) → - map-Noncoherent-Wild-Higher-Precategory 𝒜 𝒜 -map-id-colax-functor-Noncoherent-Wild-Higher-Precategory 𝒜 = - id-map-Noncoherent-Wild-Higher-Precategory 𝒜 - -preserves-id-structure-id-colax-functor-Noncoherent-Wild-Higher-Precategory : - {l1 l2 : Level} (𝒜 : Noncoherent-Wild-Higher-Precategory l1 l2) → - preserves-id-structure-map-Noncoherent-Wild-Higher-Precategory 𝒜 𝒜 - ( map-id-colax-functor-Noncoherent-Wild-Higher-Precategory 𝒜) -preserves-id-structure-id-colax-functor-Noncoherent-Wild-Higher-Precategory 𝒜 = - is-colax-reflexive-id-colax-reflexive-globular-map - ( reflexive-globular-type-Noncoherent-Wild-Higher-Precategory 𝒜) - -preserves-comp-structure-id-colax-functor-Noncoherent-Wild-Higher-Precategory : - {l1 l2 : Level} (𝒜 : Noncoherent-Wild-Higher-Precategory l1 l2) → - preserves-comp-structure-map-Noncoherent-Wild-Higher-Precategory 𝒜 𝒜 - ( map-id-colax-functor-Noncoherent-Wild-Higher-Precategory 𝒜) -preserves-comp-1-cell-is-colax-transitive-globular-map - ( preserves-comp-structure-id-colax-functor-Noncoherent-Wild-Higher-Precategory - 𝒜) - _ _ = - id-2-hom-Noncoherent-Wild-Higher-Precategory 𝒜 -is-colax-transitive-1-cell-globular-map-is-colax-transitive-globular-map - ( preserves-comp-structure-id-colax-functor-Noncoherent-Wild-Higher-Precategory - 𝒜) = - preserves-comp-structure-id-colax-functor-Noncoherent-Wild-Higher-Precategory - ( hom-noncoherent-wild-higher-precategory-Noncoherent-Wild-Higher-Precategory - ( 𝒜) - ( _) - ( _)) - -is-colax-functor-id-colax-functor-Noncoherent-Wild-Higher-Precategory : - {l1 l2 : Level} (𝒜 : Noncoherent-Wild-Higher-Precategory l1 l2) → - is-colax-functor-Noncoherent-Wild-Higher-Precategory 𝒜 𝒜 - ( map-id-colax-functor-Noncoherent-Wild-Higher-Precategory 𝒜) -is-colax-functor-id-colax-functor-Noncoherent-Wild-Higher-Precategory 𝒜 = - make-is-colax-functor-Noncoherent-Wild-Higher-Precategory - ( preserves-id-structure-id-colax-functor-Noncoherent-Wild-Higher-Precategory - 𝒜) - ( preserves-comp-structure-id-colax-functor-Noncoherent-Wild-Higher-Precategory - 𝒜) - -id-colax-functor-Noncoherent-Wild-Higher-Precategory : - {l1 l2 : Level} (𝒜 : Noncoherent-Wild-Higher-Precategory l1 l2) → - colax-functor-Noncoherent-Wild-Higher-Precategory 𝒜 𝒜 -id-colax-functor-Noncoherent-Wild-Higher-Precategory 𝒜 = - ( id-map-Noncoherent-Wild-Higher-Precategory 𝒜 , - is-colax-functor-id-colax-functor-Noncoherent-Wild-Higher-Precategory 𝒜) -``` - -### Composition of colax functors between noncoherent wild higher precategories - -```agda -module _ - {l1 l2 l3 l4 l5 l6 : Level} - (𝒜 : Noncoherent-Wild-Higher-Precategory l1 l2) - (ℬ : Noncoherent-Wild-Higher-Precategory l3 l4) - (𝒞 : Noncoherent-Wild-Higher-Precategory l5 l6) - (G : colax-functor-Noncoherent-Wild-Higher-Precategory ℬ 𝒞) - (F : colax-functor-Noncoherent-Wild-Higher-Precategory 𝒜 ℬ) - where - - map-comp-colax-functor-Noncoherent-Wild-Higher-Precategory : - map-Noncoherent-Wild-Higher-Precategory 𝒜 𝒞 - map-comp-colax-functor-Noncoherent-Wild-Higher-Precategory = - comp-map-Noncoherent-Wild-Higher-Precategory 𝒜 ℬ 𝒞 - ( map-colax-functor-Noncoherent-Wild-Higher-Precategory G) - ( map-colax-functor-Noncoherent-Wild-Higher-Precategory F) - -preserves-id-structure-comp-colax-functor-Noncoherent-Wild-Higher-Precategory : - {l1 l2 l3 l4 l5 l6 : Level} - (𝒜 : Noncoherent-Wild-Higher-Precategory l1 l2) - (ℬ : Noncoherent-Wild-Higher-Precategory l3 l4) - (𝒞 : Noncoherent-Wild-Higher-Precategory l5 l6) - (G : colax-functor-Noncoherent-Wild-Higher-Precategory ℬ 𝒞) - (F : colax-functor-Noncoherent-Wild-Higher-Precategory 𝒜 ℬ) → - preserves-id-structure-map-Noncoherent-Wild-Higher-Precategory 𝒜 𝒞 - ( map-comp-colax-functor-Noncoherent-Wild-Higher-Precategory 𝒜 ℬ 𝒞 G F) -preserves-refl-1-cell-is-colax-reflexive-globular-map - ( preserves-id-structure-comp-colax-functor-Noncoherent-Wild-Higher-Precategory - 𝒜 ℬ 𝒞 G F) - x = - comp-2-hom-Noncoherent-Wild-Higher-Precategory 𝒞 - ( preserves-id-hom-colax-functor-Noncoherent-Wild-Higher-Precategory G _) - ( 2-hom-colax-functor-Noncoherent-Wild-Higher-Precategory G - ( preserves-id-hom-colax-functor-Noncoherent-Wild-Higher-Precategory F _)) -is-colax-reflexive-1-cell-globular-map-is-colax-reflexive-globular-map - ( preserves-id-structure-comp-colax-functor-Noncoherent-Wild-Higher-Precategory - 𝒜 ℬ 𝒞 G F) = - preserves-id-structure-comp-colax-functor-Noncoherent-Wild-Higher-Precategory - ( hom-noncoherent-wild-higher-precategory-Noncoherent-Wild-Higher-Precategory - 𝒜 _ _) - ( hom-noncoherent-wild-higher-precategory-Noncoherent-Wild-Higher-Precategory - ℬ _ _) - ( hom-noncoherent-wild-higher-precategory-Noncoherent-Wild-Higher-Precategory - 𝒞 _ _) - ( hom-colax-functor-colax-functor-Noncoherent-Wild-Higher-Precategory - G _ _) - ( hom-colax-functor-colax-functor-Noncoherent-Wild-Higher-Precategory - F _ _) - -module _ - {l1 l2 l3 l4 l5 l6 : Level} - (𝒜 : Noncoherent-Wild-Higher-Precategory l1 l2) - (ℬ : Noncoherent-Wild-Higher-Precategory l3 l4) - (𝒞 : Noncoherent-Wild-Higher-Precategory l5 l6) - (G : colax-functor-Noncoherent-Wild-Higher-Precategory ℬ 𝒞) - (F : colax-functor-Noncoherent-Wild-Higher-Precategory 𝒜 ℬ) - where - - preserves-comp-structure-comp-colax-functor-Noncoherent-Wild-Higher-Precategory : - preserves-comp-structure-map-Noncoherent-Wild-Higher-Precategory 𝒜 𝒞 - ( map-comp-colax-functor-Noncoherent-Wild-Higher-Precategory 𝒜 ℬ 𝒞 G F) - preserves-comp-structure-comp-colax-functor-Noncoherent-Wild-Higher-Precategory = - is-colax-transitive-comp-colax-transitive-globular-map - ( transitive-globular-type-Noncoherent-Wild-Higher-Precategory 𝒜) - ( transitive-globular-type-Noncoherent-Wild-Higher-Precategory ℬ) - ( transitive-globular-type-Noncoherent-Wild-Higher-Precategory 𝒞) - ( colax-transitive-globular-map-colax-functor-Noncoherent-Wild-Higher-Precategory - G) - ( colax-transitive-globular-map-colax-functor-Noncoherent-Wild-Higher-Precategory - F) - - is-colax-functor-comp-colax-functor-Noncoherent-Wild-Higher-Precategory : - is-colax-functor-Noncoherent-Wild-Higher-Precategory 𝒜 𝒞 - ( map-comp-colax-functor-Noncoherent-Wild-Higher-Precategory 𝒜 ℬ 𝒞 G F) - is-colax-functor-comp-colax-functor-Noncoherent-Wild-Higher-Precategory = - make-is-colax-functor-Noncoherent-Wild-Higher-Precategory - ( preserves-id-structure-comp-colax-functor-Noncoherent-Wild-Higher-Precategory - 𝒜 ℬ 𝒞 G F) - ( preserves-comp-structure-comp-colax-functor-Noncoherent-Wild-Higher-Precategory) - - comp-colax-functor-Noncoherent-Wild-Higher-Precategory : - colax-functor-Noncoherent-Wild-Higher-Precategory 𝒜 𝒞 - pr1 comp-colax-functor-Noncoherent-Wild-Higher-Precategory = - map-comp-colax-functor-Noncoherent-Wild-Higher-Precategory 𝒜 ℬ 𝒞 G F - pr2 comp-colax-functor-Noncoherent-Wild-Higher-Precategory = - is-colax-functor-comp-colax-functor-Noncoherent-Wild-Higher-Precategory -``` diff --git a/src/wild-category-theory/isomorphisms-in-noncoherent-large-wild-higher-precategories.lagda.md b/src/wild-category-theory/isomorphisms-in-noncoherent-large-wild-higher-precategories.lagda.md deleted file mode 100644 index 78566fcef7..0000000000 --- a/src/wild-category-theory/isomorphisms-in-noncoherent-large-wild-higher-precategories.lagda.md +++ /dev/null @@ -1,225 +0,0 @@ -# Isomorphisms in noncoherent large wild higher precategories - -```agda -{-# OPTIONS --guardedness #-} - -module wild-category-theory.isomorphisms-in-noncoherent-large-wild-higher-precategories where -``` - -
Imports - -```agda -open import foundation.dependent-pair-types -open import foundation.universe-levels - -open import wild-category-theory.isomorphisms-in-noncoherent-wild-higher-precategories -open import wild-category-theory.noncoherent-large-wild-higher-precategories -``` - -
- -## Idea - -Consider a -[noncoherent large wild higher precategory](wild-category-theory.noncoherent-large-wild-higher-precategories.md) -`𝒞`. An -{{#concept "isomorphism" Disambiguation="in noncoherent large wild higher precategories" Agda=is-iso-Noncoherent-Large-Wild-Higher-Precategory}} -in `𝒞` is a morphism `f : x → y` in `𝒞` [equipped](foundation.structure.md) with - -- a morphism `s : y → x` -- a $2$-morphism `is-split-epi : f ∘ s → id`, where `∘` and `id` denote - composition of morphisms and the identity morphism given by the transitive and - reflexive structure on the underlying - [globular type](globular-types.globular-types.md), respectively -- a proof `is-iso-is-split-epi : is-iso is-split-epi`, which shows that the - above $2$-morphism is itself an isomorphism -- a morphism `r : y → x` -- a $2$-morphism `is-split-mono : r ∘ f → id` -- a proof `is-iso-is-split-mono : is-iso is-split-mono`. - -This definition of an isomorphism mirrors the definition of -[biinvertible maps](foundation-core.equivalences.md) between types. - -It would be in the spirit of the library to first define what split epimorphisms -and split monomorphisms are, and then define isomorphisms as those morphisms -which are both. When attempting that definition, one runs into the problem that -the $2$-morphisms in the definitions should still be isomorphisms. - -Note that a noncoherent large wild higher precategory is the most general -setting that allows us to _define_ isomorphisms in large wild categories, but -because of the missing coherences, we cannot show any of the expected -properties. For example we cannot show that all identities are isomorphisms, or -that isomorphisms compose. - -## Definitions - -### The predicate on morphisms of being an isomorphism - -```agda -record - is-iso-Noncoherent-Large-Wild-Higher-Precategory - {α : Level → Level} {β : Level → Level → Level} - (𝒞 : Noncoherent-Large-Wild-Higher-Precategory α β) - {l1 : Level} {x : obj-Noncoherent-Large-Wild-Higher-Precategory 𝒞 l1} - {l2 : Level} {y : obj-Noncoherent-Large-Wild-Higher-Precategory 𝒞 l2} - (f : hom-Noncoherent-Large-Wild-Higher-Precategory 𝒞 x y) - : UU (β l1 l1 ⊔ β l2 l1 ⊔ β l2 l2) - where - field - hom-section-is-iso-Noncoherent-Large-Wild-Higher-Precategory : - hom-Noncoherent-Large-Wild-Higher-Precategory 𝒞 y x - is-split-epi-is-iso-Noncoherent-Large-Wild-Higher-Precategory : - 2-hom-Noncoherent-Large-Wild-Higher-Precategory 𝒞 - ( comp-hom-Noncoherent-Large-Wild-Higher-Precategory 𝒞 - ( f) - ( hom-section-is-iso-Noncoherent-Large-Wild-Higher-Precategory)) - ( id-hom-Noncoherent-Large-Wild-Higher-Precategory 𝒞) - is-iso-is-split-epi-is-iso-Noncoherent-Large-Wild-Higher-Precategory : - is-iso-Noncoherent-Wild-Higher-Precategory - ( hom-noncoherent-wild-higher-precategory-Noncoherent-Large-Wild-Higher-Precategory - ( 𝒞) - ( y) - ( y)) - ( is-split-epi-is-iso-Noncoherent-Large-Wild-Higher-Precategory) - - hom-retraction-is-iso-Noncoherent-Large-Wild-Higher-Precategory : - hom-Noncoherent-Large-Wild-Higher-Precategory 𝒞 y x - is-split-mono-is-iso-Noncoherent-Large-Wild-Higher-Precategory : - 2-hom-Noncoherent-Large-Wild-Higher-Precategory 𝒞 - ( comp-hom-Noncoherent-Large-Wild-Higher-Precategory 𝒞 - ( hom-retraction-is-iso-Noncoherent-Large-Wild-Higher-Precategory) - ( f)) - ( id-hom-Noncoherent-Large-Wild-Higher-Precategory 𝒞) - is-iso-is-split-mono-is-iso-Noncoherent-Large-Wild-Higher-Precategory : - is-iso-Noncoherent-Wild-Higher-Precategory - ( hom-noncoherent-wild-higher-precategory-Noncoherent-Large-Wild-Higher-Precategory - ( 𝒞) - ( x) - ( x)) - ( is-split-mono-is-iso-Noncoherent-Large-Wild-Higher-Precategory) - -open is-iso-Noncoherent-Large-Wild-Higher-Precategory public -``` - -### Isomorphisms in a noncoherent large wild higher precategory - -```agda -iso-Noncoherent-Large-Wild-Higher-Precategory : - {α : Level → Level} {β : Level → Level → Level} - (𝒞 : Noncoherent-Large-Wild-Higher-Precategory α β) - {l1 : Level} (x : obj-Noncoherent-Large-Wild-Higher-Precategory 𝒞 l1) - {l2 : Level} (y : obj-Noncoherent-Large-Wild-Higher-Precategory 𝒞 l2) → - UU (β l1 l1 ⊔ β l1 l2 ⊔ β l2 l1 ⊔ β l2 l2) -iso-Noncoherent-Large-Wild-Higher-Precategory 𝒞 x y = - Σ ( hom-Noncoherent-Large-Wild-Higher-Precategory 𝒞 x y) - ( is-iso-Noncoherent-Large-Wild-Higher-Precategory 𝒞) -``` - -### Components of an isomorphism in a noncoherent large wild higher precategory - -```agda -module _ - {α : Level → Level} {β : Level → Level → Level} - {𝒞 : Noncoherent-Large-Wild-Higher-Precategory α β} - {l1 : Level} {x : obj-Noncoherent-Large-Wild-Higher-Precategory 𝒞 l1} - {l2 : Level} {y : obj-Noncoherent-Large-Wild-Higher-Precategory 𝒞 l2} - (f : iso-Noncoherent-Large-Wild-Higher-Precategory 𝒞 x y) - where - - hom-iso-Noncoherent-Large-Wild-Higher-Precategory : - hom-Noncoherent-Large-Wild-Higher-Precategory 𝒞 x y - hom-iso-Noncoherent-Large-Wild-Higher-Precategory = pr1 f - - is-iso-hom-iso-Noncoherent-Large-Wild-Higher-Precategory : - is-iso-Noncoherent-Large-Wild-Higher-Precategory 𝒞 - ( hom-iso-Noncoherent-Large-Wild-Higher-Precategory) - is-iso-hom-iso-Noncoherent-Large-Wild-Higher-Precategory = pr2 f - - hom-section-iso-Noncoherent-Large-Wild-Higher-Precategory : - hom-Noncoherent-Large-Wild-Higher-Precategory 𝒞 y x - hom-section-iso-Noncoherent-Large-Wild-Higher-Precategory = - hom-section-is-iso-Noncoherent-Large-Wild-Higher-Precategory - ( is-iso-hom-iso-Noncoherent-Large-Wild-Higher-Precategory) - - is-split-epi-iso-Noncoherent-Large-Wild-Higher-Precategory : - 2-hom-Noncoherent-Large-Wild-Higher-Precategory 𝒞 - ( comp-hom-Noncoherent-Large-Wild-Higher-Precategory 𝒞 - ( hom-iso-Noncoherent-Large-Wild-Higher-Precategory) - ( hom-section-iso-Noncoherent-Large-Wild-Higher-Precategory)) - ( id-hom-Noncoherent-Large-Wild-Higher-Precategory 𝒞) - is-split-epi-iso-Noncoherent-Large-Wild-Higher-Precategory = - is-split-epi-is-iso-Noncoherent-Large-Wild-Higher-Precategory - ( is-iso-hom-iso-Noncoherent-Large-Wild-Higher-Precategory) - - is-iso-is-split-epi-iso-Noncoherent-Large-Wild-Higher-Precategory : - is-iso-Noncoherent-Wild-Higher-Precategory - ( hom-noncoherent-wild-higher-precategory-Noncoherent-Large-Wild-Higher-Precategory - ( 𝒞) - ( y) - ( y)) - ( is-split-epi-iso-Noncoherent-Large-Wild-Higher-Precategory) - is-iso-is-split-epi-iso-Noncoherent-Large-Wild-Higher-Precategory = - is-iso-is-split-epi-is-iso-Noncoherent-Large-Wild-Higher-Precategory - ( is-iso-hom-iso-Noncoherent-Large-Wild-Higher-Precategory) - - iso-is-split-epi-iso-Noncoherent-Large-Wild-Higher-Precategory : - iso-Noncoherent-Wild-Higher-Precategory - ( hom-noncoherent-wild-higher-precategory-Noncoherent-Large-Wild-Higher-Precategory - ( 𝒞) - ( y) - ( y)) - ( comp-hom-Noncoherent-Large-Wild-Higher-Precategory 𝒞 - ( hom-iso-Noncoherent-Large-Wild-Higher-Precategory) - ( hom-section-iso-Noncoherent-Large-Wild-Higher-Precategory)) - ( id-hom-Noncoherent-Large-Wild-Higher-Precategory 𝒞) - pr1 iso-is-split-epi-iso-Noncoherent-Large-Wild-Higher-Precategory = - is-split-epi-iso-Noncoherent-Large-Wild-Higher-Precategory - pr2 iso-is-split-epi-iso-Noncoherent-Large-Wild-Higher-Precategory = - is-iso-is-split-epi-iso-Noncoherent-Large-Wild-Higher-Precategory - - hom-retraction-iso-Noncoherent-Large-Wild-Higher-Precategory : - hom-Noncoherent-Large-Wild-Higher-Precategory 𝒞 y x - hom-retraction-iso-Noncoherent-Large-Wild-Higher-Precategory = - hom-retraction-is-iso-Noncoherent-Large-Wild-Higher-Precategory - ( is-iso-hom-iso-Noncoherent-Large-Wild-Higher-Precategory) - - is-split-mono-iso-Noncoherent-Large-Wild-Higher-Precategory : - 2-hom-Noncoherent-Large-Wild-Higher-Precategory 𝒞 - ( comp-hom-Noncoherent-Large-Wild-Higher-Precategory 𝒞 - ( hom-retraction-iso-Noncoherent-Large-Wild-Higher-Precategory) - ( hom-iso-Noncoherent-Large-Wild-Higher-Precategory)) - ( id-hom-Noncoherent-Large-Wild-Higher-Precategory 𝒞) - is-split-mono-iso-Noncoherent-Large-Wild-Higher-Precategory = - is-split-mono-is-iso-Noncoherent-Large-Wild-Higher-Precategory - ( is-iso-hom-iso-Noncoherent-Large-Wild-Higher-Precategory) - - is-iso-is-split-mono-iso-Noncoherent-Large-Wild-Higher-Precategory : - is-iso-Noncoherent-Wild-Higher-Precategory - ( hom-noncoherent-wild-higher-precategory-Noncoherent-Large-Wild-Higher-Precategory - ( 𝒞) - ( x) - ( x)) - ( is-split-mono-iso-Noncoherent-Large-Wild-Higher-Precategory) - is-iso-is-split-mono-iso-Noncoherent-Large-Wild-Higher-Precategory = - is-iso-is-split-mono-is-iso-Noncoherent-Large-Wild-Higher-Precategory - ( is-iso-hom-iso-Noncoherent-Large-Wild-Higher-Precategory) - - iso-is-split-mono-iso-Noncoherent-Large-Wild-Higher-Precategory : - iso-Noncoherent-Wild-Higher-Precategory - ( hom-noncoherent-wild-higher-precategory-Noncoherent-Large-Wild-Higher-Precategory - ( 𝒞) - ( x) - ( x)) - ( comp-hom-Noncoherent-Large-Wild-Higher-Precategory 𝒞 - ( hom-retraction-iso-Noncoherent-Large-Wild-Higher-Precategory) - ( hom-iso-Noncoherent-Large-Wild-Higher-Precategory)) - ( id-hom-Noncoherent-Large-Wild-Higher-Precategory 𝒞) - pr1 iso-is-split-mono-iso-Noncoherent-Large-Wild-Higher-Precategory = - is-split-mono-iso-Noncoherent-Large-Wild-Higher-Precategory - pr2 iso-is-split-mono-iso-Noncoherent-Large-Wild-Higher-Precategory = - is-iso-is-split-mono-iso-Noncoherent-Large-Wild-Higher-Precategory -``` - -## See also - -- [Isomorphisms in noncoherent wild higher precategories](wild-category-theory.isomorphisms-in-noncoherent-wild-higher-precategories.md) diff --git a/src/wild-category-theory/isomorphisms-in-noncoherent-wild-higher-precategories.lagda.md b/src/wild-category-theory/isomorphisms-in-noncoherent-wild-higher-precategories.lagda.md deleted file mode 100644 index e0d30bc8ae..0000000000 --- a/src/wild-category-theory/isomorphisms-in-noncoherent-wild-higher-precategories.lagda.md +++ /dev/null @@ -1,221 +0,0 @@ -# Isomorphisms in noncoherent wild higher precategories - -```agda -{-# OPTIONS --guardedness #-} - -module wild-category-theory.isomorphisms-in-noncoherent-wild-higher-precategories where -``` - -
Imports - -```agda -open import foundation.dependent-pair-types -open import foundation.universe-levels - -open import wild-category-theory.noncoherent-wild-higher-precategories -``` - -
- -## Idea - -Consider a -[noncoherent wild higher precategory](wild-category-theory.noncoherent-wild-higher-precategories.md) -`𝒞`. An -{{#concept "isomorphism" Disambiguation="in noncoherent wild higher precategories" Agda=is-iso-Noncoherent-Wild-Higher-Precategory}} -in `𝒞` is a morphism `f : x → y` in `𝒞` [equipped](foundation.structure.md) with - -- a morphism `s : y → x` -- a $2$-morphism `is-split-epi : f ∘ s → id`, where `∘` and `id` denote - composition of morphisms and the identity morphism given by the transitive and - reflexive structure on the underlying - [globular type](globular-types.globular-types.md), respectively -- a proof `is-iso-is-split-epi : is-iso is-split-epi`, which shows that the - above $2$-morphism is itself an isomorphism -- a morphism `r : y → x` -- a $2$-morphism `is-split-mono : r ∘ f → id` -- a proof `is-iso-is-split-mono : is-iso is-split-mono`. - -This definition of an isomorphism mirrors the definition of -[biinvertible maps](foundation-core.equivalences.md) between types. - -It would be in the spirit of the library to first define what split epimorphisms -and split monomorphisms are, and then define isomorphisms as those morphisms -which are both. When attempting that definition, one runs into the problem that -the $2$-morphisms in the definitions should still be isomorphisms. -Alternatively, one could require that the morphisms compose to the identity -morphism up to [identification](foundation-core.identity-types.md) of morphisms, -instead of up to a higher isomorphism. - -Note that a noncoherent wild higher precategory is the most general setting that -allows us to _define_ isomorphisms in wild categories, but because of the -missing coherences, we cannot show any of the expected properties. For example -we cannot show that all identities are isomorphisms, or that isomorphisms -compose. - -## Definitions - -### The predicate on a morphism of being an isomorphism - -```agda -record - is-iso-Noncoherent-Wild-Higher-Precategory - {l1 l2 : Level} (𝒞 : Noncoherent-Wild-Higher-Precategory l1 l2) - {x y : obj-Noncoherent-Wild-Higher-Precategory 𝒞} - (f : hom-Noncoherent-Wild-Higher-Precategory 𝒞 x y) : UU l2 - where - coinductive - field - hom-section-is-iso-Noncoherent-Wild-Higher-Precategory : - hom-Noncoherent-Wild-Higher-Precategory 𝒞 y x - is-split-epi-is-iso-Noncoherent-Wild-Higher-Precategory : - 2-hom-Noncoherent-Wild-Higher-Precategory 𝒞 - ( comp-hom-Noncoherent-Wild-Higher-Precategory 𝒞 - ( f) - ( hom-section-is-iso-Noncoherent-Wild-Higher-Precategory)) - ( id-hom-Noncoherent-Wild-Higher-Precategory 𝒞) - is-iso-is-split-epi-is-iso-Noncoherent-Wild-Higher-Precategory : - is-iso-Noncoherent-Wild-Higher-Precategory - ( hom-noncoherent-wild-higher-precategory-Noncoherent-Wild-Higher-Precategory - ( 𝒞) - ( y) - ( y)) - ( is-split-epi-is-iso-Noncoherent-Wild-Higher-Precategory) - - hom-retraction-is-iso-Noncoherent-Wild-Higher-Precategory : - hom-Noncoherent-Wild-Higher-Precategory 𝒞 y x - is-split-mono-is-iso-Noncoherent-Wild-Higher-Precategory : - 2-hom-Noncoherent-Wild-Higher-Precategory 𝒞 - ( comp-hom-Noncoherent-Wild-Higher-Precategory 𝒞 - ( hom-retraction-is-iso-Noncoherent-Wild-Higher-Precategory) - ( f)) - ( id-hom-Noncoherent-Wild-Higher-Precategory 𝒞) - is-iso-is-split-mono-is-iso-Noncoherent-Wild-Higher-Precategory : - is-iso-Noncoherent-Wild-Higher-Precategory - ( hom-noncoherent-wild-higher-precategory-Noncoherent-Wild-Higher-Precategory - ( 𝒞) - ( x) - ( x)) - ( is-split-mono-is-iso-Noncoherent-Wild-Higher-Precategory) - -open is-iso-Noncoherent-Wild-Higher-Precategory public -``` - -### Isomorphisms in a noncoherent wild higher precategory - -```agda -iso-Noncoherent-Wild-Higher-Precategory : - {l1 l2 : Level} (𝒞 : Noncoherent-Wild-Higher-Precategory l1 l2) - (x y : obj-Noncoherent-Wild-Higher-Precategory 𝒞) → - UU l2 -iso-Noncoherent-Wild-Higher-Precategory 𝒞 x y = - Σ ( hom-Noncoherent-Wild-Higher-Precategory 𝒞 x y) - ( is-iso-Noncoherent-Wild-Higher-Precategory 𝒞) -``` - -### Components of an isomorphism in a noncoherent wild higher precategory - -```agda -module _ - {l1 l2 : Level} {𝒞 : Noncoherent-Wild-Higher-Precategory l1 l2} - {x y : obj-Noncoherent-Wild-Higher-Precategory 𝒞} - (f : iso-Noncoherent-Wild-Higher-Precategory 𝒞 x y) - where - - hom-iso-Noncoherent-Wild-Higher-Precategory : - hom-Noncoherent-Wild-Higher-Precategory 𝒞 x y - hom-iso-Noncoherent-Wild-Higher-Precategory = pr1 f - - is-iso-hom-iso-Noncoherent-Wild-Higher-Precategory : - is-iso-Noncoherent-Wild-Higher-Precategory 𝒞 - ( hom-iso-Noncoherent-Wild-Higher-Precategory) - is-iso-hom-iso-Noncoherent-Wild-Higher-Precategory = pr2 f - - hom-section-iso-Noncoherent-Wild-Higher-Precategory : - hom-Noncoherent-Wild-Higher-Precategory 𝒞 y x - hom-section-iso-Noncoherent-Wild-Higher-Precategory = - hom-section-is-iso-Noncoherent-Wild-Higher-Precategory - ( is-iso-hom-iso-Noncoherent-Wild-Higher-Precategory) - - is-split-epi-iso-Noncoherent-Wild-Higher-Precategory : - 2-hom-Noncoherent-Wild-Higher-Precategory 𝒞 - ( comp-hom-Noncoherent-Wild-Higher-Precategory 𝒞 - ( hom-iso-Noncoherent-Wild-Higher-Precategory) - ( hom-section-iso-Noncoherent-Wild-Higher-Precategory)) - ( id-hom-Noncoherent-Wild-Higher-Precategory 𝒞) - is-split-epi-iso-Noncoherent-Wild-Higher-Precategory = - is-split-epi-is-iso-Noncoherent-Wild-Higher-Precategory - ( is-iso-hom-iso-Noncoherent-Wild-Higher-Precategory) - - is-iso-is-split-epi-iso-Noncoherent-Wild-Higher-Precategory : - is-iso-Noncoherent-Wild-Higher-Precategory - ( hom-noncoherent-wild-higher-precategory-Noncoherent-Wild-Higher-Precategory - ( 𝒞) - ( y) - ( y)) - ( is-split-epi-iso-Noncoherent-Wild-Higher-Precategory) - is-iso-is-split-epi-iso-Noncoherent-Wild-Higher-Precategory = - is-iso-is-split-epi-is-iso-Noncoherent-Wild-Higher-Precategory - ( is-iso-hom-iso-Noncoherent-Wild-Higher-Precategory) - - iso-is-split-epi-iso-Noncoherent-Wild-Higher-Precategory : - iso-Noncoherent-Wild-Higher-Precategory - ( hom-noncoherent-wild-higher-precategory-Noncoherent-Wild-Higher-Precategory - ( 𝒞) - ( y) - ( y)) - ( comp-hom-Noncoherent-Wild-Higher-Precategory 𝒞 - ( hom-iso-Noncoherent-Wild-Higher-Precategory) - ( hom-section-iso-Noncoherent-Wild-Higher-Precategory)) - ( id-hom-Noncoherent-Wild-Higher-Precategory 𝒞) - pr1 iso-is-split-epi-iso-Noncoherent-Wild-Higher-Precategory = - is-split-epi-iso-Noncoherent-Wild-Higher-Precategory - pr2 iso-is-split-epi-iso-Noncoherent-Wild-Higher-Precategory = - is-iso-is-split-epi-iso-Noncoherent-Wild-Higher-Precategory - - hom-retraction-iso-Noncoherent-Wild-Higher-Precategory : - hom-Noncoherent-Wild-Higher-Precategory 𝒞 y x - hom-retraction-iso-Noncoherent-Wild-Higher-Precategory = - hom-retraction-is-iso-Noncoherent-Wild-Higher-Precategory - ( is-iso-hom-iso-Noncoherent-Wild-Higher-Precategory) - - is-split-mono-iso-Noncoherent-Wild-Higher-Precategory : - 2-hom-Noncoherent-Wild-Higher-Precategory 𝒞 - ( comp-hom-Noncoherent-Wild-Higher-Precategory 𝒞 - ( hom-retraction-iso-Noncoherent-Wild-Higher-Precategory) - ( hom-iso-Noncoherent-Wild-Higher-Precategory)) - ( id-hom-Noncoherent-Wild-Higher-Precategory 𝒞) - is-split-mono-iso-Noncoherent-Wild-Higher-Precategory = - is-split-mono-is-iso-Noncoherent-Wild-Higher-Precategory - ( is-iso-hom-iso-Noncoherent-Wild-Higher-Precategory) - - is-iso-is-split-mono-iso-Noncoherent-Wild-Higher-Precategory : - is-iso-Noncoherent-Wild-Higher-Precategory - ( hom-noncoherent-wild-higher-precategory-Noncoherent-Wild-Higher-Precategory - ( 𝒞) - ( x) - ( x)) - ( is-split-mono-iso-Noncoherent-Wild-Higher-Precategory) - is-iso-is-split-mono-iso-Noncoherent-Wild-Higher-Precategory = - is-iso-is-split-mono-is-iso-Noncoherent-Wild-Higher-Precategory - ( is-iso-hom-iso-Noncoherent-Wild-Higher-Precategory) - - iso-is-split-mono-iso-Noncoherent-Wild-Higher-Precategory : - iso-Noncoherent-Wild-Higher-Precategory - ( hom-noncoherent-wild-higher-precategory-Noncoherent-Wild-Higher-Precategory - ( 𝒞) - ( x) - ( x)) - ( comp-hom-Noncoherent-Wild-Higher-Precategory 𝒞 - ( hom-retraction-iso-Noncoherent-Wild-Higher-Precategory) - ( hom-iso-Noncoherent-Wild-Higher-Precategory)) - ( id-hom-Noncoherent-Wild-Higher-Precategory 𝒞) - pr1 iso-is-split-mono-iso-Noncoherent-Wild-Higher-Precategory = - is-split-mono-iso-Noncoherent-Wild-Higher-Precategory - pr2 iso-is-split-mono-iso-Noncoherent-Wild-Higher-Precategory = - is-iso-is-split-mono-iso-Noncoherent-Wild-Higher-Precategory -``` - -## See also - -- [Isomorphisms in noncoherent large wild higher precategories](wild-category-theory.isomorphisms-in-noncoherent-large-wild-higher-precategories.md) diff --git a/src/wild-category-theory/maps-noncoherent-large-omega-precategories.lagda.md b/src/wild-category-theory/maps-noncoherent-large-omega-precategories.lagda.md new file mode 100644 index 0000000000..e7adea0a47 --- /dev/null +++ b/src/wild-category-theory/maps-noncoherent-large-omega-precategories.lagda.md @@ -0,0 +1,166 @@ +# Maps between noncoherent large ω-precategories + +```agda +{-# OPTIONS --guardedness #-} + +module wild-category-theory.maps-noncoherent-large-omega-precategories where +``` + +
Imports + +```agda +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-globular-maps +open import globular-types.large-globular-types + +open import wild-category-theory.maps-noncoherent-omega-precategories +open import wild-category-theory.noncoherent-large-omega-precategories +open import wild-category-theory.noncoherent-omega-precategories +``` + +
+ +## Idea + +A +{{#concept "map" Disambiguation="between noncoherent large ω-precategories" Agda=map-Noncoherent-Large-ω-Precategory}} +`f` between +[noncoherent large ω-precategories](wild-category-theory.noncoherent-large-omega-precategories.md) +`𝒜` and `ℬ` is a [large globular map](globular-types.large-globular-maps.md) +between their underlying +[large globular types](globular-types.large-globular-types.md). More +specifically, maps between noncoherent large ω-precategories consist of a map on +objects `F₀ : obj 𝒜 → obj ℬ`, and for every pair of $n$-morphisms `f` and `g`, a +map of $(n+1)$-morphisms + +```text + Fₙ₊₁ : (𝑛+1)-hom 𝒞 f g → (𝑛+1)-hom 𝒟 (Fₙ f) (Fₙ g). +``` + +A map between noncoherent large ω-precategories does not have to preserve the +identities or composition in any shape or form, and is the least structured +notion of a "morphism" between noncoherent ω-precategories. For a notion of +"morphism" between noncoherent large ω-precategories that in one sense preserves +this additional structure, see +[colax functors between noncoherent large ω-precategories](wild-category-theory.colax-functors-noncoherent-large-omega-precategories.md). + +## Definitions + +### Maps between noncoherent large ω-precategories + +```agda +map-Noncoherent-Large-ω-Precategory : + {α1 α2 : Level → Level} {β1 β2 : Level → Level → Level} (δ : Level → Level) + (𝒜 : Noncoherent-Large-ω-Precategory α1 β1) + (ℬ : Noncoherent-Large-ω-Precategory α2 β2) → UUω +map-Noncoherent-Large-ω-Precategory δ 𝒜 ℬ = + large-globular-map δ + ( large-globular-type-Noncoherent-Large-ω-Precategory 𝒜) + ( large-globular-type-Noncoherent-Large-ω-Precategory ℬ) + +module _ + {α1 α2 : Level → Level} {β1 β2 : Level → Level → Level} {δ : Level → Level} + (𝒜 : Noncoherent-Large-ω-Precategory α1 β1) + (ℬ : Noncoherent-Large-ω-Precategory α2 β2) + (F : map-Noncoherent-Large-ω-Precategory δ 𝒜 ℬ) + where + + obj-map-Noncoherent-Large-ω-Precategory : + {l : Level} → + obj-Noncoherent-Large-ω-Precategory 𝒜 l → + obj-Noncoherent-Large-ω-Precategory ℬ (δ l) + obj-map-Noncoherent-Large-ω-Precategory = + 0-cell-large-globular-map F + + hom-globular-map-map-Noncoherent-Large-ω-Precategory : + {l1 l2 : Level} + {x : obj-Noncoherent-Large-ω-Precategory 𝒜 l1} + {y : obj-Noncoherent-Large-ω-Precategory 𝒜 l2} → + globular-map + ( hom-globular-type-Noncoherent-Large-ω-Precategory 𝒜 x y) + ( hom-globular-type-Noncoherent-Large-ω-Precategory ℬ + ( obj-map-Noncoherent-Large-ω-Precategory x) + ( obj-map-Noncoherent-Large-ω-Precategory y)) + hom-globular-map-map-Noncoherent-Large-ω-Precategory = + 1-cell-globular-map-large-globular-map F + + hom-map-Noncoherent-Large-ω-Precategory : + {l1 l2 : Level} + {x : obj-Noncoherent-Large-ω-Precategory 𝒜 l1} + {y : obj-Noncoherent-Large-ω-Precategory 𝒜 l2} → + hom-Noncoherent-Large-ω-Precategory 𝒜 x y → + hom-Noncoherent-Large-ω-Precategory ℬ + ( obj-map-Noncoherent-Large-ω-Precategory x) + ( obj-map-Noncoherent-Large-ω-Precategory y) + hom-map-Noncoherent-Large-ω-Precategory = + 1-cell-large-globular-map F + + 2-hom-map-Noncoherent-Large-ω-Precategory : + {l1 l2 : Level} + {x : obj-Noncoherent-Large-ω-Precategory 𝒜 l1} + {y : obj-Noncoherent-Large-ω-Precategory 𝒜 l2} + {f g : hom-Noncoherent-Large-ω-Precategory 𝒜 x y} → + 2-hom-Noncoherent-Large-ω-Precategory 𝒜 f g → + 2-hom-Noncoherent-Large-ω-Precategory ℬ + ( hom-map-Noncoherent-Large-ω-Precategory f) + ( hom-map-Noncoherent-Large-ω-Precategory g) + 2-hom-map-Noncoherent-Large-ω-Precategory = + 2-cell-large-globular-map F + + hom-noncoherent-ω-precategory-map-Noncoherent-Large-ω-Precategory : + {l1 l2 : Level} + (x : obj-Noncoherent-Large-ω-Precategory 𝒜 l1) + (y : obj-Noncoherent-Large-ω-Precategory 𝒜 l2) → + map-Noncoherent-ω-Precategory + ( hom-noncoherent-ω-precategory-Noncoherent-Large-ω-Precategory + ( 𝒜) + ( x) + ( y)) + ( hom-noncoherent-ω-precategory-Noncoherent-Large-ω-Precategory + ( ℬ) + ( obj-map-Noncoherent-Large-ω-Precategory x) + ( obj-map-Noncoherent-Large-ω-Precategory y)) + hom-noncoherent-ω-precategory-map-Noncoherent-Large-ω-Precategory + _ _ = + 1-cell-globular-map-large-globular-map F +``` + +### The identity map on a noncoherent large ω-precategory + +```agda +module _ + {α : Level → Level} {β : Level → Level → Level} + (𝒜 : Noncoherent-Large-ω-Precategory α β) + where + + id-map-Noncoherent-Large-ω-Precategory : + map-Noncoherent-Large-ω-Precategory (λ l → l) 𝒜 𝒜 + id-map-Noncoherent-Large-ω-Precategory = + id-large-globular-map _ +``` + +### Composition of maps of noncoherent large ω-precategories + +```agda +module _ + {α1 α2 α3 : Level → Level} + {β1 β2 β3 : Level → Level → Level} + {δ1 δ2 : Level → Level} + (𝒜 : Noncoherent-Large-ω-Precategory α1 β1) + (ℬ : Noncoherent-Large-ω-Precategory α2 β2) + (𝒞 : Noncoherent-Large-ω-Precategory α3 β3) + (G : map-Noncoherent-Large-ω-Precategory δ2 ℬ 𝒞) + (F : map-Noncoherent-Large-ω-Precategory δ1 𝒜 ℬ) + where + + comp-map-Noncoherent-Large-ω-Precategory : + map-Noncoherent-Large-ω-Precategory (λ l → δ2 (δ1 l)) 𝒜 𝒞 + comp-map-Noncoherent-Large-ω-Precategory = + comp-large-globular-map G F +``` diff --git a/src/wild-category-theory/maps-noncoherent-large-wild-higher-precategories.lagda.md b/src/wild-category-theory/maps-noncoherent-large-wild-higher-precategories.lagda.md deleted file mode 100644 index 669a93f24b..0000000000 --- a/src/wild-category-theory/maps-noncoherent-large-wild-higher-precategories.lagda.md +++ /dev/null @@ -1,166 +0,0 @@ -# Maps between noncoherent large wild higher precategories - -```agda -{-# OPTIONS --guardedness #-} - -module wild-category-theory.maps-noncoherent-large-wild-higher-precategories where -``` - -
Imports - -```agda -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-globular-maps -open import globular-types.large-globular-types - -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 -{{#concept "map" Disambiguation="between noncoherent large wild higher precategories" Agda=map-Noncoherent-Large-Wild-Higher-Precategory}} -`f` between -[noncoherent large wild higher precategories](wild-category-theory.noncoherent-large-wild-higher-precategories.md) -`𝒜` and `ℬ` is a [large globular map](globular-types.large-globular-maps.md) -between their underlying -[large globular types](globular-types.large-globular-types.md). More -specifically, maps between noncoherent large wild higher precategories consist -of a map on objects `F₀ : obj 𝒜 → obj ℬ`, and for every pair of $n$-morphisms -`f` and `g`, a map of $(n+1)$-morphisms - -```text - Fₙ₊₁ : (𝑛+1)-hom 𝒞 f g → (𝑛+1)-hom 𝒟 (Fₙ f) (Fₙ g). -``` - -A map between noncoherent large wild higher precategories does not have to -preserve the identities or composition in any shape or form, and is the least -structured notion of a "morphism" between noncoherent wild higher precategories. -For a notion of "morphism" between noncoherent large wild higher precategories -that in one sense preserves this additional structure, see -[colax functors between noncoherent large wild higher precategories](wild-category-theory.colax-functors-noncoherent-large-wild-higher-precategories.md). - -## Definitions - -### Maps between noncoherent large wild higher precategories - -```agda -map-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ω -map-Noncoherent-Large-Wild-Higher-Precategory δ 𝒜 ℬ = - large-globular-map δ - ( large-globular-type-Noncoherent-Large-Wild-Higher-Precategory 𝒜) - ( large-globular-type-Noncoherent-Large-Wild-Higher-Precategory ℬ) - -module _ - {α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 δ 𝒜 ℬ) - where - - obj-map-Noncoherent-Large-Wild-Higher-Precategory : - {l : Level} → - obj-Noncoherent-Large-Wild-Higher-Precategory 𝒜 l → - obj-Noncoherent-Large-Wild-Higher-Precategory ℬ (δ l) - obj-map-Noncoherent-Large-Wild-Higher-Precategory = - 0-cell-large-globular-map F - - hom-globular-map-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} → - globular-map - ( hom-globular-type-Noncoherent-Large-Wild-Higher-Precategory 𝒜 x y) - ( hom-globular-type-Noncoherent-Large-Wild-Higher-Precategory ℬ - ( obj-map-Noncoherent-Large-Wild-Higher-Precategory x) - ( obj-map-Noncoherent-Large-Wild-Higher-Precategory y)) - hom-globular-map-map-Noncoherent-Large-Wild-Higher-Precategory = - 1-cell-globular-map-large-globular-map F - - hom-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} → - hom-Noncoherent-Large-Wild-Higher-Precategory 𝒜 x y → - hom-Noncoherent-Large-Wild-Higher-Precategory ℬ - ( obj-map-Noncoherent-Large-Wild-Higher-Precategory x) - ( obj-map-Noncoherent-Large-Wild-Higher-Precategory y) - hom-map-Noncoherent-Large-Wild-Higher-Precategory = - 1-cell-large-globular-map F - - 2-hom-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} - {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-map-Noncoherent-Large-Wild-Higher-Precategory f) - ( hom-map-Noncoherent-Large-Wild-Higher-Precategory g) - 2-hom-map-Noncoherent-Large-Wild-Higher-Precategory = - 2-cell-large-globular-map F - - hom-noncoherent-wild-higher-precategory-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) → - 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 - ( ℬ) - ( obj-map-Noncoherent-Large-Wild-Higher-Precategory x) - ( obj-map-Noncoherent-Large-Wild-Higher-Precategory y)) - hom-noncoherent-wild-higher-precategory-map-Noncoherent-Large-Wild-Higher-Precategory - _ _ = - 1-cell-globular-map-large-globular-map F -``` - -### The identity map on a noncoherent large wild higher precategory - -```agda -module _ - {α : Level → Level} {β : Level → Level → Level} - (𝒜 : Noncoherent-Large-Wild-Higher-Precategory α β) - where - - id-map-Noncoherent-Large-Wild-Higher-Precategory : - map-Noncoherent-Large-Wild-Higher-Precategory (λ l → l) 𝒜 𝒜 - id-map-Noncoherent-Large-Wild-Higher-Precategory = - id-large-globular-map _ -``` - -### Composition of maps of noncoherent large wild higher precategories - -```agda -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 : map-Noncoherent-Large-Wild-Higher-Precategory δ2 ℬ 𝒞) - (F : map-Noncoherent-Large-Wild-Higher-Precategory δ1 𝒜 ℬ) - where - - comp-map-Noncoherent-Large-Wild-Higher-Precategory : - map-Noncoherent-Large-Wild-Higher-Precategory (λ l → δ2 (δ1 l)) 𝒜 𝒞 - comp-map-Noncoherent-Large-Wild-Higher-Precategory = - comp-large-globular-map G F -``` diff --git a/src/wild-category-theory/maps-noncoherent-omega-precategories.lagda.md b/src/wild-category-theory/maps-noncoherent-omega-precategories.lagda.md new file mode 100644 index 0000000000..2573be3c1a --- /dev/null +++ b/src/wild-category-theory/maps-noncoherent-omega-precategories.lagda.md @@ -0,0 +1,151 @@ +# Maps between noncoherent ω-precategories + +```agda +{-# OPTIONS --guardedness #-} + +module wild-category-theory.maps-noncoherent-omega-precategories where +``` + +
Imports + +```agda +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 wild-category-theory.noncoherent-omega-precategories +``` + +
+ +## Idea + +A +{{#concept "map" Disambiguation="between noncoherent ω-precategories" Agda=map-Noncoherent-ω-Precategory}} +`f` between +[noncoherent ω-precategories](wild-category-theory.noncoherent-omega-precategories.md) +`𝒜` and `ℬ` is a [globular map](globular-types.globular-maps.md) between their +underlying [globular types](globular-types.globular-types.md). More +specifically, a map `F` between noncoherent ω-precategories consists of a map on +objects `F₀ : obj 𝒜 → obj ℬ`, and for every pair of $n$-morphisms `f` and `g`, a +map of $(n+1)$-morphisms + +```text + Fₙ₊₁ : (𝑛+1)-hom 𝒞 f g → (𝑛+1)-hom 𝒟 (Fₙ f) (Fₙ g). +``` + +A map between noncoherent ω-precategories does not have to preserve the +identities or composition in any shape or form, and is the least structured +notion of a "morphism" between noncoherent ω-precategories. For a notion of +"morphism" between noncoherent ω-precategories that in one sense preserves this +additional structure, see +[colax functors between noncoherent ω-precategories](wild-category-theory.colax-functors-noncoherent-omega-precategories.md). + +## Definitions + +### Maps between noncoherent ω-precategories + +```agda +map-Noncoherent-ω-Precategory : + {l1 l2 l3 l4 : Level} + (𝒜 : Noncoherent-ω-Precategory l1 l2) + (ℬ : Noncoherent-ω-Precategory l3 l4) → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) +map-Noncoherent-ω-Precategory 𝒜 ℬ = + globular-map + ( globular-type-Noncoherent-ω-Precategory 𝒜) + ( globular-type-Noncoherent-ω-Precategory ℬ) + +module _ + {l1 l2 l3 l4 : Level} + (𝒜 : Noncoherent-ω-Precategory l1 l2) + (ℬ : Noncoherent-ω-Precategory l3 l4) + (F : map-Noncoherent-ω-Precategory 𝒜 ℬ) + where + + obj-map-Noncoherent-ω-Precategory : + obj-Noncoherent-ω-Precategory 𝒜 → + obj-Noncoherent-ω-Precategory ℬ + obj-map-Noncoherent-ω-Precategory = + 0-cell-globular-map F + + hom-globular-map-map-Noncoherent-ω-Precategory : + {x y : obj-Noncoherent-ω-Precategory 𝒜} → + globular-map + ( hom-globular-type-Noncoherent-ω-Precategory 𝒜 x y) + ( hom-globular-type-Noncoherent-ω-Precategory ℬ + ( obj-map-Noncoherent-ω-Precategory x) + ( obj-map-Noncoherent-ω-Precategory y)) + hom-globular-map-map-Noncoherent-ω-Precategory = + 1-cell-globular-map-globular-map F + + hom-map-Noncoherent-ω-Precategory : + {x y : obj-Noncoherent-ω-Precategory 𝒜} → + hom-Noncoherent-ω-Precategory 𝒜 x y → + hom-Noncoherent-ω-Precategory ℬ + ( obj-map-Noncoherent-ω-Precategory x) + ( obj-map-Noncoherent-ω-Precategory y) + hom-map-Noncoherent-ω-Precategory = + 0-cell-globular-map + ( hom-globular-map-map-Noncoherent-ω-Precategory) + + 2-hom-map-Noncoherent-ω-Precategory : + {x y : obj-Noncoherent-ω-Precategory 𝒜} + {f g : hom-Noncoherent-ω-Precategory 𝒜 x y} → + 2-hom-Noncoherent-ω-Precategory 𝒜 f g → + 2-hom-Noncoherent-ω-Precategory ℬ + ( hom-map-Noncoherent-ω-Precategory f) + ( hom-map-Noncoherent-ω-Precategory g) + 2-hom-map-Noncoherent-ω-Precategory = + 1-cell-globular-map + ( hom-globular-map-map-Noncoherent-ω-Precategory) + + hom-noncoherent-ω-precategory-map-Noncoherent-ω-Precategory : + (x y : obj-Noncoherent-ω-Precategory 𝒜) → + map-Noncoherent-ω-Precategory + ( hom-noncoherent-ω-precategory-Noncoherent-ω-Precategory + ( 𝒜) + ( x) + ( y)) + ( hom-noncoherent-ω-precategory-Noncoherent-ω-Precategory + ( ℬ) + ( obj-map-Noncoherent-ω-Precategory x) + ( obj-map-Noncoherent-ω-Precategory y)) + hom-noncoherent-ω-precategory-map-Noncoherent-ω-Precategory + x y = + 1-cell-globular-map-globular-map F +``` + +### The identity map on a noncoherent ω-precategory + +```agda +module _ + {l1 l2 : Level} (𝒜 : Noncoherent-ω-Precategory l1 l2) + where + + id-map-Noncoherent-ω-Precategory : + map-Noncoherent-ω-Precategory 𝒜 𝒜 + id-map-Noncoherent-ω-Precategory = + id-globular-map _ +``` + +### Composition of maps between noncoherent ω-precategories + +```agda +module _ + {l1 l2 l3 l4 l5 l6 : Level} + (𝒜 : Noncoherent-ω-Precategory l1 l2) + (ℬ : Noncoherent-ω-Precategory l3 l4) + (𝒞 : Noncoherent-ω-Precategory l5 l6) + (G : map-Noncoherent-ω-Precategory ℬ 𝒞) + (F : map-Noncoherent-ω-Precategory 𝒜 ℬ) + where + + comp-map-Noncoherent-ω-Precategory : + map-Noncoherent-ω-Precategory 𝒜 𝒞 + comp-map-Noncoherent-ω-Precategory = + comp-globular-map G F +``` diff --git a/src/wild-category-theory/maps-noncoherent-wild-higher-precategories.lagda.md b/src/wild-category-theory/maps-noncoherent-wild-higher-precategories.lagda.md deleted file mode 100644 index 6cb3fcbda1..0000000000 --- a/src/wild-category-theory/maps-noncoherent-wild-higher-precategories.lagda.md +++ /dev/null @@ -1,151 +0,0 @@ -# Maps between noncoherent wild higher precategories - -```agda -{-# OPTIONS --guardedness #-} - -module wild-category-theory.maps-noncoherent-wild-higher-precategories where -``` - -
Imports - -```agda -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 wild-category-theory.noncoherent-wild-higher-precategories -``` - -
- -## Idea - -A -{{#concept "map" Disambiguation="between noncoherent wild higher precategories" Agda=map-Noncoherent-Wild-Higher-Precategory}} -`f` between -[noncoherent wild higher precategories](wild-category-theory.noncoherent-wild-higher-precategories.md) -`𝒜` and `ℬ` is a [globular map](globular-types.globular-maps.md) between their -underlying [globular types](globular-types.globular-types.md). More -specifically, a map `F` between noncoherent wild higher precategories consists -of a map on objects `F₀ : obj 𝒜 → obj ℬ`, and for every pair of $n$-morphisms -`f` and `g`, a map of $(n+1)$-morphisms - -```text - Fₙ₊₁ : (𝑛+1)-hom 𝒞 f g → (𝑛+1)-hom 𝒟 (Fₙ f) (Fₙ g). -``` - -A map between noncoherent wild higher precategories does not have to preserve -the identities or composition in any shape or form, and is the least structured -notion of a "morphism" between noncoherent wild higher precategories. For a -notion of "morphism" between noncoherent wild higher precategories that in one -sense preserves this additional structure, see -[colax functors between noncoherent wild higher precategories](wild-category-theory.colax-functors-noncoherent-wild-higher-precategories.md). - -## Definitions - -### Maps between noncoherent wild higher precategories - -```agda -map-Noncoherent-Wild-Higher-Precategory : - {l1 l2 l3 l4 : Level} - (𝒜 : Noncoherent-Wild-Higher-Precategory l1 l2) - (ℬ : Noncoherent-Wild-Higher-Precategory l3 l4) → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) -map-Noncoherent-Wild-Higher-Precategory 𝒜 ℬ = - globular-map - ( globular-type-Noncoherent-Wild-Higher-Precategory 𝒜) - ( globular-type-Noncoherent-Wild-Higher-Precategory ℬ) - -module _ - {l1 l2 l3 l4 : Level} - (𝒜 : Noncoherent-Wild-Higher-Precategory l1 l2) - (ℬ : Noncoherent-Wild-Higher-Precategory l3 l4) - (F : map-Noncoherent-Wild-Higher-Precategory 𝒜 ℬ) - where - - obj-map-Noncoherent-Wild-Higher-Precategory : - obj-Noncoherent-Wild-Higher-Precategory 𝒜 → - obj-Noncoherent-Wild-Higher-Precategory ℬ - obj-map-Noncoherent-Wild-Higher-Precategory = - 0-cell-globular-map F - - hom-globular-map-map-Noncoherent-Wild-Higher-Precategory : - {x y : obj-Noncoherent-Wild-Higher-Precategory 𝒜} → - globular-map - ( hom-globular-type-Noncoherent-Wild-Higher-Precategory 𝒜 x y) - ( hom-globular-type-Noncoherent-Wild-Higher-Precategory ℬ - ( obj-map-Noncoherent-Wild-Higher-Precategory x) - ( obj-map-Noncoherent-Wild-Higher-Precategory y)) - hom-globular-map-map-Noncoherent-Wild-Higher-Precategory = - 1-cell-globular-map-globular-map F - - hom-map-Noncoherent-Wild-Higher-Precategory : - {x y : obj-Noncoherent-Wild-Higher-Precategory 𝒜} → - hom-Noncoherent-Wild-Higher-Precategory 𝒜 x y → - hom-Noncoherent-Wild-Higher-Precategory ℬ - ( obj-map-Noncoherent-Wild-Higher-Precategory x) - ( obj-map-Noncoherent-Wild-Higher-Precategory y) - hom-map-Noncoherent-Wild-Higher-Precategory = - 0-cell-globular-map - ( hom-globular-map-map-Noncoherent-Wild-Higher-Precategory) - - 2-hom-map-Noncoherent-Wild-Higher-Precategory : - {x y : obj-Noncoherent-Wild-Higher-Precategory 𝒜} - {f g : hom-Noncoherent-Wild-Higher-Precategory 𝒜 x y} → - 2-hom-Noncoherent-Wild-Higher-Precategory 𝒜 f g → - 2-hom-Noncoherent-Wild-Higher-Precategory ℬ - ( hom-map-Noncoherent-Wild-Higher-Precategory f) - ( hom-map-Noncoherent-Wild-Higher-Precategory g) - 2-hom-map-Noncoherent-Wild-Higher-Precategory = - 1-cell-globular-map - ( hom-globular-map-map-Noncoherent-Wild-Higher-Precategory) - - hom-noncoherent-wild-higher-precategory-map-Noncoherent-Wild-Higher-Precategory : - (x y : obj-Noncoherent-Wild-Higher-Precategory 𝒜) → - map-Noncoherent-Wild-Higher-Precategory - ( hom-noncoherent-wild-higher-precategory-Noncoherent-Wild-Higher-Precategory - ( 𝒜) - ( x) - ( y)) - ( hom-noncoherent-wild-higher-precategory-Noncoherent-Wild-Higher-Precategory - ( ℬ) - ( obj-map-Noncoherent-Wild-Higher-Precategory x) - ( obj-map-Noncoherent-Wild-Higher-Precategory y)) - hom-noncoherent-wild-higher-precategory-map-Noncoherent-Wild-Higher-Precategory - x y = - 1-cell-globular-map-globular-map F -``` - -### The identity map on a noncoherent wild higher precategory - -```agda -module _ - {l1 l2 : Level} (𝒜 : Noncoherent-Wild-Higher-Precategory l1 l2) - where - - id-map-Noncoherent-Wild-Higher-Precategory : - map-Noncoherent-Wild-Higher-Precategory 𝒜 𝒜 - id-map-Noncoherent-Wild-Higher-Precategory = - id-globular-map _ -``` - -### Composition of maps between noncoherent wild higher precategories - -```agda -module _ - {l1 l2 l3 l4 l5 l6 : Level} - (𝒜 : Noncoherent-Wild-Higher-Precategory l1 l2) - (ℬ : Noncoherent-Wild-Higher-Precategory l3 l4) - (𝒞 : Noncoherent-Wild-Higher-Precategory l5 l6) - (G : map-Noncoherent-Wild-Higher-Precategory ℬ 𝒞) - (F : map-Noncoherent-Wild-Higher-Precategory 𝒜 ℬ) - where - - comp-map-Noncoherent-Wild-Higher-Precategory : - map-Noncoherent-Wild-Higher-Precategory 𝒜 𝒞 - comp-map-Noncoherent-Wild-Higher-Precategory = - comp-globular-map G F -``` diff --git a/src/wild-category-theory/noncoherent-large-omega-precategories.lagda.md b/src/wild-category-theory/noncoherent-large-omega-precategories.lagda.md new file mode 100644 index 0000000000..d40fa26fd8 --- /dev/null +++ b/src/wild-category-theory/noncoherent-large-omega-precategories.lagda.md @@ -0,0 +1,362 @@ +# Noncoherent large ω-precategories + +```agda +{-# OPTIONS --guardedness #-} + +module wild-category-theory.noncoherent-large-omega-precategories where +``` + +
Imports + +```agda +open import category-theory.precategories + +open import foundation.action-on-identifications-binary-functions +open import foundation.dependent-pair-types +open import foundation.function-types +open import foundation.homotopies +open import foundation.identity-types +open import foundation.sets +open import foundation.strictly-involutive-identity-types +open import foundation.universe-levels + +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.noncoherent-omega-precategories +``` + +
+ +## Idea + +It is an important open problem known as the _coherence problem_ to define a +fully coherent notion of $∞$-category or higher variants in univalent type +theory. The subject of _wild category theory_ attempts to recover some of the +benefits of $∞$-category theory without tackling this problem. We introduce, as +one of our basic building blocks in this subject, the notion of a _noncoherent +large ω-precategory_. + +A _noncoherent large ω-precategory_ `𝒞` is a structure that attempts at +capturing the structure of a large ω-category to the $0$'th order. It consists +of in some sense all of the operations and none of the coherence. Thus, it is +defined as a [large globular type](globular-types.large-globular-types.md) with +families of $n$-morphisms labeled as "identities" + +```text + id-hom : (x : 𝒞ₙ) → 𝒞ₙ₊₁ x x +``` + +and a composition operation at every dimension + +```text + comp-hom : {x y z : 𝒞ₙ} → 𝒞ₙ₊₁ y z → 𝒞ₙ₊₁ x y → 𝒞ₙ₊₁ x z. +``` + +Entirely concretely, we define a +{{#concept "noncoherent large ω-precategory" Agda=Noncoherent-Large-ω-Precategory}} +to be a [reflexive](globular-types.reflexive-globular-types.md) and +[transitive](globular-types.transitive-globular-types.md) large globular type. +We call the 0-cells the _objects_, the 1-cells the _morphisms_ and the higher +cells the _$n$-morphisms_. The reflexivities are called the _identity +morphisms_, and the transitivity operations are branded as _composition of +morphisms_. + +## Definitions + +### Noncoherent large ω-precategories + +```agda +record + Noncoherent-Large-ω-Precategory + (α : Level → Level) (β : Level → Level → Level) : UUω + where +``` + +The underlying large globular type of a noncoherent large wild precategory: + +```agda + field + large-globular-type-Noncoherent-Large-ω-Precategory : + Large-Globular-Type α β +``` + +The type of objects of a noncoherent large ω-precategory: + +```agda + obj-Noncoherent-Large-ω-Precategory : (l : Level) → UU (α l) + obj-Noncoherent-Large-ω-Precategory = + 0-cell-Large-Globular-Type + large-globular-type-Noncoherent-Large-ω-Precategory +``` + +The globular type of morphisms between two objects in a noncoherent large +ω-precategory: + +```agda + hom-globular-type-Noncoherent-Large-ω-Precategory : + {l1 l2 : Level} + (x : obj-Noncoherent-Large-ω-Precategory l1) + (y : obj-Noncoherent-Large-ω-Precategory l2) → + Globular-Type (β l1 l2) (β l1 l2) + hom-globular-type-Noncoherent-Large-ω-Precategory = + 1-cell-globular-type-Large-Globular-Type + large-globular-type-Noncoherent-Large-ω-Precategory + + hom-Noncoherent-Large-ω-Precategory : + {l1 l2 : Level} + (x : obj-Noncoherent-Large-ω-Precategory l1) + (y : obj-Noncoherent-Large-ω-Precategory l2) → + UU (β l1 l2) + hom-Noncoherent-Large-ω-Precategory = + 1-cell-Large-Globular-Type + large-globular-type-Noncoherent-Large-ω-Precategory +``` + +The globular structure on the type of objects of a noncoherent large +ω-precategory: + +```agda + globular-structure-obj-Noncoherent-Large-ω-Precategory : + large-globular-structure β obj-Noncoherent-Large-ω-Precategory + globular-structure-obj-Noncoherent-Large-ω-Precategory = + large-globular-structure-0-cell-Large-Globular-Type + large-globular-type-Noncoherent-Large-ω-Precategory +``` + +The globular type of 2-morphisms is a noncoherent large ω-precategory: + +```agda + 2-hom-globular-type-Noncoherent-Large-ω-Precategory : + {l1 l2 : Level} + {x : obj-Noncoherent-Large-ω-Precategory l1} + {y : obj-Noncoherent-Large-ω-Precategory l2} + (f g : hom-Noncoherent-Large-ω-Precategory x y) → + Globular-Type (β l1 l2) (β l1 l2) + 2-hom-globular-type-Noncoherent-Large-ω-Precategory = + 2-cell-globular-type-Large-Globular-Type + large-globular-type-Noncoherent-Large-ω-Precategory + + 2-hom-Noncoherent-Large-ω-Precategory : + {l1 l2 : Level} + {x : obj-Noncoherent-Large-ω-Precategory l1} + {y : obj-Noncoherent-Large-ω-Precategory l2} → + (f g : hom-Noncoherent-Large-ω-Precategory x y) → UU (β l1 l2) + 2-hom-Noncoherent-Large-ω-Precategory = + 2-cell-Large-Globular-Type + large-globular-type-Noncoherent-Large-ω-Precategory +``` + +The globular structure on the type of morphisms between two objects in a +noncoherent large ω-precategory: + +```agda + globular-structure-hom-Noncoherent-Large-ω-Precategory : + {l1 l2 : Level} + (x : obj-Noncoherent-Large-ω-Precategory l1) + (y : obj-Noncoherent-Large-ω-Precategory l2) → + globular-structure + ( β l1 l2) + ( hom-Noncoherent-Large-ω-Precategory x y) + globular-structure-hom-Noncoherent-Large-ω-Precategory = + globular-structure-1-cell-Large-Globular-Type + large-globular-type-Noncoherent-Large-ω-Precategory +``` + +The globular type of 3-morphisms in a noncoherent large ω-precategory: + +```agda + 3-hom-globular-type-Noncoherent-Large-ω-Precategory : + {l1 l2 : Level} + {x : obj-Noncoherent-Large-ω-Precategory l1} + {y : obj-Noncoherent-Large-ω-Precategory l2} + {f g : hom-Noncoherent-Large-ω-Precategory x y} + (s t : 2-hom-Noncoherent-Large-ω-Precategory f g) → + Globular-Type (β l1 l2) (β l1 l2) + 3-hom-globular-type-Noncoherent-Large-ω-Precategory = + 3-cell-globular-type-Large-Globular-Type + large-globular-type-Noncoherent-Large-ω-Precategory + + 3-hom-Noncoherent-Large-ω-Precategory : + {l1 l2 : Level} + {x : obj-Noncoherent-Large-ω-Precategory l1} + {y : obj-Noncoherent-Large-ω-Precategory l2} + {f g : hom-Noncoherent-Large-ω-Precategory x y} → + 2-hom-Noncoherent-Large-ω-Precategory f g → + 2-hom-Noncoherent-Large-ω-Precategory f g → + UU (β l1 l2) + 3-hom-Noncoherent-Large-ω-Precategory = + 3-cell-Large-Globular-Type + large-globular-type-Noncoherent-Large-ω-Precategory +``` + +The globular structure on the type of 2-morphisms in a noncoherent large +ω-precategory: + +```agda + globular-structure-2-hom-Noncoherent-Large-ω-Precategory : + {l1 l2 : Level} + {x : obj-Noncoherent-Large-ω-Precategory l1} + {y : obj-Noncoherent-Large-ω-Precategory l2} + (f g : hom-Noncoherent-Large-ω-Precategory x y) → + globular-structure + ( β l1 l2) + ( 2-hom-Noncoherent-Large-ω-Precategory f g) + globular-structure-2-hom-Noncoherent-Large-ω-Precategory = + globular-structure-2-cell-Large-Globular-Type + large-globular-type-Noncoherent-Large-ω-Precategory +``` + +The structure of identity morphisms in a noncoherent large ω-precategory: + +```agda + field + id-structure-Noncoherent-Large-ω-Precategory : + is-reflexive-Large-Globular-Type + large-globular-type-Noncoherent-Large-ω-Precategory + + id-hom-Noncoherent-Large-ω-Precategory : + {l1 : Level} {x : obj-Noncoherent-Large-ω-Precategory l1} → + hom-Noncoherent-Large-ω-Precategory x x + id-hom-Noncoherent-Large-ω-Precategory {l1} {x} = + refl-1-cell-is-reflexive-Large-Globular-Type + ( id-structure-Noncoherent-Large-ω-Precategory) + ( x) + + id-structure-hom-globular-type-Noncoherent-Large-ω-Precategory : + {l1 l2 : Level} + {x : obj-Noncoherent-Large-ω-Precategory l1} + {y : obj-Noncoherent-Large-ω-Precategory l2} → + is-reflexive-Globular-Type + ( hom-globular-type-Noncoherent-Large-ω-Precategory x y) + id-structure-hom-globular-type-Noncoherent-Large-ω-Precategory = + is-reflexive-1-cell-globular-type-is-reflexive-Large-Globular-Type + id-structure-Noncoherent-Large-ω-Precategory + + id-2-hom-Noncoherent-Large-ω-Precategory : + {l1 l2 : Level} + {x : obj-Noncoherent-Large-ω-Precategory l1} + {y : obj-Noncoherent-Large-ω-Precategory l2} + (f : hom-Noncoherent-Large-ω-Precategory x y) → + 2-hom-Noncoherent-Large-ω-Precategory f f + id-2-hom-Noncoherent-Large-ω-Precategory = + refl-2-cell-is-reflexive-Large-Globular-Type + id-structure-Noncoherent-Large-ω-Precategory + + id-3-hom-Noncoherent-Large-ω-Precategory : + {l1 l2 : Level} + {x : obj-Noncoherent-Large-ω-Precategory l1} + {y : obj-Noncoherent-Large-ω-Precategory l2} + {f g : hom-Noncoherent-Large-ω-Precategory x y} + (s : 2-hom-Noncoherent-Large-ω-Precategory f g) → + 3-hom-Noncoherent-Large-ω-Precategory s s + id-3-hom-Noncoherent-Large-ω-Precategory = + refl-3-cell-is-reflexive-Large-Globular-Type + id-structure-Noncoherent-Large-ω-Precategory +``` + +The structure of composition in a noncoherent large ω-precategory: + +```agda + field + comp-structure-Noncoherent-Large-ω-Precategory : + is-transitive-Large-Globular-Type + large-globular-type-Noncoherent-Large-ω-Precategory + + comp-hom-Noncoherent-Large-ω-Precategory : + {l1 l2 l3 : Level} + {x : obj-Noncoherent-Large-ω-Precategory l1} + {y : obj-Noncoherent-Large-ω-Precategory l2} + {z : obj-Noncoherent-Large-ω-Precategory l3} → + hom-Noncoherent-Large-ω-Precategory y z → + hom-Noncoherent-Large-ω-Precategory x y → + hom-Noncoherent-Large-ω-Precategory x z + comp-hom-Noncoherent-Large-ω-Precategory = + comp-1-cell-is-transitive-Large-Globular-Type + comp-structure-Noncoherent-Large-ω-Precategory + + comp-structure-hom-globular-type-Noncoherent-Large-ω-Precategory : + {l1 l2 : Level} + {x : obj-Noncoherent-Large-ω-Precategory l1} + {y : obj-Noncoherent-Large-ω-Precategory l2} → + is-transitive-Globular-Type + ( hom-globular-type-Noncoherent-Large-ω-Precategory x y) + comp-structure-hom-globular-type-Noncoherent-Large-ω-Precategory = + is-transitive-1-cell-globular-type-is-transitive-Large-Globular-Type + comp-structure-Noncoherent-Large-ω-Precategory + + comp-2-hom-Noncoherent-Large-ω-Precategory : + {l1 l2 : Level} + {x : obj-Noncoherent-Large-ω-Precategory l1} + {y : obj-Noncoherent-Large-ω-Precategory l2} + {f g h : hom-Noncoherent-Large-ω-Precategory x y} → + 2-hom-Noncoherent-Large-ω-Precategory g h → + 2-hom-Noncoherent-Large-ω-Precategory f g → + 2-hom-Noncoherent-Large-ω-Precategory f h + comp-2-hom-Noncoherent-Large-ω-Precategory = + comp-2-cell-is-transitive-Large-Globular-Type + comp-structure-Noncoherent-Large-ω-Precategory + + comp-3-hom-Noncoherent-Large-ω-Precategory : + {l1 l2 : Level} + {x : obj-Noncoherent-Large-ω-Precategory l1} + {y : obj-Noncoherent-Large-ω-Precategory l2} + {f g : hom-Noncoherent-Large-ω-Precategory x y} + {r s t : 2-hom-Noncoherent-Large-ω-Precategory f g} → + 3-hom-Noncoherent-Large-ω-Precategory s t → + 3-hom-Noncoherent-Large-ω-Precategory r s → + 3-hom-Noncoherent-Large-ω-Precategory r t + comp-3-hom-Noncoherent-Large-ω-Precategory = + comp-3-cell-is-transitive-Large-Globular-Type + comp-structure-Noncoherent-Large-ω-Precategory +``` + +The noncoherent ω-precategory of morphisms between two object in a noncoherent +large ω-precategory: + +```agda + hom-noncoherent-ω-precategory-Noncoherent-Large-ω-Precategory : + {l1 l2 : Level} + (x : obj-Noncoherent-Large-ω-Precategory l1) + (y : obj-Noncoherent-Large-ω-Precategory l2) → + Noncoherent-ω-Precategory (β l1 l2) (β l1 l2) + hom-noncoherent-ω-precategory-Noncoherent-Large-ω-Precategory + x y = + make-Noncoherent-ω-Precategory + ( id-structure-hom-globular-type-Noncoherent-Large-ω-Precategory + { x = x} + { y}) + ( comp-structure-hom-globular-type-Noncoherent-Large-ω-Precategory) +``` + +The underlying reflexive globular type of a noncoherent large ω-precategory: + +```agda + large-reflexive-globular-type-Noncoherent-Large-ω-Precategory : + Large-Reflexive-Globular-Type α β + large-globular-type-Large-Reflexive-Globular-Type + large-reflexive-globular-type-Noncoherent-Large-ω-Precategory = + large-globular-type-Noncoherent-Large-ω-Precategory + is-reflexive-Large-Reflexive-Globular-Type + large-reflexive-globular-type-Noncoherent-Large-ω-Precategory = + id-structure-Noncoherent-Large-ω-Precategory +``` + +The underlying transitive globular type of a noncoherent large ω-precategory: + +```agda + large-transitive-globular-type-Noncoherent-Large-ω-Precategory : + Large-Transitive-Globular-Type α β + large-globular-type-Large-Transitive-Globular-Type + large-transitive-globular-type-Noncoherent-Large-ω-Precategory = + large-globular-type-Noncoherent-Large-ω-Precategory + is-transitive-Large-Transitive-Globular-Type + large-transitive-globular-type-Noncoherent-Large-ω-Precategory = + comp-structure-Noncoherent-Large-ω-Precategory + +open Noncoherent-Large-ω-Precategory public +``` diff --git a/src/wild-category-theory/noncoherent-large-wild-higher-precategories.lagda.md b/src/wild-category-theory/noncoherent-large-wild-higher-precategories.lagda.md deleted file mode 100644 index d5b568a950..0000000000 --- a/src/wild-category-theory/noncoherent-large-wild-higher-precategories.lagda.md +++ /dev/null @@ -1,367 +0,0 @@ -# Noncoherent large wild higher precategories - -```agda -{-# OPTIONS --guardedness #-} - -module wild-category-theory.noncoherent-large-wild-higher-precategories where -``` - -
Imports - -```agda -open import category-theory.precategories - -open import foundation.action-on-identifications-binary-functions -open import foundation.dependent-pair-types -open import foundation.function-types -open import foundation.homotopies -open import foundation.identity-types -open import foundation.sets -open import foundation.strictly-involutive-identity-types -open import foundation.universe-levels - -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.noncoherent-wild-higher-precategories -``` - -
- -## Idea - -It is an important open problem known as the _coherence problem_ to define a -fully coherent notion of $∞$-category in univalent type theory. The subject of -_wild category theory_ attempts to recover some of the benefits of $∞$-category -theory without tackling this problem. We introduce, as one of our basic building -blocks in this subject, the notion of a _large noncoherent wild higher -precategory_. - -A _large noncoherent wild higher precategory_ `𝒞` is a structure that attempts -at capturing the structure of a large higher precategory to the $0$'th order. It -consists of in some sense all of the operations and none of the coherence of a -large higher precategory. Thus, it is defined as a -[large globular type](globular-types.large-globular-types.md) with families of -$n$-morphisms labeled as "identities" - -```text - id-hom : (x : 𝑛-Cell 𝒞) → (𝑛+1)-Cell 𝒞 x x -``` - -and a composition operation at every dimension - -```text - comp-hom : - {x y z : 𝑛-Cell 𝒞} → (𝑛+1)-Cell 𝒞 y z → (𝑛+1)-Cell 𝒞 x y → (𝑛+1)-Cell 𝒞 x z. -``` - -Entirely concretely, we define a -{{#concept "noncoherent large wild higher precategory" Agda=Noncoherent-Large-Wild-Higher-Precategory}} -to be a [reflexive](globular-types.reflexive-globular-types.md) and -[transitive](globular-types.transitive-globular-types.md) large globular type. -We call the 0-cells the _objects_, the 1-cells the _morphisms_ and the higher -cells the _$n$-morphisms_. The reflexivities are called the _identity -morphisms_, and the transitivity operations are branded as _composition of -morphisms_. - -## Definitions - -### Noncoherent large wild higher precategories - -```agda -record - Noncoherent-Large-Wild-Higher-Precategory - (α : Level → Level) (β : Level → Level → Level) : UUω - where -``` - -The underlying large globular type of a noncoherent large wild precategory: - -```agda - field - large-globular-type-Noncoherent-Large-Wild-Higher-Precategory : - Large-Globular-Type α β -``` - -The type of objects of a noncoherent large wild higher precategory: - -```agda - obj-Noncoherent-Large-Wild-Higher-Precategory : (l : Level) → UU (α l) - obj-Noncoherent-Large-Wild-Higher-Precategory = - 0-cell-Large-Globular-Type - large-globular-type-Noncoherent-Large-Wild-Higher-Precategory -``` - -The globular type of morphisms between two objects in a noncoherent large wild -higher precategory: - -```agda - hom-globular-type-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-Type (β l1 l2) (β l1 l2) - hom-globular-type-Noncoherent-Large-Wild-Higher-Precategory = - 1-cell-globular-type-Large-Globular-Type - large-globular-type-Noncoherent-Large-Wild-Higher-Precategory - - hom-Noncoherent-Large-Wild-Higher-Precategory : - {l1 l2 : Level} - (x : obj-Noncoherent-Large-Wild-Higher-Precategory l1) - (y : obj-Noncoherent-Large-Wild-Higher-Precategory l2) → - UU (β l1 l2) - hom-Noncoherent-Large-Wild-Higher-Precategory = - 1-cell-Large-Globular-Type - large-globular-type-Noncoherent-Large-Wild-Higher-Precategory -``` - -The globular structure on the type of objects of a noncoherent large wild higher -precategory: - -```agda - globular-structure-obj-Noncoherent-Large-Wild-Higher-Precategory : - large-globular-structure β obj-Noncoherent-Large-Wild-Higher-Precategory - globular-structure-obj-Noncoherent-Large-Wild-Higher-Precategory = - large-globular-structure-0-cell-Large-Globular-Type - large-globular-type-Noncoherent-Large-Wild-Higher-Precategory -``` - -The globular type of 2-morphisms is a noncoherent large wild higher precategory: - -```agda - 2-hom-globular-type-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) → - Globular-Type (β l1 l2) (β l1 l2) - 2-hom-globular-type-Noncoherent-Large-Wild-Higher-Precategory = - 2-cell-globular-type-Large-Globular-Type - large-globular-type-Noncoherent-Large-Wild-Higher-Precategory - - 2-hom-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) → UU (β l1 l2) - 2-hom-Noncoherent-Large-Wild-Higher-Precategory = - 2-cell-Large-Globular-Type - large-globular-type-Noncoherent-Large-Wild-Higher-Precategory -``` - -The globular structure on the type of morphisms between two objects in a -noncoherent large wild higher precategory: - -```agda - globular-structure-hom-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-structure - ( β l1 l2) - ( hom-Noncoherent-Large-Wild-Higher-Precategory x y) - globular-structure-hom-Noncoherent-Large-Wild-Higher-Precategory = - globular-structure-1-cell-Large-Globular-Type - large-globular-type-Noncoherent-Large-Wild-Higher-Precategory -``` - -The globular type of 3-morphisms in a noncoherent large wild higher precategory: - -```agda - 3-hom-globular-type-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} - (s t : 2-hom-Noncoherent-Large-Wild-Higher-Precategory f g) → - Globular-Type (β l1 l2) (β l1 l2) - 3-hom-globular-type-Noncoherent-Large-Wild-Higher-Precategory = - 3-cell-globular-type-Large-Globular-Type - large-globular-type-Noncoherent-Large-Wild-Higher-Precategory - - 3-hom-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 f g → - UU (β l1 l2) - 3-hom-Noncoherent-Large-Wild-Higher-Precategory = - 3-cell-Large-Globular-Type - large-globular-type-Noncoherent-Large-Wild-Higher-Precategory -``` - -The globular structure on the type of 2-morphisms in a noncoherent large wild -higher precategory: - -```agda - globular-structure-2-hom-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) → - globular-structure - ( β l1 l2) - ( 2-hom-Noncoherent-Large-Wild-Higher-Precategory f g) - globular-structure-2-hom-Noncoherent-Large-Wild-Higher-Precategory = - globular-structure-2-cell-Large-Globular-Type - large-globular-type-Noncoherent-Large-Wild-Higher-Precategory -``` - -The structure of identity morphisms in a noncoherent large wild higher -precategory: - -```agda - field - id-structure-Noncoherent-Large-Wild-Higher-Precategory : - is-reflexive-Large-Globular-Type - large-globular-type-Noncoherent-Large-Wild-Higher-Precategory - - id-hom-Noncoherent-Large-Wild-Higher-Precategory : - {l1 : Level} {x : obj-Noncoherent-Large-Wild-Higher-Precategory l1} → - hom-Noncoherent-Large-Wild-Higher-Precategory x x - id-hom-Noncoherent-Large-Wild-Higher-Precategory {l1} {x} = - refl-1-cell-is-reflexive-Large-Globular-Type - ( id-structure-Noncoherent-Large-Wild-Higher-Precategory) - ( x) - - id-structure-hom-globular-type-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-reflexive-Globular-Type - ( hom-globular-type-Noncoherent-Large-Wild-Higher-Precategory x y) - id-structure-hom-globular-type-Noncoherent-Large-Wild-Higher-Precategory = - is-reflexive-1-cell-globular-type-is-reflexive-Large-Globular-Type - id-structure-Noncoherent-Large-Wild-Higher-Precategory - - id-2-hom-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 : hom-Noncoherent-Large-Wild-Higher-Precategory x y) → - 2-hom-Noncoherent-Large-Wild-Higher-Precategory f f - id-2-hom-Noncoherent-Large-Wild-Higher-Precategory = - refl-2-cell-is-reflexive-Large-Globular-Type - id-structure-Noncoherent-Large-Wild-Higher-Precategory - - id-3-hom-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} - (s : 2-hom-Noncoherent-Large-Wild-Higher-Precategory f g) → - 3-hom-Noncoherent-Large-Wild-Higher-Precategory s s - id-3-hom-Noncoherent-Large-Wild-Higher-Precategory = - refl-3-cell-is-reflexive-Large-Globular-Type - id-structure-Noncoherent-Large-Wild-Higher-Precategory -``` - -The structure of composition in a noncoherent large wild higher precategory: - -```agda - field - comp-structure-Noncoherent-Large-Wild-Higher-Precategory : - is-transitive-Large-Globular-Type - large-globular-type-Noncoherent-Large-Wild-Higher-Precategory - - comp-hom-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} → - hom-Noncoherent-Large-Wild-Higher-Precategory y z → - hom-Noncoherent-Large-Wild-Higher-Precategory x y → - hom-Noncoherent-Large-Wild-Higher-Precategory x z - comp-hom-Noncoherent-Large-Wild-Higher-Precategory = - comp-1-cell-is-transitive-Large-Globular-Type - comp-structure-Noncoherent-Large-Wild-Higher-Precategory - - comp-structure-hom-globular-type-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-transitive-Globular-Type - ( hom-globular-type-Noncoherent-Large-Wild-Higher-Precategory x y) - comp-structure-hom-globular-type-Noncoherent-Large-Wild-Higher-Precategory = - is-transitive-1-cell-globular-type-is-transitive-Large-Globular-Type - comp-structure-Noncoherent-Large-Wild-Higher-Precategory - - comp-2-hom-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 h : hom-Noncoherent-Large-Wild-Higher-Precategory x y} → - 2-hom-Noncoherent-Large-Wild-Higher-Precategory g h → - 2-hom-Noncoherent-Large-Wild-Higher-Precategory f g → - 2-hom-Noncoherent-Large-Wild-Higher-Precategory f h - comp-2-hom-Noncoherent-Large-Wild-Higher-Precategory = - comp-2-cell-is-transitive-Large-Globular-Type - comp-structure-Noncoherent-Large-Wild-Higher-Precategory - - comp-3-hom-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} - {r s t : 2-hom-Noncoherent-Large-Wild-Higher-Precategory f g} → - 3-hom-Noncoherent-Large-Wild-Higher-Precategory s t → - 3-hom-Noncoherent-Large-Wild-Higher-Precategory r s → - 3-hom-Noncoherent-Large-Wild-Higher-Precategory r t - comp-3-hom-Noncoherent-Large-Wild-Higher-Precategory = - comp-3-cell-is-transitive-Large-Globular-Type - comp-structure-Noncoherent-Large-Wild-Higher-Precategory -``` - -The noncoherent wild higher precategory of morphisms between two object in a -noncoherent large wild higher precategory: - -```agda - hom-noncoherent-wild-higher-precategory-Noncoherent-Large-Wild-Higher-Precategory : - {l1 l2 : Level} - (x : obj-Noncoherent-Large-Wild-Higher-Precategory l1) - (y : obj-Noncoherent-Large-Wild-Higher-Precategory l2) → - Noncoherent-Wild-Higher-Precategory (β l1 l2) (β l1 l2) - hom-noncoherent-wild-higher-precategory-Noncoherent-Large-Wild-Higher-Precategory - x y = - make-Noncoherent-Wild-Higher-Precategory - ( id-structure-hom-globular-type-Noncoherent-Large-Wild-Higher-Precategory - { x = x} - { y}) - ( comp-structure-hom-globular-type-Noncoherent-Large-Wild-Higher-Precategory) -``` - -The underlying reflexive globular type of a noncoherent large wild higher -precategory: - -```agda - large-reflexive-globular-type-Noncoherent-Large-Wild-Higher-Precategory : - Large-Reflexive-Globular-Type α β - large-globular-type-Large-Reflexive-Globular-Type - large-reflexive-globular-type-Noncoherent-Large-Wild-Higher-Precategory = - large-globular-type-Noncoherent-Large-Wild-Higher-Precategory - is-reflexive-Large-Reflexive-Globular-Type - large-reflexive-globular-type-Noncoherent-Large-Wild-Higher-Precategory = - id-structure-Noncoherent-Large-Wild-Higher-Precategory -``` - -The underlying transitive globular type of a noncoherent large wild higher -precategory: - -```agda - large-transitive-globular-type-Noncoherent-Large-Wild-Higher-Precategory : - Large-Transitive-Globular-Type α β - large-globular-type-Large-Transitive-Globular-Type - large-transitive-globular-type-Noncoherent-Large-Wild-Higher-Precategory = - large-globular-type-Noncoherent-Large-Wild-Higher-Precategory - is-transitive-Large-Transitive-Globular-Type - large-transitive-globular-type-Noncoherent-Large-Wild-Higher-Precategory = - comp-structure-Noncoherent-Large-Wild-Higher-Precategory - -open Noncoherent-Large-Wild-Higher-Precategory public -``` diff --git a/src/wild-category-theory/noncoherent-omega-precategories.lagda.md b/src/wild-category-theory/noncoherent-omega-precategories.lagda.md new file mode 100644 index 0000000000..648d1f464f --- /dev/null +++ b/src/wild-category-theory/noncoherent-omega-precategories.lagda.md @@ -0,0 +1,275 @@ +# Noncoherent ω-precategories + +```agda +{-# OPTIONS --guardedness #-} + +module wild-category-theory.noncoherent-omega-precategories where +``` + +
Imports + +```agda +open import category-theory.precategories + +open import foundation.action-on-identifications-binary-functions +open import foundation.cartesian-product-types +open import foundation.dependent-pair-types +open import foundation.function-types +open import foundation.homotopies +open import foundation.identity-types +open import foundation.sets +open import foundation.strictly-involutive-identity-types +open import foundation.universe-levels + +open import globular-types.globular-types +open import globular-types.reflexive-globular-types +open import globular-types.transitive-globular-types +``` + +
+ +## Idea + +It is an important open problem known as the _coherence problem_ to define a +fully coherent notion of $∞$-category or higher variants in univalent type +theory. The subject of _wild category theory_ attempts to recover some of the +benefits of $∞$-category theory without tackling this problem. We introduce, as +one of our basic building blocks in this subject, the notion of a _noncoherent +ω-precategory_. + +A _noncoherent ω-precategory_ `𝒞` is a structure that attempts at capturing the +structure of an ω-category to the $0$'th order. It consists of in some sense all +of the operations and none of the coherence. Thus, it is defined as a +[globular type](globular-types.globular-types.md) with families of $n$-morphisms +labeled as "identities" + +```text + id-hom : (x : 𝒞ₙ) → 𝒞ₙ₊₁ x x +``` + +and a composition operation at every dimension + +```text + comp-hom : {x y z : 𝒞ₙ} → 𝒞ₙ₊₁ y z → 𝒞ₙ₊₁ x y → 𝒞ₙ₊₁ x z. +``` + +Entirely concretely, we define a +{{#concept "noncoherent ω-precategory" Agda=Noncoherent-ω-Precategory}} to be a +[reflexive](globular-types.reflexive-globular-types.md) and +[transitive](globular-types.transitive-globular-types.md) globular type. We call +the 0-cells the _objects_, the 1-cells the _morphisms_ and the higher cells the +_$n$-morphisms_. The reflexivities are called the _identity morphisms_, and the +transitivity operations are branded as _composition of morphisms_. + +## Definitions + +### Noncoherent ω-precategories + +```agda +Noncoherent-ω-Precategory : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2) +Noncoherent-ω-Precategory l1 l2 = + Σ ( Globular-Type l1 l2) + ( λ X → is-reflexive-Globular-Type X × is-transitive-Globular-Type X) + +make-Noncoherent-ω-Precategory : + {l1 l2 : Level} {X : Globular-Type l1 l2} → is-reflexive-Globular-Type X → + is-transitive-Globular-Type X → Noncoherent-ω-Precategory l1 l2 +make-Noncoherent-ω-Precategory id comp = + ( _ , id , comp) + +{-# INLINE make-Noncoherent-ω-Precategory #-} + +module _ + {l1 l2 : Level} (𝒞 : Noncoherent-ω-Precategory l1 l2) + where + + globular-type-Noncoherent-ω-Precategory : Globular-Type l1 l2 + globular-type-Noncoherent-ω-Precategory = pr1 𝒞 + + obj-Noncoherent-ω-Precategory : UU l1 + obj-Noncoherent-ω-Precategory = + 0-cell-Globular-Type globular-type-Noncoherent-ω-Precategory +``` + +Morphisms in a noncoherent ω-precategory: + +```agda + hom-globular-type-Noncoherent-ω-Precategory : + (x y : obj-Noncoherent-ω-Precategory) → + Globular-Type l2 l2 + hom-globular-type-Noncoherent-ω-Precategory = + 1-cell-globular-type-Globular-Type + globular-type-Noncoherent-ω-Precategory + + hom-Noncoherent-ω-Precategory : + obj-Noncoherent-ω-Precategory → + obj-Noncoherent-ω-Precategory → + UU l2 + hom-Noncoherent-ω-Precategory = + 1-cell-Globular-Type globular-type-Noncoherent-ω-Precategory +``` + +Identity morphisms in a noncoherent ω-precategory: + +```agda + id-structure-Noncoherent-ω-Precategory : + is-reflexive-Globular-Type globular-type-Noncoherent-ω-Precategory + id-structure-Noncoherent-ω-Precategory = + pr1 (pr2 𝒞) + + id-hom-Noncoherent-ω-Precategory : + {x : obj-Noncoherent-ω-Precategory} → + hom-Noncoherent-ω-Precategory x x + id-hom-Noncoherent-ω-Precategory {x} = + refl-2-cell-is-reflexive-Globular-Type + id-structure-Noncoherent-ω-Precategory + + id-structure-hom-globular-type-Noncoherent-ω-Precategory : + {x y : obj-Noncoherent-ω-Precategory} → + is-reflexive-Globular-Type + ( hom-globular-type-Noncoherent-ω-Precategory x y) + id-structure-hom-globular-type-Noncoherent-ω-Precategory = + is-reflexive-1-cell-globular-type-is-reflexive-Globular-Type + id-structure-Noncoherent-ω-Precategory + + reflexive-globular-type-Noncoherent-ω-Precategory : + Reflexive-Globular-Type l1 l2 + globular-type-Reflexive-Globular-Type + reflexive-globular-type-Noncoherent-ω-Precategory = + globular-type-Noncoherent-ω-Precategory + refl-Reflexive-Globular-Type + reflexive-globular-type-Noncoherent-ω-Precategory = + id-structure-Noncoherent-ω-Precategory + + hom-reflexive-globular-type-Noncoherent-ω-Precategory : + (x y : obj-Noncoherent-ω-Precategory) → + Reflexive-Globular-Type l2 l2 + hom-reflexive-globular-type-Noncoherent-ω-Precategory x y = + 1-cell-reflexive-globular-type-Reflexive-Globular-Type + ( reflexive-globular-type-Noncoherent-ω-Precategory) + ( x) + ( y) +``` + +Composition in a noncoherent ω-precategory: + +```agda + comp-structure-Noncoherent-ω-Precategory : + is-transitive-Globular-Type + globular-type-Noncoherent-ω-Precategory + comp-structure-Noncoherent-ω-Precategory = + pr2 (pr2 𝒞) + + comp-hom-Noncoherent-ω-Precategory : + {x y z : obj-Noncoherent-ω-Precategory} → + hom-Noncoherent-ω-Precategory y z → + hom-Noncoherent-ω-Precategory x y → + hom-Noncoherent-ω-Precategory x z + comp-hom-Noncoherent-ω-Precategory = + comp-1-cell-is-transitive-Globular-Type + comp-structure-Noncoherent-ω-Precategory + + comp-structure-hom-globular-type-Noncoherent-ω-Precategory : + {x y : obj-Noncoherent-ω-Precategory} → + is-transitive-Globular-Type + ( hom-globular-type-Noncoherent-ω-Precategory x y) + comp-structure-hom-globular-type-Noncoherent-ω-Precategory = + is-transitive-1-cell-globular-type-is-transitive-Globular-Type + comp-structure-Noncoherent-ω-Precategory + + transitive-globular-type-Noncoherent-ω-Precategory : + Transitive-Globular-Type l1 l2 + globular-type-Transitive-Globular-Type + transitive-globular-type-Noncoherent-ω-Precategory = + globular-type-Noncoherent-ω-Precategory + is-transitive-Transitive-Globular-Type + transitive-globular-type-Noncoherent-ω-Precategory = + comp-structure-Noncoherent-ω-Precategory + + hom-transitive-globular-type-Noncoherent-ω-Precategory : + (x y : obj-Noncoherent-ω-Precategory) → + Transitive-Globular-Type l2 l2 + hom-transitive-globular-type-Noncoherent-ω-Precategory x y = + 1-cell-transitive-globular-type-Transitive-Globular-Type + ( transitive-globular-type-Noncoherent-ω-Precategory) + ( x) + ( y) +``` + +The noncoherent ω-precategory of morphisms between two objects in a noncoherent +ω-precategory: + +```agda + hom-noncoherent-ω-precategory-Noncoherent-ω-Precategory : + (x y : obj-Noncoherent-ω-Precategory) → + Noncoherent-ω-Precategory l2 l2 + hom-noncoherent-ω-precategory-Noncoherent-ω-Precategory + x y = + make-Noncoherent-ω-Precategory + ( id-structure-hom-globular-type-Noncoherent-ω-Precategory + {x} {y}) + ( comp-structure-hom-globular-type-Noncoherent-ω-Precategory) +``` + +2-Morphisms in a noncoherent ω-precategory: + +```agda + 2-hom-Noncoherent-ω-Precategory : + {x y : obj-Noncoherent-ω-Precategory} → + hom-Noncoherent-ω-Precategory x y → + hom-Noncoherent-ω-Precategory x y → + UU l2 + 2-hom-Noncoherent-ω-Precategory = + 2-cell-Globular-Type globular-type-Noncoherent-ω-Precategory + + id-2-hom-Noncoherent-ω-Precategory : + {x y : obj-Noncoherent-ω-Precategory} + {f : hom-Noncoherent-ω-Precategory x y} → + 2-hom-Noncoherent-ω-Precategory f f + id-2-hom-Noncoherent-ω-Precategory = + refl-3-cell-is-reflexive-Globular-Type + id-structure-Noncoherent-ω-Precategory + + comp-2-hom-Noncoherent-ω-Precategory : + {x y : obj-Noncoherent-ω-Precategory} + {f g h : hom-Noncoherent-ω-Precategory x y} → + 2-hom-Noncoherent-ω-Precategory g h → + 2-hom-Noncoherent-ω-Precategory f g → + 2-hom-Noncoherent-ω-Precategory f h + comp-2-hom-Noncoherent-ω-Precategory = + comp-2-cell-is-transitive-Globular-Type + comp-structure-Noncoherent-ω-Precategory +``` + +3-Morphisms in a noncoherent ω-precategory: + +```agda + 3-hom-Noncoherent-ω-Precategory : + {x y : obj-Noncoherent-ω-Precategory} + {f g : hom-Noncoherent-ω-Precategory x y} → + 2-hom-Noncoherent-ω-Precategory f g → + 2-hom-Noncoherent-ω-Precategory f g → UU l2 + 3-hom-Noncoherent-ω-Precategory = + 3-cell-Globular-Type globular-type-Noncoherent-ω-Precategory + + id-3-hom-Noncoherent-ω-Precategory : + {x y : obj-Noncoherent-ω-Precategory} + {f g : hom-Noncoherent-ω-Precategory x y} + {H : 2-hom-Noncoherent-ω-Precategory f g} → + 3-hom-Noncoherent-ω-Precategory H H + id-3-hom-Noncoherent-ω-Precategory = + refl-4-cell-is-reflexive-Globular-Type + globular-type-Noncoherent-ω-Precategory + id-structure-Noncoherent-ω-Precategory + + comp-3-hom-Noncoherent-ω-Precategory : + {x y : obj-Noncoherent-ω-Precategory} + {f g : hom-Noncoherent-ω-Precategory x y} + {H K L : 2-hom-Noncoherent-ω-Precategory f g} → + 3-hom-Noncoherent-ω-Precategory K L → + 3-hom-Noncoherent-ω-Precategory H K → + 3-hom-Noncoherent-ω-Precategory H L + comp-3-hom-Noncoherent-ω-Precategory = + comp-3-cell-is-transitive-Globular-Type + comp-structure-Noncoherent-ω-Precategory +``` diff --git a/src/wild-category-theory/noncoherent-wild-higher-precategories.lagda.md b/src/wild-category-theory/noncoherent-wild-higher-precategories.lagda.md deleted file mode 100644 index b558da4ca2..0000000000 --- a/src/wild-category-theory/noncoherent-wild-higher-precategories.lagda.md +++ /dev/null @@ -1,276 +0,0 @@ -# Noncoherent wild higher precategories - -```agda -{-# OPTIONS --guardedness #-} - -module wild-category-theory.noncoherent-wild-higher-precategories where -``` - -
Imports - -```agda -open import category-theory.precategories - -open import foundation.action-on-identifications-binary-functions -open import foundation.cartesian-product-types -open import foundation.dependent-pair-types -open import foundation.function-types -open import foundation.homotopies -open import foundation.identity-types -open import foundation.sets -open import foundation.strictly-involutive-identity-types -open import foundation.universe-levels - -open import globular-types.globular-types -open import globular-types.reflexive-globular-types -open import globular-types.transitive-globular-types -``` - -
- -## Idea - -It is an important open problem known as the _coherence problem_ to define a -fully coherent notion of $∞$-category in univalent type theory. The subject of -_wild category theory_ attempts to recover some of the benefits of $∞$-category -theory without tackling this problem. We introduce, as one of our basic building -blocks in this subject, the notion of a _noncoherent wild higher precategory_. - -A _noncoherent wild higher precategory_ `𝒞` is a structure that attempts at -capturing the structure of a higher precategory to the $0$'th order. It consists -of in some sense all of the operations and none of the coherence of a higher -precategory. Thus, it is defined as a -[globular type](globular-types.globular-types.md) with families of $n$-morphisms -labeled as "identities" - -```text - id-hom : (x : 𝑛-Cell 𝒞) → (𝑛+1)-Cell 𝒞 x x -``` - -and a composition operation at every dimension - -```text - comp-hom : - {x y z : 𝑛-Cell 𝒞} → (𝑛+1)-Cell 𝒞 y z → (𝑛+1)-Cell 𝒞 x y → (𝑛+1)-Cell 𝒞 x z. -``` - -Entirely concretely, we define a -{{#concept "noncoherent wild higher precategory" Agda=Noncoherent-Wild-Higher-Precategory}} -to be a [reflexive](globular-types.reflexive-globular-types.md) and -[transitive](globular-types.transitive-globular-types.md) globular type. We call -the 0-cells the _objects_, the 1-cells the _morphisms_ and the higher cells the -_$n$-morphisms_. The reflexivities are called the _identity morphisms_, and the -transitivity operations are branded as _composition of morphisms_. - -## Definitions - -### Noncoherent wild higher precategories - -```agda -Noncoherent-Wild-Higher-Precategory : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2) -Noncoherent-Wild-Higher-Precategory l1 l2 = - Σ ( Globular-Type l1 l2) - ( λ X → is-reflexive-Globular-Type X × is-transitive-Globular-Type X) - -make-Noncoherent-Wild-Higher-Precategory : - {l1 l2 : Level} {X : Globular-Type l1 l2} → is-reflexive-Globular-Type X → - is-transitive-Globular-Type X → Noncoherent-Wild-Higher-Precategory l1 l2 -make-Noncoherent-Wild-Higher-Precategory id comp = - ( _ , id , comp) - -{-# INLINE make-Noncoherent-Wild-Higher-Precategory #-} - -module _ - {l1 l2 : Level} (𝒞 : Noncoherent-Wild-Higher-Precategory l1 l2) - where - - globular-type-Noncoherent-Wild-Higher-Precategory : Globular-Type l1 l2 - globular-type-Noncoherent-Wild-Higher-Precategory = pr1 𝒞 - - obj-Noncoherent-Wild-Higher-Precategory : UU l1 - obj-Noncoherent-Wild-Higher-Precategory = - 0-cell-Globular-Type globular-type-Noncoherent-Wild-Higher-Precategory -``` - -Morphisms in a noncoherent wild higher precategory: - -```agda - hom-globular-type-Noncoherent-Wild-Higher-Precategory : - (x y : obj-Noncoherent-Wild-Higher-Precategory) → - Globular-Type l2 l2 - hom-globular-type-Noncoherent-Wild-Higher-Precategory = - 1-cell-globular-type-Globular-Type - globular-type-Noncoherent-Wild-Higher-Precategory - - hom-Noncoherent-Wild-Higher-Precategory : - obj-Noncoherent-Wild-Higher-Precategory → - obj-Noncoherent-Wild-Higher-Precategory → - UU l2 - hom-Noncoherent-Wild-Higher-Precategory = - 1-cell-Globular-Type globular-type-Noncoherent-Wild-Higher-Precategory -``` - -Identity morphisms in a noncoherent wild higher precategory: - -```agda - id-structure-Noncoherent-Wild-Higher-Precategory : - is-reflexive-Globular-Type globular-type-Noncoherent-Wild-Higher-Precategory - id-structure-Noncoherent-Wild-Higher-Precategory = - pr1 (pr2 𝒞) - - id-hom-Noncoherent-Wild-Higher-Precategory : - {x : obj-Noncoherent-Wild-Higher-Precategory} → - hom-Noncoherent-Wild-Higher-Precategory x x - id-hom-Noncoherent-Wild-Higher-Precategory {x} = - refl-2-cell-is-reflexive-Globular-Type - id-structure-Noncoherent-Wild-Higher-Precategory - - id-structure-hom-globular-type-Noncoherent-Wild-Higher-Precategory : - {x y : obj-Noncoherent-Wild-Higher-Precategory} → - is-reflexive-Globular-Type - ( hom-globular-type-Noncoherent-Wild-Higher-Precategory x y) - id-structure-hom-globular-type-Noncoherent-Wild-Higher-Precategory = - is-reflexive-1-cell-globular-type-is-reflexive-Globular-Type - id-structure-Noncoherent-Wild-Higher-Precategory - - reflexive-globular-type-Noncoherent-Wild-Higher-Precategory : - Reflexive-Globular-Type l1 l2 - globular-type-Reflexive-Globular-Type - reflexive-globular-type-Noncoherent-Wild-Higher-Precategory = - globular-type-Noncoherent-Wild-Higher-Precategory - refl-Reflexive-Globular-Type - reflexive-globular-type-Noncoherent-Wild-Higher-Precategory = - id-structure-Noncoherent-Wild-Higher-Precategory - - hom-reflexive-globular-type-Noncoherent-Wild-Higher-Precategory : - (x y : obj-Noncoherent-Wild-Higher-Precategory) → - Reflexive-Globular-Type l2 l2 - hom-reflexive-globular-type-Noncoherent-Wild-Higher-Precategory x y = - 1-cell-reflexive-globular-type-Reflexive-Globular-Type - ( reflexive-globular-type-Noncoherent-Wild-Higher-Precategory) - ( x) - ( y) -``` - -Composition in a noncoherent wild higher precategory: - -```agda - comp-structure-Noncoherent-Wild-Higher-Precategory : - is-transitive-Globular-Type - globular-type-Noncoherent-Wild-Higher-Precategory - comp-structure-Noncoherent-Wild-Higher-Precategory = - pr2 (pr2 𝒞) - - comp-hom-Noncoherent-Wild-Higher-Precategory : - {x y z : obj-Noncoherent-Wild-Higher-Precategory} → - hom-Noncoherent-Wild-Higher-Precategory y z → - hom-Noncoherent-Wild-Higher-Precategory x y → - hom-Noncoherent-Wild-Higher-Precategory x z - comp-hom-Noncoherent-Wild-Higher-Precategory = - comp-1-cell-is-transitive-Globular-Type - comp-structure-Noncoherent-Wild-Higher-Precategory - - comp-structure-hom-globular-type-Noncoherent-Wild-Higher-Precategory : - {x y : obj-Noncoherent-Wild-Higher-Precategory} → - is-transitive-Globular-Type - ( hom-globular-type-Noncoherent-Wild-Higher-Precategory x y) - comp-structure-hom-globular-type-Noncoherent-Wild-Higher-Precategory = - is-transitive-1-cell-globular-type-is-transitive-Globular-Type - comp-structure-Noncoherent-Wild-Higher-Precategory - - transitive-globular-type-Noncoherent-Wild-Higher-Precategory : - Transitive-Globular-Type l1 l2 - globular-type-Transitive-Globular-Type - transitive-globular-type-Noncoherent-Wild-Higher-Precategory = - globular-type-Noncoherent-Wild-Higher-Precategory - is-transitive-Transitive-Globular-Type - transitive-globular-type-Noncoherent-Wild-Higher-Precategory = - comp-structure-Noncoherent-Wild-Higher-Precategory - - hom-transitive-globular-type-Noncoherent-Wild-Higher-Precategory : - (x y : obj-Noncoherent-Wild-Higher-Precategory) → - Transitive-Globular-Type l2 l2 - hom-transitive-globular-type-Noncoherent-Wild-Higher-Precategory x y = - 1-cell-transitive-globular-type-Transitive-Globular-Type - ( transitive-globular-type-Noncoherent-Wild-Higher-Precategory) - ( x) - ( y) -``` - -The noncoherent wild higher precategory of morphisms between two objects in a -noncoherent wild higher precategory: - -```agda - hom-noncoherent-wild-higher-precategory-Noncoherent-Wild-Higher-Precategory : - (x y : obj-Noncoherent-Wild-Higher-Precategory) → - Noncoherent-Wild-Higher-Precategory l2 l2 - hom-noncoherent-wild-higher-precategory-Noncoherent-Wild-Higher-Precategory - x y = - make-Noncoherent-Wild-Higher-Precategory - ( id-structure-hom-globular-type-Noncoherent-Wild-Higher-Precategory - {x} {y}) - ( comp-structure-hom-globular-type-Noncoherent-Wild-Higher-Precategory) -``` - -2-Morphisms in a noncoherent wild higher precategory: - -```agda - 2-hom-Noncoherent-Wild-Higher-Precategory : - {x y : obj-Noncoherent-Wild-Higher-Precategory} → - hom-Noncoherent-Wild-Higher-Precategory x y → - hom-Noncoherent-Wild-Higher-Precategory x y → - UU l2 - 2-hom-Noncoherent-Wild-Higher-Precategory = - 2-cell-Globular-Type globular-type-Noncoherent-Wild-Higher-Precategory - - id-2-hom-Noncoherent-Wild-Higher-Precategory : - {x y : obj-Noncoherent-Wild-Higher-Precategory} - {f : hom-Noncoherent-Wild-Higher-Precategory x y} → - 2-hom-Noncoherent-Wild-Higher-Precategory f f - id-2-hom-Noncoherent-Wild-Higher-Precategory = - refl-3-cell-is-reflexive-Globular-Type - id-structure-Noncoherent-Wild-Higher-Precategory - - comp-2-hom-Noncoherent-Wild-Higher-Precategory : - {x y : obj-Noncoherent-Wild-Higher-Precategory} - {f g h : hom-Noncoherent-Wild-Higher-Precategory x y} → - 2-hom-Noncoherent-Wild-Higher-Precategory g h → - 2-hom-Noncoherent-Wild-Higher-Precategory f g → - 2-hom-Noncoherent-Wild-Higher-Precategory f h - comp-2-hom-Noncoherent-Wild-Higher-Precategory = - comp-2-cell-is-transitive-Globular-Type - comp-structure-Noncoherent-Wild-Higher-Precategory -``` - -3-Morphisms in a noncoherent wild higher precategory: - -```agda - 3-hom-Noncoherent-Wild-Higher-Precategory : - {x y : obj-Noncoherent-Wild-Higher-Precategory} - {f g : hom-Noncoherent-Wild-Higher-Precategory x y} → - 2-hom-Noncoherent-Wild-Higher-Precategory f g → - 2-hom-Noncoherent-Wild-Higher-Precategory f g → UU l2 - 3-hom-Noncoherent-Wild-Higher-Precategory = - 3-cell-Globular-Type globular-type-Noncoherent-Wild-Higher-Precategory - - id-3-hom-Noncoherent-Wild-Higher-Precategory : - {x y : obj-Noncoherent-Wild-Higher-Precategory} - {f g : hom-Noncoherent-Wild-Higher-Precategory x y} - {H : 2-hom-Noncoherent-Wild-Higher-Precategory f g} → - 3-hom-Noncoherent-Wild-Higher-Precategory H H - id-3-hom-Noncoherent-Wild-Higher-Precategory = - refl-4-cell-is-reflexive-Globular-Type - globular-type-Noncoherent-Wild-Higher-Precategory - id-structure-Noncoherent-Wild-Higher-Precategory - - comp-3-hom-Noncoherent-Wild-Higher-Precategory : - {x y : obj-Noncoherent-Wild-Higher-Precategory} - {f g : hom-Noncoherent-Wild-Higher-Precategory x y} - {H K L : 2-hom-Noncoherent-Wild-Higher-Precategory f g} → - 3-hom-Noncoherent-Wild-Higher-Precategory K L → - 3-hom-Noncoherent-Wild-Higher-Precategory H K → - 3-hom-Noncoherent-Wild-Higher-Precategory H L - comp-3-hom-Noncoherent-Wild-Higher-Precategory = - comp-3-cell-is-transitive-Globular-Type - comp-structure-Noncoherent-Wild-Higher-Precategory -```