diff --git a/src/foundation-core/pullbacks.lagda.md b/src/foundation-core/pullbacks.lagda.md index 9749065efc..332e6e96e2 100644 --- a/src/foundation-core/pullbacks.lagda.md +++ b/src/foundation-core/pullbacks.lagda.md @@ -15,6 +15,7 @@ open import foundation.functoriality-fibers-of-maps open import foundation.identity-types open import foundation.morphisms-arrows open import foundation.standard-pullbacks +open import foundation.type-arithmetic-standard-pullbacks open import foundation.universe-levels open import foundation-core.commuting-triangles-of-maps diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md index 78a7642b23..df1b40c78a 100644 --- a/src/foundation.lagda.md +++ b/src/foundation.lagda.md @@ -76,6 +76,7 @@ open import foundation.complements public open import foundation.complements-subtypes public open import foundation.composite-maps-in-inverse-sequential-diagrams public open import foundation.composition-algebra public +open import foundation.composition-spans public open import foundation.computational-identity-types public open import foundation.cones-over-cospan-diagrams public open import foundation.cones-over-inverse-sequential-diagrams public @@ -380,6 +381,7 @@ open import foundation.split-idempotent-maps public open import foundation.split-surjective-maps public open import foundation.standard-apartness-relations public open import foundation.standard-pullbacks public +open import foundation.standard-ternary-pullbacks public open import foundation.strict-symmetrization-binary-relations public open import foundation.strictly-involutive-identity-types public open import foundation.strictly-right-unital-concatenation-identifications public @@ -432,6 +434,7 @@ open import foundation.type-arithmetic-coproduct-types public open import foundation.type-arithmetic-dependent-function-types public open import foundation.type-arithmetic-dependent-pair-types public open import foundation.type-arithmetic-empty-type public +open import foundation.type-arithmetic-standard-pullbacks public open import foundation.type-arithmetic-unit-type public open import foundation.type-duality public open import foundation.type-theoretic-principle-of-choice public diff --git a/src/foundation/composition-spans.lagda.md b/src/foundation/composition-spans.lagda.md new file mode 100644 index 0000000000..2611cdf5b1 --- /dev/null +++ b/src/foundation/composition-spans.lagda.md @@ -0,0 +1,163 @@ +# Composition of spans + +```agda +module foundation.composition-spans where +``` + +
Imports + +```agda +open import foundation.commuting-triangles-of-maps +open import foundation.dependent-pair-types +open import foundation.equivalences +open import foundation.equivalences-arrows +open import foundation.equivalences-spans +open import foundation.homotopies +open import foundation.identity-types +open import foundation.morphisms-arrows +open import foundation.morphisms-spans +open import foundation.pullbacks +open import foundation.spans +open import foundation.standard-pullbacks +open import foundation.type-arithmetic-standard-pullbacks +open import foundation.universe-levels + +open import foundation-core.function-types +``` + +
+ +## Idea + +Given two [spans](foundation.spans.md) `F` and `G` such that the source of `G` +is the target of `F` + +```text + F G + + A <----- S -----> B <----- T -----> C, +``` + +then we may +{{#concept "compose" Disambiguation="spans of types" Agda=comp-span}} the two +spans by forming the [pullback](foundation.standard-pullbacks.md) of the middle +[cospan diagram](foundation.cospan-diagrams.md) + +```text + ∙ ------> T ------> C + | ⌟ | + | | G + ∨ ∨ + S ------> B + | + | F + ∨ + A +``` + +giving us a span `G ∘ F` from `A` to `C`. This operation is unital and +associative. + +## Definitions + +### Composition of spans + +```agda +module _ + {l1 l2 l3 l4 l5 : Level} + {A : UU l1} {B : UU l2} {C : UU l3} + (G : span l4 B C) (F : span l5 A B) + where + + spanning-type-comp-span : UU (l2 ⊔ l4 ⊔ l5) + spanning-type-comp-span = + standard-pullback (right-map-span F) (left-map-span G) + + left-map-comp-span : spanning-type-comp-span → A + left-map-comp-span = left-map-span F ∘ vertical-map-standard-pullback + + right-map-comp-span : spanning-type-comp-span → C + right-map-comp-span = right-map-span G ∘ horizontal-map-standard-pullback + + comp-span : span (l2 ⊔ l4 ⊔ l5) A C + comp-span = spanning-type-comp-span , left-map-comp-span , right-map-comp-span +``` + +## Properties + +### Associativity of composition of spans + +```agda +module _ + {l1 l2 l3 l4 l5 l6 l7 : Level} + {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4} + (H : span l5 C D) (G : span l6 B C) (F : span l7 A B) + where + + essentially-associative-spanning-type-comp-span : + spanning-type-comp-span (comp-span H G) F ≃ + spanning-type-comp-span H (comp-span G F) + essentially-associative-spanning-type-comp-span = + inv-associative-standard-pullback + ( right-map-span F) + ( left-map-span G) + ( right-map-span G) + ( left-map-span H) + + essentially-associative-comp-span : + equiv-span (comp-span (comp-span H G) F) (comp-span H (comp-span G F)) + essentially-associative-comp-span = + ( essentially-associative-spanning-type-comp-span , refl-htpy , refl-htpy) + + associative-comp-span : + comp-span (comp-span H G) F ＝ comp-span H (comp-span G F) + associative-comp-span = + eq-equiv-span + ( comp-span (comp-span H G) F) + ( comp-span H (comp-span G F)) + ( essentially-associative-comp-span) +``` + +### The left unit law for composition of spans + +```agda +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (F : span l3 A B) + where + + left-unit-law-comp-span' : + equiv-span F (comp-span id-span F) + left-unit-law-comp-span' = + inv-right-unit-law-standard-pullback (right-map-span F) , + refl-htpy , + refl-htpy + + left-unit-law-comp-span : + equiv-span (comp-span id-span F) F + left-unit-law-comp-span = + right-unit-law-standard-pullback (right-map-span F) , + refl-htpy , + inv-htpy coherence-square-standard-pullback +``` + +### The right unit law for composition of spans + +```agda +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (F : span l3 A B) + where + + right-unit-law-comp-span' : + equiv-span F (comp-span F id-span) + right-unit-law-comp-span' = + inv-left-unit-law-standard-pullback (left-map-span F) , + refl-htpy , + refl-htpy + + right-unit-law-comp-span : + equiv-span (comp-span F id-span) F + right-unit-law-comp-span = + left-unit-law-standard-pullback (left-map-span F) , + coherence-square-standard-pullback , + refl-htpy +``` diff --git a/src/foundation/operations-spans.lagda.md b/src/foundation/operations-spans.lagda.md index 9037d78969..6562513941 100644 --- a/src/foundation/operations-spans.lagda.md +++ b/src/foundation/operations-spans.lagda.md @@ -138,3 +138,8 @@ module _ pr2 (pr2 right-concat-equiv-arrow-span) = right-map-right-concat-equiv-arrow-span ``` + +## See also + +- [Composition of spans](foundation.composition-spans.md) +- [Opposite spans](foundation.opposite-spans.md) diff --git a/src/foundation/standard-pullbacks.lagda.md b/src/foundation/standard-pullbacks.lagda.md index bd7131a988..8f0db009ca 100644 --- a/src/foundation/standard-pullbacks.lagda.md +++ b/src/foundation/standard-pullbacks.lagda.md @@ -129,36 +129,6 @@ module _ pr2 (pr2 (gap c z)) = coherence-square-cone f g c z ``` -#### The standard ternary pullback - -Given two cospans with a shared vertex `B`: - -```text - f g h i - A ----> X <---- B ----> Y <---- C, -``` - -we call the standard limit of the diagram the -{{#concept "standard ternary pullback" Disambiguation="of types" Agda=standard-ternary-pullback}}. -It is defined as the sum - -```text - standard-ternary-pullback f g h i := - Σ (a : A) (b : B) (c : C), ((f a ＝ g b) × (h b ＝ i c)). -``` - -```agda -module _ - {l1 l2 l3 l4 l5 : Level} - {X : UU l1} {Y : UU l2} {A : UU l3} {B : UU l4} {C : UU l5} - (f : A → X) (g : B → X) (h : B → Y) (i : C → Y) - where - - standard-ternary-pullback : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5) - standard-ternary-pullback = - Σ A (λ a → Σ B (λ b → Σ C (λ c → (f a ＝ g b) × (h b ＝ i c)))) -``` - ## Properties ### Characterization of the identity type of the standard pullback @@ -257,231 +227,6 @@ module _ pr2 (pr2 (htpy-cone-up-pullback-standard-pullback c)) = right-unit-htpy ``` -### Standard pullbacks are symmetric - -The standard pullback of `f : A -> X <- B : g` is equivalent to the standard -pullback of `g : B -> X <- A : f`. - -```agda -map-commutative-standard-pullback : - {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3} - (f : A → X) (g : B → X) → standard-pullback f g → standard-pullback g f -pr1 (map-commutative-standard-pullback f g x) = - horizontal-map-standard-pullback x -pr1 (pr2 (map-commutative-standard-pullback f g x)) = - vertical-map-standard-pullback x -pr2 (pr2 (map-commutative-standard-pullback f g x)) = - inv (coherence-square-standard-pullback x) - -inv-inv-map-commutative-standard-pullback : - {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3} - (f : A → X) (g : B → X) → - ( map-commutative-standard-pullback f g ∘ - map-commutative-standard-pullback g f) ~ id -inv-inv-map-commutative-standard-pullback f g x = - eq-pair-eq-fiber - ( eq-pair-eq-fiber - ( inv-inv (coherence-square-standard-pullback x))) - -abstract - is-equiv-map-commutative-standard-pullback : - {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3} - (f : A → X) (g : B → X) → is-equiv (map-commutative-standard-pullback f g) - is-equiv-map-commutative-standard-pullback f g = - is-equiv-is-invertible - ( map-commutative-standard-pullback g f) - ( inv-inv-map-commutative-standard-pullback f g) - ( inv-inv-map-commutative-standard-pullback g f) - -commutative-standard-pullback : - {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3} - (f : A → X) (g : B → X) → - standard-pullback f g ≃ standard-pullback g f -pr1 (commutative-standard-pullback f g) = - map-commutative-standard-pullback f g -pr2 (commutative-standard-pullback f g) = - is-equiv-map-commutative-standard-pullback f g -``` - -#### The gap map of the swapped cone computes as the underlying gap map followed by a swap - -```agda -triangle-map-commutative-standard-pullback : - {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {C : UU l4} - (f : A → X) (g : B → X) (c : cone f g C) → - gap g f (swap-cone f g c) ~ - map-commutative-standard-pullback f g ∘ gap f g c -triangle-map-commutative-standard-pullback f g c = refl-htpy -``` - -### Standard pullbacks are associative - -Consider two cospans with a shared vertex `B`: - -```text - f g h i - A ----> X <---- B ----> Y <---- C, -``` - -then we can construct their limit using standard pullbacks in two equivalent -ways. We can construct it by first forming the standard pullback of `f` and `g`, -and then forming the standard pullback of the resulting `h ∘ f'` and `i` - -```text - (A ×_X B) ×_Y C ---------------------> C - | ⌟ | - | | i - ∨ ∨ - A ×_X B ---------> B ------------> Y - | ⌟ f' | h - | | g - ∨ ∨ - A ------------> X, - f -``` - -or we can first form the pullback of `h` and `i`, and then form the pullback of -`f` and the resulting `g ∘ i'`: - -```text - A ×_X (B ×_Y C) --> B ×_Y C ---------> C - | ⌟ | ⌟ | - | | i' | i - | ∨ ∨ - | B ------------> Y - | | h - | | g - ∨ ∨ - A ------------> X. - f -``` - -We show that both of these constructions are equivalent by showing they are -equivalent to the standard ternary pullback. - -**Note:** Associativity with respect to ternary cospans - -```text - B - | - | g - ∨ - A ------> X <------ C - f h -``` - -is a special case of what we consider here that is recovered by using - -```text - f g g h - A ----> X <---- B ----> X <---- C. -``` - -- See also the following relevant stack exchange question: - [Associativity of pullbacks](https://math.stackexchange.com/questions/2046276/associativity-of-pullbacks). - -#### Computing the left associated iterated standard pullback - -```agda -module _ - {l1 l2 l3 l4 l5 : Level} - {X : UU l1} {Y : UU l2} {A : UU l3} {B : UU l4} {C : UU l5} - (f : A → X) (g : B → X) (h : B → Y) (i : C → Y) - where - - map-left-associative-standard-pullback : - standard-pullback (h ∘ horizontal-map-standard-pullback {f = f} {g = g}) i → - standard-ternary-pullback f g h i - map-left-associative-standard-pullback ((a , b , p) , c , q) = - ( a , b , c , p , q) - - map-inv-left-associative-standard-pullback : - standard-ternary-pullback f g h i → - standard-pullback (h ∘ horizontal-map-standard-pullback {f = f} {g = g}) i - map-inv-left-associative-standard-pullback (a , b , c , p , q) = - ( ( a , b , p) , c , q) - - is-equiv-map-left-associative-standard-pullback : - is-equiv map-left-associative-standard-pullback - is-equiv-map-left-associative-standard-pullback = - is-equiv-is-invertible - ( map-inv-left-associative-standard-pullback) - ( refl-htpy) - ( refl-htpy) - - compute-left-associative-standard-pullback : - standard-pullback (h ∘ horizontal-map-standard-pullback {f = f} {g = g}) i ≃ - standard-ternary-pullback f g h i - compute-left-associative-standard-pullback = - ( map-left-associative-standard-pullback , - is-equiv-map-left-associative-standard-pullback) -``` - -#### Computing the right associated iterated dependent pullback - -```agda -module _ - {l1 l2 l3 l4 l5 : Level} - {X : UU l1} {Y : UU l2} {A : UU l3} {B : UU l4} {C : UU l5} - (f : A → X) (g : B → X) (h : B → Y) (i : C → Y) - where - - map-right-associative-standard-pullback : - standard-pullback f (g ∘ vertical-map-standard-pullback {f = h} {g = i}) → - standard-ternary-pullback f g h i - map-right-associative-standard-pullback (a , (b , c , p) , q) = - ( a , b , c , q , p) - - map-inv-right-associative-standard-pullback : - standard-ternary-pullback f g h i → - standard-pullback f (g ∘ vertical-map-standard-pullback {f = h} {g = i}) - map-inv-right-associative-standard-pullback (a , b , c , p , q) = - ( a , (b , c , q) , p) - - is-equiv-map-right-associative-standard-pullback : - is-equiv map-right-associative-standard-pullback - is-equiv-map-right-associative-standard-pullback = - is-equiv-is-invertible - ( map-inv-right-associative-standard-pullback) - ( refl-htpy) - ( refl-htpy) - - compute-right-associative-standard-pullback : - standard-pullback f (g ∘ vertical-map-standard-pullback {f = h} {g = i}) ≃ - standard-ternary-pullback f g h i - compute-right-associative-standard-pullback = - ( map-right-associative-standard-pullback , - is-equiv-map-right-associative-standard-pullback) -``` - -#### Standard pullbacks are associative - -```agda -module _ - {l1 l2 l3 l4 l5 : Level} - {X : UU l1} {Y : UU l2} {A : UU l3} {B : UU l4} {C : UU l5} - (f : A → X) (g : B → X) (h : B → Y) (i : C → Y) - where - - associative-standard-pullback : - standard-pullback (h ∘ horizontal-map-standard-pullback {f = f} {g = g}) i ≃ - standard-pullback f (g ∘ vertical-map-standard-pullback {f = h} {g = i}) - associative-standard-pullback = - ( inv-equiv (compute-right-associative-standard-pullback f g h i)) ∘e - ( compute-left-associative-standard-pullback f g h i) - - map-associative-standard-pullback : - standard-pullback (h ∘ horizontal-map-standard-pullback {f = f} {g = g}) i → - standard-pullback f (g ∘ vertical-map-standard-pullback {f = h} {g = i}) - map-associative-standard-pullback = map-equiv associative-standard-pullback - - map-inv-associative-standard-pullback : - standard-pullback f (g ∘ vertical-map-standard-pullback {f = h} {g = i}) → - standard-pullback (h ∘ horizontal-map-standard-pullback {f = f} {g = g}) i - map-inv-associative-standard-pullback = - map-inv-equiv associative-standard-pullback -``` - ### Pullbacks can be "folded" Given a standard pullback square diff --git a/src/foundation/standard-ternary-pullbacks.lagda.md b/src/foundation/standard-ternary-pullbacks.lagda.md new file mode 100644 index 0000000000..6ca4fd1596 --- /dev/null +++ b/src/foundation/standard-ternary-pullbacks.lagda.md @@ -0,0 +1,76 @@ +# Standard ternary pullbacks + +```agda +module foundation.standard-ternary-pullbacks where +``` + +
Imports + +```agda +open import foundation.action-on-identifications-functions +open import foundation.cones-over-cospan-diagrams +open import foundation.dependent-pair-types +open import foundation.equality-cartesian-product-types +open import foundation.functoriality-cartesian-product-types +open import foundation.identity-types +open import foundation.structure-identity-principle +open import foundation.universe-levels + +open import foundation-core.cartesian-product-types +open import foundation-core.commuting-squares-of-maps +open import foundation-core.diagonal-maps-cartesian-products-of-types +open import foundation-core.equality-dependent-pair-types +open import foundation-core.equivalences +open import foundation-core.function-types +open import foundation-core.functoriality-dependent-pair-types +open import foundation-core.homotopies +open import foundation-core.retractions +open import foundation-core.sections +open import foundation-core.type-theoretic-principle-of-choice +open import foundation-core.universal-property-pullbacks +open import foundation-core.whiskering-identifications-concatenation +``` + +
+ +## Idea + +Given two [cospan of types](foundation.cospans.md) with a shared vertex `B`: + +```text + f g h i + A ----> X <---- B ----> Y <---- C, +``` + +we call the standard limit of the diagram the +{{#concept "standard ternary pullback" Disambiguation="of types" Agda=standard-ternary-pullback}}. +It is defined as the [sum](foundation.dependent-pair-types.md) + +```text + standard-ternary-pullback f g h i := + Σ (a : A) (b : B) (c : C), ((f a ＝ g b) × (h b ＝ i c)). +``` + +## Definitions + +```agda +module _ + {l1 l2 l3 l4 l5 : Level} + {X : UU l1} {Y : UU l2} {A : UU l3} {B : UU l4} {C : UU l5} + (f : A → X) (g : B → X) (h : B → Y) (i : C → Y) + where + + standard-ternary-pullback : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5) + standard-ternary-pullback = + Σ A (λ a → Σ B (λ b → Σ C (λ c → (f a ＝ g b) × (h b ＝ i c)))) +``` + +## See also + +- [Type arithmetic with standard pullbacks](foundation.type-arithmetic-standard-pullbacks.md) + +## Table of files about pullbacks + +The following table lists files that are about pullbacks as a general concept. + +{{#include tables/pullbacks.md}} diff --git a/src/foundation/type-arithmetic-standard-pullbacks.lagda.md b/src/foundation/type-arithmetic-standard-pullbacks.lagda.md new file mode 100644 index 0000000000..09335074fa --- /dev/null +++ b/src/foundation/type-arithmetic-standard-pullbacks.lagda.md @@ -0,0 +1,417 @@ +# Type arithmetic with standard pullbacks + +```agda +module foundation.type-arithmetic-standard-pullbacks where +``` + +
Imports + +```agda +open import foundation.cones-over-cospan-diagrams +open import foundation.dependent-pair-types +open import foundation.equality-dependent-pair-types +open import foundation.standard-pullbacks +open import foundation.standard-ternary-pullbacks +open import foundation.type-arithmetic-dependent-pair-types +open import foundation.universe-levels + +open import foundation-core.cartesian-product-types +open import foundation-core.contractible-types +open import foundation-core.equivalences +open import foundation-core.function-types +open import foundation-core.homotopies +open import foundation-core.identity-types +open import foundation-core.propositions +open import foundation-core.retractions +open import foundation-core.sections +``` + +
+ +## Idea + +We prove laws for the manipulation of +[standard pullbacks](foundation.standard-pullbacks.md) with respect to +themselves. + +## Laws + +### Standard pullbacks are associative + +Consider two cospans with a shared vertex `B`: + +```text + f g h i + A ----> X <---- B ----> Y <---- C, +``` + +then we can construct their limit using standard pullbacks in two equivalent +ways. We can construct it by first forming the standard pullback of `f` and `g`, +and then forming the standard pullback of the resulting `h ∘ f'` and `i` + +```text + (A ×_X B) ×_Y C ---------------------> C + | ⌟ | + | | i + ∨ ∨ + A ×_X B ---------> B ------------> Y + | ⌟ f' | h + | | g + ∨ ∨ + A ------------> X, + f +``` + +or we can first form the pullback of `h` and `i`, and then form the pullback of +`f` and the resulting `g ∘ i'`: + +```text + A ×_X (B ×_Y C) --> B ×_Y C ---------> C + | ⌟ | ⌟ | + | | i' | i + | ∨ ∨ + | B ------------> Y + | | h + | | g + ∨ ∨ + A ------------> X. + f +``` + +We show that both of these constructions are equivalent by showing they are +equivalent to the standard ternary pullback. + +**Note:** Associativity with respect to ternary cospans + +```text + B + | + | g + ∨ + A ------> X <------ C + f h +``` + +is a special case of what we consider here that is recovered by using + +```text + f g g h + A ----> X <---- B ----> X <---- C. +``` + +- See also the following relevant stack exchange question: + [Associativity of pullbacks](https://math.stackexchange.com/questions/2046276/associativity-of-pullbacks). + +#### Computing the left associated iterated standard pullback + +```agda +module _ + {l1 l2 l3 l4 l5 : Level} + {X : UU l1} {Y : UU l2} {A : UU l3} {B : UU l4} {C : UU l5} + (f : A → X) (g : B → X) (h : B → Y) (i : C → Y) + where + + map-left-associative-standard-pullback : + standard-pullback (h ∘ horizontal-map-standard-pullback {f = f} {g = g}) i → + standard-ternary-pullback f g h i + map-left-associative-standard-pullback ((a , b , p) , c , q) = + ( a , b , c , p , q) + + map-inv-left-associative-standard-pullback : + standard-ternary-pullback f g h i → + standard-pullback (h ∘ horizontal-map-standard-pullback {f = f} {g = g}) i + map-inv-left-associative-standard-pullback (a , b , c , p , q) = + ( ( a , b , p) , c , q) + + is-equiv-map-left-associative-standard-pullback : + is-equiv map-left-associative-standard-pullback + is-equiv-map-left-associative-standard-pullback = + is-equiv-is-invertible + ( map-inv-left-associative-standard-pullback) + ( refl-htpy) + ( refl-htpy) + + is-equiv-map-inv-left-associative-standard-pullback : + is-equiv map-inv-left-associative-standard-pullback + is-equiv-map-inv-left-associative-standard-pullback = + is-equiv-is-invertible + ( map-left-associative-standard-pullback) + ( refl-htpy) + ( refl-htpy) + + compute-left-associative-standard-pullback : + standard-pullback (h ∘ horizontal-map-standard-pullback {f = f} {g = g}) i ≃ + standard-ternary-pullback f g h i + compute-left-associative-standard-pullback = + ( map-left-associative-standard-pullback , + is-equiv-map-left-associative-standard-pullback) + + compute-inv-left-associative-standard-pullback : + standard-ternary-pullback f g h i ≃ + standard-pullback (h ∘ horizontal-map-standard-pullback {f = f} {g = g}) i + compute-inv-left-associative-standard-pullback = + ( map-inv-left-associative-standard-pullback , + is-equiv-map-inv-left-associative-standard-pullback) +``` + +#### Computing the right associated iterated dependent pullback + +```agda +module _ + {l1 l2 l3 l4 l5 : Level} + {X : UU l1} {Y : UU l2} {A : UU l3} {B : UU l4} {C : UU l5} + (f : A → X) (g : B → X) (h : B → Y) (i : C → Y) + where + + map-right-associative-standard-pullback : + standard-pullback f (g ∘ vertical-map-standard-pullback {f = h} {g = i}) → + standard-ternary-pullback f g h i + map-right-associative-standard-pullback (a , (b , c , p) , q) = + ( a , b , c , q , p) + + map-inv-right-associative-standard-pullback : + standard-ternary-pullback f g h i → + standard-pullback f (g ∘ vertical-map-standard-pullback {f = h} {g = i}) + map-inv-right-associative-standard-pullback (a , b , c , p , q) = + ( a , (b , c , q) , p) + + is-equiv-map-right-associative-standard-pullback : + is-equiv map-right-associative-standard-pullback + is-equiv-map-right-associative-standard-pullback = + is-equiv-is-invertible + ( map-inv-right-associative-standard-pullback) + ( refl-htpy) + ( refl-htpy) + + is-equiv-map-inv-right-associative-standard-pullback : + is-equiv map-inv-right-associative-standard-pullback + is-equiv-map-inv-right-associative-standard-pullback = + is-equiv-is-invertible + ( map-right-associative-standard-pullback) + ( refl-htpy) + ( refl-htpy) + + compute-right-associative-standard-pullback : + standard-pullback f (g ∘ vertical-map-standard-pullback {f = h} {g = i}) ≃ + standard-ternary-pullback f g h i + compute-right-associative-standard-pullback = + ( map-right-associative-standard-pullback , + is-equiv-map-right-associative-standard-pullback) + + compute-inv-right-associative-standard-pullback : + standard-ternary-pullback f g h i ≃ + standard-pullback f (g ∘ vertical-map-standard-pullback {f = h} {g = i}) + compute-inv-right-associative-standard-pullback = + ( map-inv-right-associative-standard-pullback , + is-equiv-map-inv-right-associative-standard-pullback) +``` + +#### Standard pullbacks are associative + +```agda +module _ + {l1 l2 l3 l4 l5 : Level} + {X : UU l1} {Y : UU l2} {A : UU l3} {B : UU l4} {C : UU l5} + (f : A → X) (g : B → X) (h : B → Y) (i : C → Y) + where + + associative-standard-pullback : + standard-pullback (h ∘ horizontal-map-standard-pullback {f = f} {g = g}) i ≃ + standard-pullback f (g ∘ vertical-map-standard-pullback {f = h} {g = i}) + associative-standard-pullback = + ( compute-inv-right-associative-standard-pullback f g h i) ∘e + ( compute-left-associative-standard-pullback f g h i) + + inv-associative-standard-pullback : + standard-pullback f (g ∘ vertical-map-standard-pullback {f = h} {g = i}) ≃ + standard-pullback (h ∘ horizontal-map-standard-pullback {f = f} {g = g}) i + inv-associative-standard-pullback = + ( compute-inv-left-associative-standard-pullback f g h i) ∘e + ( compute-right-associative-standard-pullback f g h i) + + map-associative-standard-pullback : + standard-pullback (h ∘ horizontal-map-standard-pullback {f = f} {g = g}) i → + standard-pullback f (g ∘ vertical-map-standard-pullback {f = h} {g = i}) + map-associative-standard-pullback = map-equiv associative-standard-pullback + + map-inv-associative-standard-pullback : + standard-pullback f (g ∘ vertical-map-standard-pullback {f = h} {g = i}) → + standard-pullback (h ∘ horizontal-map-standard-pullback {f = f} {g = g}) i + map-inv-associative-standard-pullback = + map-inv-equiv associative-standard-pullback +``` + +### Unit laws for standard pullbacks + +Pulling back along the identity map + +```agda +module _ + {l1 l2 : Level} {X : UU l1} {A : UU l2} (f : A → X) + where + + map-left-unit-law-standard-pullback : + standard-pullback id f → A + map-left-unit-law-standard-pullback (x , a , p) = a + + map-inv-left-unit-law-standard-pullback : + A → standard-pullback id f + map-inv-left-unit-law-standard-pullback a = f a , a , refl + + is-section-map-inv-left-unit-law-standard-pullback : + is-section + map-left-unit-law-standard-pullback + map-inv-left-unit-law-standard-pullback + is-section-map-inv-left-unit-law-standard-pullback = refl-htpy + + is-retraction-map-inv-left-unit-law-standard-pullback : + is-retraction + map-left-unit-law-standard-pullback + map-inv-left-unit-law-standard-pullback + is-retraction-map-inv-left-unit-law-standard-pullback (.(f a) , a , refl) = + refl + + is-equiv-map-left-unit-law-standard-pullback : + is-equiv map-left-unit-law-standard-pullback + is-equiv-map-left-unit-law-standard-pullback = + is-equiv-is-invertible + map-inv-left-unit-law-standard-pullback + is-section-map-inv-left-unit-law-standard-pullback + is-retraction-map-inv-left-unit-law-standard-pullback + + is-equiv-map-inv-left-unit-law-standard-pullback : + is-equiv map-inv-left-unit-law-standard-pullback + is-equiv-map-inv-left-unit-law-standard-pullback = + is-equiv-is-invertible + map-left-unit-law-standard-pullback + is-retraction-map-inv-left-unit-law-standard-pullback + is-section-map-inv-left-unit-law-standard-pullback + + left-unit-law-standard-pullback : + standard-pullback id f ≃ A + left-unit-law-standard-pullback = + map-left-unit-law-standard-pullback , + is-equiv-map-left-unit-law-standard-pullback + + inv-left-unit-law-standard-pullback : + A ≃ standard-pullback id f + inv-left-unit-law-standard-pullback = + map-inv-left-unit-law-standard-pullback , + is-equiv-map-inv-left-unit-law-standard-pullback +``` + +### Unit laws for standard pullbacks + +Pulling back along the identity map is the identity operation. + +```agda +module _ + {l1 l2 : Level} {X : UU l1} {A : UU l2} (f : A → X) + where + + map-right-unit-law-standard-pullback : + standard-pullback f id → A + map-right-unit-law-standard-pullback (a , x , p) = a + + map-inv-right-unit-law-standard-pullback : + A → standard-pullback f id + map-inv-right-unit-law-standard-pullback a = a , f a , refl + + is-section-map-inv-right-unit-law-standard-pullback : + is-section + map-right-unit-law-standard-pullback + map-inv-right-unit-law-standard-pullback + is-section-map-inv-right-unit-law-standard-pullback = refl-htpy + + is-retraction-map-inv-right-unit-law-standard-pullback : + is-retraction + map-right-unit-law-standard-pullback + map-inv-right-unit-law-standard-pullback + is-retraction-map-inv-right-unit-law-standard-pullback (a , .(f a) , refl) = + refl + + is-equiv-map-right-unit-law-standard-pullback : + is-equiv map-right-unit-law-standard-pullback + is-equiv-map-right-unit-law-standard-pullback = + is-equiv-is-invertible + map-inv-right-unit-law-standard-pullback + is-section-map-inv-right-unit-law-standard-pullback + is-retraction-map-inv-right-unit-law-standard-pullback + + is-equiv-map-inv-right-unit-law-standard-pullback : + is-equiv map-inv-right-unit-law-standard-pullback + is-equiv-map-inv-right-unit-law-standard-pullback = + is-equiv-is-invertible + map-right-unit-law-standard-pullback + is-retraction-map-inv-right-unit-law-standard-pullback + is-section-map-inv-right-unit-law-standard-pullback + + right-unit-law-standard-pullback : + standard-pullback f id ≃ A + right-unit-law-standard-pullback = + map-right-unit-law-standard-pullback , + is-equiv-map-right-unit-law-standard-pullback + + inv-right-unit-law-standard-pullback : + A ≃ standard-pullback f id + inv-right-unit-law-standard-pullback = + map-inv-right-unit-law-standard-pullback , + is-equiv-map-inv-right-unit-law-standard-pullback +``` + +### Standard pullbacks are symmetric + +The standard pullback of `f : A -> X <- B : g` is equivalent to the standard +pullback of `g : B -> X <- A : f`. + +```agda +map-commutative-standard-pullback : + {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3} + (f : A → X) (g : B → X) → standard-pullback f g → standard-pullback g f +pr1 (map-commutative-standard-pullback f g x) = + horizontal-map-standard-pullback x +pr1 (pr2 (map-commutative-standard-pullback f g x)) = + vertical-map-standard-pullback x +pr2 (pr2 (map-commutative-standard-pullback f g x)) = + inv (coherence-square-standard-pullback x) + +inv-inv-map-commutative-standard-pullback : + {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3} + (f : A → X) (g : B → X) → + ( map-commutative-standard-pullback f g ∘ + map-commutative-standard-pullback g f) ~ id +inv-inv-map-commutative-standard-pullback f g x = + eq-pair-eq-fiber + ( eq-pair-eq-fiber + ( inv-inv (coherence-square-standard-pullback x))) + +abstract + is-equiv-map-commutative-standard-pullback : + {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3} + (f : A → X) (g : B → X) → is-equiv (map-commutative-standard-pullback f g) + is-equiv-map-commutative-standard-pullback f g = + is-equiv-is-invertible + ( map-commutative-standard-pullback g f) + ( inv-inv-map-commutative-standard-pullback f g) + ( inv-inv-map-commutative-standard-pullback g f) + +commutative-standard-pullback : + {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3} + (f : A → X) (g : B → X) → + standard-pullback f g ≃ standard-pullback g f +pr1 (commutative-standard-pullback f g) = + map-commutative-standard-pullback f g +pr2 (commutative-standard-pullback f g) = + is-equiv-map-commutative-standard-pullback f g +``` + +#### The gap map of the swapped cone computes as the underlying gap map followed by a swap + +```agda +triangle-map-commutative-standard-pullback : + {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {C : UU l4} + (f : A → X) (g : B → X) (c : cone f g C) → + gap g f (swap-cone f g c) ~ + map-commutative-standard-pullback f g ∘ gap f g c +triangle-map-commutative-standard-pullback f g c = refl-htpy +``` diff --git a/src/globular-types.lagda.md b/src/globular-types.lagda.md index 260995b614..89ac4160a3 100644 --- a/src/globular-types.lagda.md +++ b/src/globular-types.lagda.md @@ -31,6 +31,7 @@ open import globular-types.fibers-globular-maps public open import globular-types.globular-equivalences public open import globular-types.globular-maps public open import globular-types.globular-types public +open import globular-types.homotopies-globular-maps public open import globular-types.large-colax-reflexive-globular-maps public open import globular-types.large-colax-transitive-globular-maps public open import globular-types.large-globular-maps public diff --git a/src/globular-types/binary-globular-maps.lagda.md b/src/globular-types/binary-globular-maps.lagda.md index aa89346264..16bdfa722f 100644 --- a/src/globular-types/binary-globular-maps.lagda.md +++ b/src/globular-types/binary-globular-maps.lagda.md @@ -13,6 +13,7 @@ open import foundation.universe-levels open import globular-types.globular-maps open import globular-types.globular-types +open import globular-types.points-globular-types ``` @@ -45,19 +46,82 @@ record {l1 l2 l3 l4 l5 l6 : Level} (G : Globular-Type l1 l2) (H : Globular-Type l3 l4) (K : Globular-Type l5 l6) : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5 ⊔ l6) - where - coinductive - field - 0-cell-binary-globular-map : - 0-cell-Globular-Type G → 0-cell-Globular-Type H → - 0-cell-Globular-Type K - 1-cell-binary-globular-map-binary-globular-map : - {x x' : 0-cell-Globular-Type G} - {y y' : 0-cell-Globular-Type H} → - binary-globular-map - ( 1-cell-globular-type-Globular-Type G x x') - ( 1-cell-globular-type-Globular-Type H y y') - ( 1-cell-globular-type-Globular-Type K - ( 0-cell-binary-globular-map x y) - ( 0-cell-binary-globular-map x' y')) + where + coinductive + field + 0-cell-binary-globular-map : + 0-cell-Globular-Type G → 0-cell-Globular-Type H → + 0-cell-Globular-Type K + + 1-cell-binary-globular-map-binary-globular-map : + {x x' : 0-cell-Globular-Type G} + {y y' : 0-cell-Globular-Type H} → + binary-globular-map + ( 1-cell-globular-type-Globular-Type G x x') + ( 1-cell-globular-type-Globular-Type H y y') + ( 1-cell-globular-type-Globular-Type K + ( 0-cell-binary-globular-map x y) + ( 0-cell-binary-globular-map x' y')) + +open binary-globular-map public +``` + +```agda +module _ + {l1 l2 l3 l4 l5 l6 : Level} + {G : Globular-Type l1 l2} {H : Globular-Type l3 l4} {K : Globular-Type l5 l6} + (F : binary-globular-map G H K) + where + + 1-cell-binary-globular-map : + {x x' : 0-cell-Globular-Type G} {y y' : 0-cell-Globular-Type H} → + 1-cell-Globular-Type G x x' → + 1-cell-Globular-Type H y y' → + 1-cell-Globular-Type K + ( 0-cell-binary-globular-map F x y) + ( 0-cell-binary-globular-map F x' y') + 1-cell-binary-globular-map = + 0-cell-binary-globular-map + ( 1-cell-binary-globular-map-binary-globular-map F) + + 2-cell-binary-globular-map : + {x x' : 0-cell-Globular-Type G} + {y y' : 0-cell-Globular-Type H} + {f f' : 1-cell-Globular-Type G x x'} + {g g' : 1-cell-Globular-Type H y y'} → + 2-cell-Globular-Type G f f' → + 2-cell-Globular-Type H g g' → + 2-cell-Globular-Type K + ( 1-cell-binary-globular-map f g) + ( 1-cell-binary-globular-map f' g') + 2-cell-binary-globular-map = + 0-cell-binary-globular-map + ( 1-cell-binary-globular-map-binary-globular-map + ( 1-cell-binary-globular-map-binary-globular-map F)) +``` + +### Evaluating one of the arguments of a binary globular map + +```agda +ev-left-binary-globular-map : + {l1 l2 l3 l4 l5 l6 : Level} + {G : Globular-Type l1 l2} {H : Globular-Type l3 l4} {K : Globular-Type l5 l6} + (F : binary-globular-map G H K) (x : point-Globular-Type G) → globular-map H K +0-cell-globular-map (ev-left-binary-globular-map F x) = + 0-cell-binary-globular-map F (0-cell-point-Globular-Type x) +1-cell-globular-map-globular-map (ev-left-binary-globular-map F x) = + ev-left-binary-globular-map + ( 1-cell-binary-globular-map-binary-globular-map F) + ( 1-cell-point-point-Globular-Type x) + +ev-right-binary-globular-map : + {l1 l2 l3 l4 l5 l6 : Level} + {G : Globular-Type l1 l2} {H : Globular-Type l3 l4} {K : Globular-Type l5 l6} + (F : binary-globular-map G H K) (x : point-Globular-Type H) → globular-map G K +0-cell-globular-map (ev-right-binary-globular-map F x) y = + 0-cell-binary-globular-map F y (0-cell-point-Globular-Type x) +1-cell-globular-map-globular-map (ev-right-binary-globular-map F x) = + ev-right-binary-globular-map + ( 1-cell-binary-globular-map-binary-globular-map F) + ( 1-cell-point-point-Globular-Type x) ``` diff --git a/src/globular-types/composition-structure-globular-types.lagda.md b/src/globular-types/composition-structure-globular-types.lagda.md index cadac1c419..ec0b18b2bd 100644 --- a/src/globular-types/composition-structure-globular-types.lagda.md +++ b/src/globular-types/composition-structure-globular-types.lagda.md @@ -13,6 +13,7 @@ open import foundation.universe-levels open import globular-types.binary-globular-maps open import globular-types.globular-types +open import globular-types.transitive-globular-types ``` @@ -36,10 +37,9 @@ consists of binary operations - ∘ - : (𝑛+1)-Cell G y z → (𝑛+1)-Cell G x y → (𝑛+1)-Cell G x z, ``` -each of which preserve all higher cells of the globular type `G`. Globular -composition structure is therefore a strengthening of the -[transitivity structure](globular-types.transitive-globular-types.md) on -globular types. +each of which preserve all higher cells of the globular type `G`. In comparison +to [transitivity structure](globular-types.transitive-globular-types.md) on +globular types, this also gives horizontal composition of higher cells. ## Definitions @@ -66,5 +66,109 @@ record composition-Globular-Type ( 1-cell-globular-type-Globular-Type G x y) + comp-1-cell-composition-Globular-Type : + {x y z : 0-cell-Globular-Type G} → + 1-cell-Globular-Type G y z → + 1-cell-Globular-Type G x y → + 1-cell-Globular-Type G x z + comp-1-cell-composition-Globular-Type = + 0-cell-binary-globular-map + comp-binary-globular-map-composition-Globular-Type + + horizontal-comp-2-cell-composition-Globular-Type : + {x y z : 0-cell-Globular-Type G} → + {g g' : 1-cell-Globular-Type G y z} → + {f f' : 1-cell-Globular-Type G x y} → + 2-cell-Globular-Type G g g' → + 2-cell-Globular-Type G f f' → + 2-cell-Globular-Type G + ( comp-1-cell-composition-Globular-Type g f) + ( comp-1-cell-composition-Globular-Type g' f') + horizontal-comp-2-cell-composition-Globular-Type = + 1-cell-binary-globular-map + ( comp-binary-globular-map-composition-Globular-Type) + + horizontal-comp-3-cell-composition-Globular-Type' : + {x y z : 0-cell-Globular-Type G} + {g g' : 1-cell-Globular-Type G y z} + {f f' : 1-cell-Globular-Type G x y} + {α α' : 2-cell-Globular-Type G g g'} + {β β' : 2-cell-Globular-Type G f f'} → + 3-cell-Globular-Type G α α' → + 3-cell-Globular-Type G β β' → + 3-cell-Globular-Type G + ( horizontal-comp-2-cell-composition-Globular-Type α β) + ( horizontal-comp-2-cell-composition-Globular-Type α' β') + horizontal-comp-3-cell-composition-Globular-Type' = + 2-cell-binary-globular-map + comp-binary-globular-map-composition-Globular-Type + open composition-Globular-Type public ``` + +```agda +module _ + {l1 l2 : Level} {G : Globular-Type l1 l2} (H : composition-Globular-Type G) + where + + comp-2-cell-composition-Globular-Type : + {x y : 0-cell-Globular-Type G} → + {f g h : 1-cell-Globular-Type G x y} → + 2-cell-Globular-Type G g h → + 2-cell-Globular-Type G f g → + 2-cell-Globular-Type G f h + comp-2-cell-composition-Globular-Type = + comp-1-cell-composition-Globular-Type + ( composition-1-cell-globular-type-Globular-Type H) + + horizontal-comp-3-cell-composition-Globular-Type : + {x y : 0-cell-Globular-Type G} + {f g h : 1-cell-Globular-Type G x y} + {α α' : 2-cell-Globular-Type G g h} + {β β' : 2-cell-Globular-Type G f g} → + 3-cell-Globular-Type G α α' → + 3-cell-Globular-Type G β β' → + 3-cell-Globular-Type G + ( comp-2-cell-composition-Globular-Type α β) + ( comp-2-cell-composition-Globular-Type α' β') + horizontal-comp-3-cell-composition-Globular-Type = + horizontal-comp-2-cell-composition-Globular-Type + ( composition-1-cell-globular-type-Globular-Type H) + +module _ + {l1 l2 : Level} {G : Globular-Type l1 l2} (H : composition-Globular-Type G) + where + + comp-3-cell-composition-Globular-Type : + {x y : 0-cell-Globular-Type G} → + {f g : 1-cell-Globular-Type G x y} → + {α β γ : 2-cell-Globular-Type G f g} → + 3-cell-Globular-Type G β γ → + 3-cell-Globular-Type G α β → + 3-cell-Globular-Type G α γ + comp-3-cell-composition-Globular-Type = + comp-2-cell-composition-Globular-Type + ( composition-1-cell-globular-type-Globular-Type H) +``` + +## Properties + +### Globular types with composition structure are transitive + +```agda +is-transitive-composition-Globular-Type : + {l1 l2 : Level} {G : Globular-Type l1 l2} → + composition-Globular-Type G → + is-transitive-Globular-Type G +comp-1-cell-is-transitive-Globular-Type + ( is-transitive-composition-Globular-Type H) = + comp-1-cell-composition-Globular-Type H +is-transitive-1-cell-globular-type-is-transitive-Globular-Type + ( is-transitive-composition-Globular-Type H) = + is-transitive-composition-Globular-Type + ( composition-1-cell-globular-type-Globular-Type H) +``` + +## See also + +- [Noncoherent wild $\omega$-semiprecategories](wild-category-theory.noncoherent-wild-omega-semiprecategories.md) diff --git a/src/globular-types/globular-equivalences.lagda.md b/src/globular-types/globular-equivalences.lagda.md index 5afece9603..b8a29f84dd 100644 --- a/src/globular-types/globular-equivalences.lagda.md +++ b/src/globular-types/globular-equivalences.lagda.md @@ -29,47 +29,90 @@ A {{#concept "globular equivalence" Agda=globular-equiv}} `e` between pair of $n$-cells `x` and `y`, an equivalence of $(n+1)$-cells ```text - eₙ₊₁ : (𝑛+1)-Cell A x y ≃ (𝑛+1)-Cell B (eₙ x) (eₙ y). + eₙ₊₁ : Aₙ₊₁ x y ≃ Bₙ₊₁ (eₙ x) (eₙ y). ``` ## Definitions -### Equivalences between globular types +### The predicate on a globular map of being an equivalence ```agda record - globular-equiv - {l1 l2 l3 l4 : Level} (A : Globular-Type l1 l2) (B : Globular-Type l3 l4) : + is-equiv-globular-map + {l1 l2 l3 l4 : Level} + {A : Globular-Type l1 l2} {B : Globular-Type l3 l4} + (f : globular-map A B) : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) where coinductive field - 0-cell-equiv-globular-equiv : - 0-cell-Globular-Type A ≃ 0-cell-Globular-Type B - - 0-cell-globular-equiv : 0-cell-Globular-Type A → 0-cell-Globular-Type B - 0-cell-globular-equiv = map-equiv 0-cell-equiv-globular-equiv + is-equiv-0-cell-is-equiv-globular-map : is-equiv (0-cell-globular-map f) - field - 1-cell-globular-equiv-globular-equiv : + 1-cell-is-equiv-globular-map : {x y : 0-cell-Globular-Type A} → - globular-equiv - ( 1-cell-globular-type-Globular-Type A x y) - ( 1-cell-globular-type-Globular-Type B - ( 0-cell-globular-equiv x) - ( 0-cell-globular-equiv y)) + is-equiv-globular-map (1-cell-globular-map-globular-map f {x} {y}) + +open is-equiv-globular-map public +``` -open globular-equiv public +### Equivalences between globular types -globular-map-globular-equiv : - {l1 l2 l3 l4 : Level} - {A : Globular-Type l1 l2} {B : Globular-Type l3 l4} → - globular-equiv A B → globular-map A B -0-cell-globular-map (globular-map-globular-equiv e) = - map-equiv (0-cell-equiv-globular-equiv e) -1-cell-globular-map-globular-map (globular-map-globular-equiv e) = - globular-map-globular-equiv (1-cell-globular-equiv-globular-equiv e) +```agda +globular-equiv : + {l1 l2 l3 l4 : Level} → Globular-Type l1 l2 → Globular-Type l3 l4 → + UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) +globular-equiv A B = Σ (globular-map A B) (is-equiv-globular-map) + +module _ + {l1 l2 l3 l4 : Level} {A : Globular-Type l1 l2} {B : Globular-Type l3 l4} + (e : globular-equiv A B) + where + + globular-map-globular-equiv : globular-map A B + globular-map-globular-equiv = pr1 e + + is-equiv-globular-equiv : is-equiv-globular-map globular-map-globular-equiv + is-equiv-globular-equiv = pr2 e + + 0-cell-map-globular-equiv : 0-cell-Globular-Type A → 0-cell-Globular-Type B + 0-cell-map-globular-equiv = + 0-cell-globular-map globular-map-globular-equiv + + is-equiv-0-cell-map-globular-equiv : is-equiv 0-cell-map-globular-equiv + is-equiv-0-cell-map-globular-equiv = + is-equiv-0-cell-is-equiv-globular-map is-equiv-globular-equiv + + 0-cell-globular-equiv : 0-cell-Globular-Type A ≃ 0-cell-Globular-Type B + 0-cell-globular-equiv = + 0-cell-map-globular-equiv , is-equiv-0-cell-map-globular-equiv + + 1-cell-globular-map-globular-equiv : + (x y : 0-cell-Globular-Type A) → + globular-map + ( 1-cell-globular-type-Globular-Type A x y) + ( 1-cell-globular-type-Globular-Type B + ( 0-cell-map-globular-equiv x) + ( 0-cell-map-globular-equiv y)) + 1-cell-globular-map-globular-equiv x y = + 1-cell-globular-map-globular-map globular-map-globular-equiv + + is-equiv-1-cell-globular-map-globular-equiv : + {x y : 0-cell-Globular-Type A} → + is-equiv-globular-map (1-cell-globular-map-globular-equiv x y) + is-equiv-1-cell-globular-map-globular-equiv = + 1-cell-is-equiv-globular-map is-equiv-globular-equiv + + 1-cell-globular-equiv-globular-equiv : + {x y : 0-cell-Globular-Type A} → + globular-equiv + ( 1-cell-globular-type-Globular-Type A x y) + ( 1-cell-globular-type-Globular-Type B + ( 0-cell-map-globular-equiv x) + ( 0-cell-map-globular-equiv y)) + 1-cell-globular-equiv-globular-equiv {x} {y} = + 1-cell-globular-map-globular-equiv x y , + is-equiv-1-cell-globular-map-globular-equiv module _ {l1 l2 l3 l4 : Level} @@ -81,20 +124,19 @@ module _ {x y : 0-cell-Globular-Type A} → 1-cell-Globular-Type A x y ≃ 1-cell-Globular-Type B - ( 0-cell-globular-equiv e x) - ( 0-cell-globular-equiv e y) + ( 0-cell-map-globular-equiv e x) + ( 0-cell-map-globular-equiv e y) 1-cell-equiv-globular-equiv = - 0-cell-equiv-globular-equiv - ( 1-cell-globular-equiv-globular-equiv e) + 0-cell-globular-equiv (1-cell-globular-equiv-globular-equiv e) - 1-cell-globular-equiv : + 1-cell-map-globular-equiv : {x y : 0-cell-Globular-Type A} → 1-cell-Globular-Type A x y → 1-cell-Globular-Type B - ( 0-cell-globular-equiv e x) - ( 0-cell-globular-equiv e y) - 1-cell-globular-equiv = - 0-cell-globular-equiv (1-cell-globular-equiv-globular-equiv e) + ( 0-cell-map-globular-equiv e x) + ( 0-cell-map-globular-equiv e y) + 1-cell-map-globular-equiv = + 0-cell-map-globular-equiv (1-cell-globular-equiv-globular-equiv e) module _ {l1 l2 l3 l4 : Level} @@ -107,8 +149,8 @@ module _ {f g : 1-cell-Globular-Type A x y} → 2-cell-Globular-Type A f g ≃ 2-cell-Globular-Type B - ( 1-cell-globular-equiv e f) - ( 1-cell-globular-equiv e g) + ( 1-cell-map-globular-equiv e f) + ( 1-cell-map-globular-equiv e g) 2-cell-equiv-globular-equiv = 1-cell-equiv-globular-equiv ( 1-cell-globular-equiv-globular-equiv e) @@ -118,10 +160,10 @@ module _ {f g : 1-cell-Globular-Type A x y} → 2-cell-Globular-Type A f g → 2-cell-Globular-Type B - ( 1-cell-globular-equiv e f) - ( 1-cell-globular-equiv e g) + ( 1-cell-map-globular-equiv e f) + ( 1-cell-map-globular-equiv e g) 2-cell-globular-equiv = - 1-cell-globular-equiv (1-cell-globular-equiv-globular-equiv e) + 1-cell-map-globular-equiv (1-cell-globular-equiv-globular-equiv e) module _ {l1 l2 l3 l4 : Level} @@ -145,18 +187,40 @@ module _ ### The identity equivalence on a globular type ```agda +is-equiv-id-globular-map : + {l1 l2 : Level} (A : Globular-Type l1 l2) → + is-equiv-globular-map (id-globular-map A) +is-equiv-0-cell-is-equiv-globular-map (is-equiv-id-globular-map A) = is-equiv-id +1-cell-is-equiv-globular-map (is-equiv-id-globular-map A) = + is-equiv-id-globular-map (1-cell-globular-type-Globular-Type A _ _) + id-globular-equiv : {l1 l2 : Level} (A : Globular-Type l1 l2) → globular-equiv A A -id-globular-equiv A = - λ where - .0-cell-equiv-globular-equiv → id-equiv - .1-cell-globular-equiv-globular-equiv {x} {y} → - id-globular-equiv (1-cell-globular-type-Globular-Type A x y) +id-globular-equiv A = id-globular-map A , is-equiv-id-globular-map A ``` ### Composition of equivalences of globular types ```agda +is-equiv-comp-globular-map : + {l1 l2 l3 l4 l5 l6 : Level} + {A : Globular-Type l1 l2} + {B : Globular-Type l3 l4} + {C : Globular-Type l5 l6} + {g : globular-map B C} + {f : globular-map A B} → + is-equiv-globular-map g → + is-equiv-globular-map f → + is-equiv-globular-map (comp-globular-map g f) +is-equiv-0-cell-is-equiv-globular-map (is-equiv-comp-globular-map G F) = + is-equiv-comp _ _ + ( is-equiv-0-cell-is-equiv-globular-map F) + ( is-equiv-0-cell-is-equiv-globular-map G) +1-cell-is-equiv-globular-map (is-equiv-comp-globular-map G F) = + is-equiv-comp-globular-map + ( 1-cell-is-equiv-globular-map G) + ( 1-cell-is-equiv-globular-map F) + comp-globular-equiv : {l1 l2 l3 l4 l5 l6 : Level} {A : Globular-Type l1 l2} @@ -164,11 +228,10 @@ comp-globular-equiv : {C : Globular-Type l5 l6} → globular-equiv B C → globular-equiv A B → globular-equiv A C comp-globular-equiv g f = - λ where - .0-cell-equiv-globular-equiv → - 0-cell-equiv-globular-equiv g ∘e 0-cell-equiv-globular-equiv f - .1-cell-globular-equiv-globular-equiv → - comp-globular-equiv - ( 1-cell-globular-equiv-globular-equiv g) - ( 1-cell-globular-equiv-globular-equiv f) + comp-globular-map + ( globular-map-globular-equiv g) + ( globular-map-globular-equiv f) , + is-equiv-comp-globular-map + ( is-equiv-globular-equiv g) + ( is-equiv-globular-equiv f) ``` diff --git a/src/globular-types/globular-maps.lagda.md b/src/globular-types/globular-maps.lagda.md index 4cdc042698..7c56f702f1 100644 --- a/src/globular-types/globular-maps.lagda.md +++ b/src/globular-types/globular-maps.lagda.md @@ -157,3 +157,8 @@ comp-globular-map g f = ( 1-cell-globular-map-globular-map g) ( 1-cell-globular-map-globular-map f) ``` + +## See also + +- The dependent counterpart to globular maps is + [sections of dependent globular types](type-theories.sections-dependent-globular-types.md) diff --git a/src/globular-types/homotopies-globular-maps.lagda.md b/src/globular-types/homotopies-globular-maps.lagda.md new file mode 100644 index 0000000000..be9d5d563c --- /dev/null +++ b/src/globular-types/homotopies-globular-maps.lagda.md @@ -0,0 +1,181 @@ +# Homotopies of maps between globular types + +```agda +{-# OPTIONS --guardedness #-} + +module globular-types.homotopies-globular-maps where +``` + +
Imports + +```agda +open import foundation.action-on-identifications-functions +open import foundation.dependent-identifications +open import foundation.dependent-pair-types +open import foundation.function-types +open import foundation.homotopies +open import foundation.identity-types +open import foundation.transport-along-pairs-of-identifications +open import foundation.universe-levels +open import foundation.whiskering-homotopies-composition + +open import globular-types.globular-equivalences +open import globular-types.globular-maps +open import globular-types.globular-types +``` + +
+ +## Idea + +A +{{#concept "homotopy" Disambiguation="of globular maps of globular types" Agda=htpy-globular-map}} +`f ~ g` is a homotopy `H₀ : f₀ ~ g₀` together with a family of equivalences + +```text + A₁ x y + / \ + / \ + / \ + ∨ ∨ + B₁ (f₀ x) (f₀ y) ---> B₁ (g₀ x) (g₀ y) + tr-htpy B H +``` + +## Definitions + +### Homotopies of maps between globular types + +```agda +tr-pair-globular-map : + {l1 l2 l3 l4 : Level} + {A : UU l1} {B : UU l2} + (C : A → B → Globular-Type l3 l4) → + {x y : A} (p : x ＝ y) {x' : B} {y' : B} (q : x' ＝ y') → + globular-map (C x x') (C y y') +tr-pair-globular-map C {x} refl {x'} refl = id-globular-map (C x x') + +module _ + {l1 l2 l3 l4 : Level} + {A : UU l1} {B : UU l2} + (C : A → B → Globular-Type l3 l4) + where + + compute-0-cell-tr-pair-globular-map : + {x y : A} (p : x ＝ y) {x' : B} {y' : B} (q : x' ＝ y') → + tr-pair' (λ u v → 0-cell-Globular-Type (C u v)) p q ~ + 0-cell-globular-map (tr-pair-globular-map C p q) + compute-0-cell-tr-pair-globular-map refl refl = refl-htpy + +record + htpy-globular-map + {l1 l2 l3 l4 : Level} {A : Globular-Type l1 l2} {B : Globular-Type l3 l4} + (f g : globular-map A B) : + UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) + where + coinductive + field + 0-cell-htpy-globular-map : + 0-cell-globular-map f ~ 0-cell-globular-map g + + 1-cell-htpy-globular-map-htpy-globular-map : + {x y : 0-cell-Globular-Type A} → + htpy-globular-map + ( comp-globular-map + ( tr-pair-globular-map + ( 1-cell-globular-type-Globular-Type B) + ( 0-cell-htpy-globular-map x) + ( 0-cell-htpy-globular-map y)) + ( 1-cell-globular-map-globular-map f {x} {y})) + ( 1-cell-globular-map-globular-map g {x} {y}) + +open htpy-globular-map public + +module _ + {l1 l2 l3 l4 : Level} + {A : Globular-Type l1 l2} {B : Globular-Type l3 l4} + (f g : globular-map A B) + where + + 1-cell-htpy-globular-map : + (H : htpy-globular-map f g) → + {x y : 0-cell-Globular-Type A} → + tr-pair' + ( 1-cell-Globular-Type B) + ( 0-cell-htpy-globular-map H x) + ( 0-cell-htpy-globular-map H y) ∘ + 1-cell-globular-map f {x} {y} ~ + 1-cell-globular-map g {x} {y} + 1-cell-htpy-globular-map H {x} {y} = + ( ( compute-0-cell-tr-pair-globular-map + ( 1-cell-globular-type-Globular-Type B) + ( 0-cell-htpy-globular-map H x) + ( 0-cell-htpy-globular-map H y)) ·r + ( 0-cell-globular-map (1-cell-globular-map-globular-map f))) ∙h + ( 0-cell-htpy-globular-map (1-cell-htpy-globular-map-htpy-globular-map H)) +``` + +### The concatenation of homotopies of globular maps + +```agda +-- concat-htpy-globular-map : +-- {l1 l2 l3 l4 : Level} +-- {A : Globular-Type l1 l2} {B : Globular-Type l3 l4} +-- {f g h : globular-map A B} → +-- htpy-globular-map f g → +-- htpy-globular-map g h → +-- htpy-globular-map f h +-- 0-cell-htpy-globular-map (concat-htpy-globular-map H K) = +-- 0-cell-htpy-globular-map H ∙h +-- 0-cell-htpy-globular-map K +-- 1-cell-htpy-globular-map-htpy-globular-map (concat-htpy-globular-map H K) = +-- concat-htpy-globular-map +-- {! !} +-- ( concat-htpy-globular-map +-- {! 1-cell-htpy-globular-map-htpy-globular-map H !} +-- ( 1-cell-htpy-globular-map-htpy-globular-map K)) +``` + +### The right unit law of globular map composition + +```agda +-- left-unit-law-htpy-globular-map : +-- {l1 l2 l3 l4 : Level} +-- {A : Globular-Type l1 l2} {B : Globular-Type l3 l4} (f : globular-map A B) → +-- htpy-globular-map (comp-globular-map (id-globular-map B) f) f +-- 0-cell-htpy-globular-map (left-unit-law-htpy-globular-map f) = refl-htpy +-- 1-cell-htpy-globular-map-htpy-globular-map (left-unit-law-htpy-globular-map f) = +-- concat-htpy-globular-map +-- {! !} +-- ( left-unit-law-htpy-globular-map (1-cell-globular-map-globular-map f)) +``` + +### The reflexivity homotopy on a globular map + +```text +refl-htpy-globular-map : + {l1 l2 l3 l4 : Level} {A : Globular-Type l1 l2} {B : Globular-Type l3 l4} → + (f : globular-map A B) → htpy-globular-map f f +0-cell-htpy-globular-map (refl-htpy-globular-map f) = refl-htpy +1-cell-htpy-globular-map-htpy-globular-map (refl-htpy-globular-map f) = + left-unit-law-htpy-globular-map (1-cell-globular-map-globular-map f) +``` + +### Composition of maps of globular types + +```text +comp-globular-map : + {l1 l2 l3 l4 l5 l6 : Level} + {A : Globular-Type l1 l2} + {B : Globular-Type l3 l4} + {C : Globular-Type l5 l6} → + globular-map B C → globular-map A B → globular-map A C +comp-globular-map g f = + λ where + .0-cell-globular-map → + 0-cell-globular-map g ∘ 0-cell-globular-map f + .1-cell-globular-map-globular-map → + comp-globular-map + ( 1-cell-globular-map-globular-map g) + ( 1-cell-globular-map-globular-map f) +``` diff --git a/src/globular-types/points-globular-types.lagda.md b/src/globular-types/points-globular-types.lagda.md index 94e81c6f56..fa008006f2 100644 --- a/src/globular-types/points-globular-types.lagda.md +++ b/src/globular-types/points-globular-types.lagda.md @@ -53,7 +53,7 @@ open point-Globular-Type public 1-cell-point-Globular-Type : {l1 l2 : Level} (G : Globular-Type l1 l2) (x : point-Globular-Type G) → 1-cell-Globular-Type G - (0-cell-point-Globular-Type x) + ( 0-cell-point-Globular-Type x) ( 0-cell-point-Globular-Type x) 1-cell-point-Globular-Type G x = 0-cell-point-Globular-Type (1-cell-point-point-Globular-Type x) diff --git a/src/globular-types/reflexive-globular-equivalences.lagda.md b/src/globular-types/reflexive-globular-equivalences.lagda.md index 8d154f39af..27a6655106 100644 --- a/src/globular-types/reflexive-globular-equivalences.lagda.md +++ b/src/globular-types/reflexive-globular-equivalences.lagda.md @@ -72,12 +72,12 @@ record 0-cell-equiv-reflexive-globular-equiv : 0-cell-Reflexive-Globular-Type G ≃ 0-cell-Reflexive-Globular-Type H 0-cell-equiv-reflexive-globular-equiv = - 0-cell-equiv-globular-equiv globular-equiv-reflexive-globular-equiv + 0-cell-globular-equiv globular-equiv-reflexive-globular-equiv 0-cell-reflexive-globular-equiv : 0-cell-Reflexive-Globular-Type G → 0-cell-Reflexive-Globular-Type H 0-cell-reflexive-globular-equiv = - 0-cell-globular-equiv globular-equiv-reflexive-globular-equiv + 0-cell-map-globular-equiv globular-equiv-reflexive-globular-equiv 1-cell-equiv-reflexive-globular-equiv : {x y : 0-cell-Reflexive-Globular-Type G} → @@ -95,7 +95,7 @@ record ( 0-cell-reflexive-globular-equiv x) ( 0-cell-reflexive-globular-equiv y) 1-cell-reflexive-globular-equiv = - 1-cell-globular-equiv globular-equiv-reflexive-globular-equiv + 1-cell-map-globular-equiv globular-equiv-reflexive-globular-equiv 1-cell-globular-equiv-reflexive-globular-equiv : {x y : 0-cell-Reflexive-Globular-Type G} → diff --git a/src/wild-category-theory.lagda.md b/src/wild-category-theory.lagda.md index 63cf266e2d..501bb2b25e 100644 --- a/src/wild-category-theory.lagda.md +++ b/src/wild-category-theory.lagda.md @@ -15,10 +15,17 @@ 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.idempotent-points-noncoherent-omega-semiprecategories 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-omega-semiprecategories public open import wild-category-theory.maps-noncoherent-wild-higher-precategories public +open import wild-category-theory.neutral-morphisms-noncoherent-omega-semiprecategories public open import wild-category-theory.noncoherent-large-wild-higher-precategories public +open import wild-category-theory.noncoherent-omega-semiprecategories public open import wild-category-theory.noncoherent-wild-higher-precategories public +open import wild-category-theory.postcomposition-morphisms-noncoherent-omega-semiprecategories public +open import wild-category-theory.precomposition-morphisms-noncoherent-omega-semiprecategories public +open import wild-category-theory.universal-property-isomorphisms-noncoherent-omega-semiprecategories public ``` diff --git a/src/wild-category-theory/idempotent-points-noncoherent-omega-semiprecategories.lagda.md b/src/wild-category-theory/idempotent-points-noncoherent-omega-semiprecategories.lagda.md new file mode 100644 index 0000000000..9fdf07a543 --- /dev/null +++ b/src/wild-category-theory/idempotent-points-noncoherent-omega-semiprecategories.lagda.md @@ -0,0 +1,71 @@ +# Idempotent points in noncoherent ω-semiprecategories + +```agda +{-# OPTIONS --guardedness #-} + +module wild-category-theory.idempotent-points-noncoherent-omega-semiprecategories where +``` + +
Imports + +```agda +open import foundation.cartesian-product-types +open import foundation.dependent-pair-types +open import foundation.identity-types +open import foundation.universe-levels + +open import globular-types.binary-globular-maps +open import globular-types.composition-structure-globular-types +open import globular-types.globular-equivalences +open import globular-types.globular-types +open import globular-types.points-globular-types + +open import wild-category-theory.maps-noncoherent-omega-semiprecategories +open import wild-category-theory.noncoherent-omega-semiprecategories +open import wild-category-theory.postcomposition-morphisms-noncoherent-omega-semiprecategories +open import wild-category-theory.precomposition-morphisms-noncoherent-omega-semiprecategories +``` + +
+ +## Idea + +We say a [point](globular-types.points-globular-types.md) `x` in a +[noncoherent ω-semiprecategory](wild-category-theory.noncoherent-omega-semiprecategories.md) +`𝒞` is +{{#concept "idempotent" Disambiguation="point in a noncoherent ω-semiprecategory" Agda=is-idempotent-obj-Noncoherent-ω-Semiprecategory}} +if the equipped endomorphism `f : 𝒞₁ x x` satisfies the law `f ∘ f = f`, and is +again idempotent as a point of the hom-ω-semiprecategory. + +## Definitions + +### Idempotent points + +```agda +record + is-idempotent-point-Noncoherent-ω-Semiprecategory + {l1 l2 : Level} (𝒞 : Noncoherent-ω-Semiprecategory l1 l2) + (x : point-Globular-Type (globular-type-Noncoherent-ω-Semiprecategory 𝒞)) : + UU l2 + where + coinductive + field + is-idempotent-endo-Noncoherent-ω-Semiprecategory : + comp-hom-Noncoherent-ω-Semiprecategory 𝒞 + ( 1-cell-point-Globular-Type + ( globular-type-Noncoherent-ω-Semiprecategory 𝒞) + ( x)) + ( 1-cell-point-Globular-Type + ( globular-type-Noncoherent-ω-Semiprecategory 𝒞) + ( x)) ＝ + 1-cell-point-Globular-Type + ( globular-type-Noncoherent-ω-Semiprecategory 𝒞) + ( x) + + is-idempotent-hom-point-point-Noncoherent-ω-Semiprecategory : + is-idempotent-point-Noncoherent-ω-Semiprecategory + ( hom-noncoherent-ω-semiprecategory-Noncoherent-ω-Semiprecategory 𝒞 + ( 0-cell-point-Globular-Type x) + ( 0-cell-point-Globular-Type x)) + ( 1-cell-point-point-Globular-Type x) +``` diff --git a/src/wild-category-theory/maps-noncoherent-omega-semiprecategories.lagda.md b/src/wild-category-theory/maps-noncoherent-omega-semiprecategories.lagda.md new file mode 100644 index 0000000000..ef7695f9f3 --- /dev/null +++ b/src/wild-category-theory/maps-noncoherent-omega-semiprecategories.lagda.md @@ -0,0 +1,151 @@ +# Maps between noncoherent ω-semiprecategories + +```agda +{-# OPTIONS --guardedness #-} + +module wild-category-theory.maps-noncoherent-omega-semiprecategories 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-semiprecategories +``` + +
+ +## Idea + +A +{{#concept "map" Disambiguation="between noncoherent ω-semiprecategories" Agda=map-Noncoherent-ω-Semiprecategory}} +`f` between +[noncoherent ω-semiprecategories](wild-category-theory.noncoherent-omega-semiprecategories.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 ω-semiprecategories 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 ω-semiprecategories 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 ω-semiprecategories. For a notion of +"morphism" between noncoherent ω-semiprecategories that in one sense preserves +this additional structure, see +[colax functors between noncoherent ω-semiprecategories](wild-category-theory.colax-functors-noncoherent-omega-semiprecategories.md). + +## Definitions + +### Maps between noncoherent ω-semiprecategories + +```agda +map-Noncoherent-ω-Semiprecategory : + {l1 l2 l3 l4 : Level} + (𝒜 : Noncoherent-ω-Semiprecategory l1 l2) + (ℬ : Noncoherent-ω-Semiprecategory l3 l4) → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) +map-Noncoherent-ω-Semiprecategory 𝒜 ℬ = + globular-map + ( globular-type-Noncoherent-ω-Semiprecategory 𝒜) + ( globular-type-Noncoherent-ω-Semiprecategory ℬ) + +module _ + {l1 l2 l3 l4 : Level} + (𝒜 : Noncoherent-ω-Semiprecategory l1 l2) + (ℬ : Noncoherent-ω-Semiprecategory l3 l4) + (F : map-Noncoherent-ω-Semiprecategory 𝒜 ℬ) + where + + obj-map-Noncoherent-ω-Semiprecategory : + obj-Noncoherent-ω-Semiprecategory 𝒜 → + obj-Noncoherent-ω-Semiprecategory ℬ + obj-map-Noncoherent-ω-Semiprecategory = + 0-cell-globular-map F + + hom-globular-map-map-Noncoherent-ω-Semiprecategory : + {x y : obj-Noncoherent-ω-Semiprecategory 𝒜} → + globular-map + ( hom-globular-type-Noncoherent-ω-Semiprecategory 𝒜 x y) + ( hom-globular-type-Noncoherent-ω-Semiprecategory ℬ + ( obj-map-Noncoherent-ω-Semiprecategory x) + ( obj-map-Noncoherent-ω-Semiprecategory y)) + hom-globular-map-map-Noncoherent-ω-Semiprecategory = + 1-cell-globular-map-globular-map F + + hom-map-Noncoherent-ω-Semiprecategory : + {x y : obj-Noncoherent-ω-Semiprecategory 𝒜} → + hom-Noncoherent-ω-Semiprecategory 𝒜 x y → + hom-Noncoherent-ω-Semiprecategory ℬ + ( obj-map-Noncoherent-ω-Semiprecategory x) + ( obj-map-Noncoherent-ω-Semiprecategory y) + hom-map-Noncoherent-ω-Semiprecategory = + 0-cell-globular-map + ( hom-globular-map-map-Noncoherent-ω-Semiprecategory) + + 2-hom-map-Noncoherent-ω-Semiprecategory : + {x y : obj-Noncoherent-ω-Semiprecategory 𝒜} + {f g : hom-Noncoherent-ω-Semiprecategory 𝒜 x y} → + 2-hom-Noncoherent-ω-Semiprecategory 𝒜 f g → + 2-hom-Noncoherent-ω-Semiprecategory ℬ + ( hom-map-Noncoherent-ω-Semiprecategory f) + ( hom-map-Noncoherent-ω-Semiprecategory g) + 2-hom-map-Noncoherent-ω-Semiprecategory = + 1-cell-globular-map + ( hom-globular-map-map-Noncoherent-ω-Semiprecategory) + + hom-noncoherent-ω-semiprecategory-map-Noncoherent-ω-Semiprecategory : + (x y : obj-Noncoherent-ω-Semiprecategory 𝒜) → + map-Noncoherent-ω-Semiprecategory + ( hom-noncoherent-ω-semiprecategory-Noncoherent-ω-Semiprecategory + ( 𝒜) + ( x) + ( y)) + ( hom-noncoherent-ω-semiprecategory-Noncoherent-ω-Semiprecategory + ( ℬ) + ( obj-map-Noncoherent-ω-Semiprecategory x) + ( obj-map-Noncoherent-ω-Semiprecategory y)) + hom-noncoherent-ω-semiprecategory-map-Noncoherent-ω-Semiprecategory + x y = + 1-cell-globular-map-globular-map F +``` + +### The identity map on a noncoherent ω-semiprecategory + +```agda +module _ + {l1 l2 : Level} (𝒜 : Noncoherent-ω-Semiprecategory l1 l2) + where + + id-map-Noncoherent-ω-Semiprecategory : + map-Noncoherent-ω-Semiprecategory 𝒜 𝒜 + id-map-Noncoherent-ω-Semiprecategory = + id-globular-map _ +``` + +### Composition of maps between noncoherent ω-semiprecategories + +```agda +module _ + {l1 l2 l3 l4 l5 l6 : Level} + (𝒜 : Noncoherent-ω-Semiprecategory l1 l2) + (ℬ : Noncoherent-ω-Semiprecategory l3 l4) + (𝒞 : Noncoherent-ω-Semiprecategory l5 l6) + (G : map-Noncoherent-ω-Semiprecategory ℬ 𝒞) + (F : map-Noncoherent-ω-Semiprecategory 𝒜 ℬ) + where + + comp-map-Noncoherent-ω-Semiprecategory : + map-Noncoherent-ω-Semiprecategory 𝒜 𝒞 + comp-map-Noncoherent-ω-Semiprecategory = + comp-globular-map G F +``` diff --git a/src/wild-category-theory/neutral-morphisms-noncoherent-omega-semiprecategories.lagda.md b/src/wild-category-theory/neutral-morphisms-noncoherent-omega-semiprecategories.lagda.md new file mode 100644 index 0000000000..f8179a2c72 --- /dev/null +++ b/src/wild-category-theory/neutral-morphisms-noncoherent-omega-semiprecategories.lagda.md @@ -0,0 +1,92 @@ +# Neutral points in noncoherent ω-semiprecategories + +```agda +{-# OPTIONS --guardedness --allow-unsolved-metas #-} + +module wild-category-theory.neutral-morphisms-noncoherent-omega-semiprecategories where +``` + +
Imports + +```agda +open import foundation.cartesian-product-types +open import foundation.dependent-pair-types +open import foundation.identity-types +open import foundation.universe-levels + +open import globular-types.binary-globular-maps +open import globular-types.composition-structure-globular-types +open import globular-types.globular-equivalences +open import globular-types.globular-maps +open import globular-types.globular-types +open import globular-types.homotopies-globular-maps +open import globular-types.points-globular-types + +open import wild-category-theory.maps-noncoherent-omega-semiprecategories +open import wild-category-theory.noncoherent-omega-semiprecategories +open import wild-category-theory.postcomposition-morphisms-noncoherent-omega-semiprecategories +open import wild-category-theory.precomposition-morphisms-noncoherent-omega-semiprecategories +``` + +
+ +## Idea + +We say a point `x` in a +[noncoherent ω-semiprecategory](wild-category-theory.noncoherent-omega-semiprecategories.md) +`𝒞` is +{{#concept "neutral" Disambiguation="point in a noncoherent ω-semiprecategory" Agda=is-neutral-point-Noncoherent-ω-Semiprecategory}} +if the precomposition and postcomposition globular maps at the distinguished +endomorphism `f : 𝒞₁ x x` are homotopic to identity maps. + +## Definitions + +### Right neutral points + +```agda +is-right-neutral-point-Noncoherent-ω-Semiprecategory : + {l1 l2 : Level} (𝒞 : Noncoherent-ω-Semiprecategory l1 l2) + (x : point-Globular-Type (globular-type-Noncoherent-ω-Semiprecategory 𝒞)) → + UU (l1 ⊔ l2) +is-right-neutral-point-Noncoherent-ω-Semiprecategory 𝒞 x = + (z : obj-Noncoherent-ω-Semiprecategory 𝒞) → + htpy-globular-map + ( precomp-globular-map-hom-Noncoherent-ω-Semiprecategory 𝒞 + ( 1-cell-point-point-Globular-Type x) + ( z)) + ( id-globular-map + ( hom-globular-type-Noncoherent-ω-Semiprecategory 𝒞 + ( 0-cell-point-Globular-Type x) + ( z))) +``` + +### Left neutral points + +```agda +is-left-neutral-point-Noncoherent-ω-Semiprecategory : + {l1 l2 : Level} (𝒞 : Noncoherent-ω-Semiprecategory l1 l2) + (x : point-Globular-Type (globular-type-Noncoherent-ω-Semiprecategory 𝒞)) → + UU (l1 ⊔ l2) +is-left-neutral-point-Noncoherent-ω-Semiprecategory 𝒞 x = + (z : obj-Noncoherent-ω-Semiprecategory 𝒞) → + htpy-globular-map + ( postcomp-globular-map-hom-Noncoherent-ω-Semiprecategory 𝒞 + ( 1-cell-point-point-Globular-Type x) + ( z)) + ( id-globular-map + ( hom-globular-type-Noncoherent-ω-Semiprecategory 𝒞 + ( z) + ( 0-cell-point-Globular-Type x))) +``` + +### Right neutral points + +```agda +is-neutral-point-Noncoherent-ω-Semiprecategory : + {l1 l2 : Level} (𝒞 : Noncoherent-ω-Semiprecategory l1 l2) + (x : point-Globular-Type (globular-type-Noncoherent-ω-Semiprecategory 𝒞)) → + UU (l1 ⊔ l2) +is-neutral-point-Noncoherent-ω-Semiprecategory 𝒞 x = + ( is-right-neutral-point-Noncoherent-ω-Semiprecategory 𝒞 x) × + ( is-left-neutral-point-Noncoherent-ω-Semiprecategory 𝒞 x) +``` diff --git a/src/wild-category-theory/noncoherent-omega-semiprecategories.lagda.md b/src/wild-category-theory/noncoherent-omega-semiprecategories.lagda.md new file mode 100644 index 0000000000..0d9dc41490 --- /dev/null +++ b/src/wild-category-theory/noncoherent-omega-semiprecategories.lagda.md @@ -0,0 +1,238 @@ +# Noncoherent ω-semiprecategories + +```agda +{-# OPTIONS --guardedness #-} + +module wild-category-theory.noncoherent-omega-semiprecategories where +``` + +
Imports + +```agda +open import foundation.dependent-pair-types +open import foundation.universe-levels + +open import globular-types.binary-globular-maps +open import globular-types.composition-structure-globular-types +open import globular-types.globular-types +``` + +
+ +## Idea + +A +{{#concept "noncoherent ω-semiprecategory" Agda=Noncoherent-ω-Semiprecategory}} +`𝒞` is a [globular type](globular-types.globular-types.md) `G` +[equipped](foundation.structure.md) with a +[composition structure](globular-types.composition-structure-globular-types.md). +It comes equipped with a type of objects `𝒞₀` such that for every pair of +objects `x y : 𝒞₀` there is a type of _morphisms_ `𝒞₁ x y`, in fact, a +noncoherent ω-semiprecategory of morphisms. For every pair of morphisms +`g : 𝒞₁ y z` and `f : 𝒞₁ x y` there is a morphism `g ∘ f : 𝒞₁ x z`, and a +noncoherent ω-semiprecategory also comes equipped with horizontal composition +operations on its higher morphisms. + +## Definitions + +### Noncoherent ω-semiprecategories + +```agda +Noncoherent-ω-Semiprecategory : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2) +Noncoherent-ω-Semiprecategory l1 l2 = + Σ (Globular-Type l1 l2) (composition-Globular-Type) +``` + +```agda +module _ + {l1 l2 : Level} (𝒞 : Noncoherent-ω-Semiprecategory l1 l2) + where + + globular-type-Noncoherent-ω-Semiprecategory : Globular-Type l1 l2 + globular-type-Noncoherent-ω-Semiprecategory = pr1 𝒞 + + obj-Noncoherent-ω-Semiprecategory : UU l1 + obj-Noncoherent-ω-Semiprecategory = + 0-cell-Globular-Type globular-type-Noncoherent-ω-Semiprecategory +``` + +Morphisms in a noncoherent ω-semiprecategory: + +```agda + hom-globular-type-Noncoherent-ω-Semiprecategory : + (x y : obj-Noncoherent-ω-Semiprecategory) → Globular-Type l2 l2 + hom-globular-type-Noncoherent-ω-Semiprecategory = + 1-cell-globular-type-Globular-Type + globular-type-Noncoherent-ω-Semiprecategory + + hom-Noncoherent-ω-Semiprecategory : + (x y : obj-Noncoherent-ω-Semiprecategory) → UU l2 + hom-Noncoherent-ω-Semiprecategory = + 1-cell-Globular-Type globular-type-Noncoherent-ω-Semiprecategory +``` + +Composition in a noncoherent ω-semiprecategory: + +```agda + composition-Noncoherent-ω-Semiprecategory : + composition-Globular-Type globular-type-Noncoherent-ω-Semiprecategory + composition-Noncoherent-ω-Semiprecategory = pr2 𝒞 + + comp-binary-globular-map-hom-Noncoherent-ω-Semiprecategory : + {x y z : obj-Noncoherent-ω-Semiprecategory} → + binary-globular-map + ( hom-globular-type-Noncoherent-ω-Semiprecategory y z) + ( hom-globular-type-Noncoherent-ω-Semiprecategory x y) + ( hom-globular-type-Noncoherent-ω-Semiprecategory x z) + comp-binary-globular-map-hom-Noncoherent-ω-Semiprecategory = + comp-binary-globular-map-composition-Globular-Type + composition-Noncoherent-ω-Semiprecategory + + comp-hom-Noncoherent-ω-Semiprecategory : + {x y z : obj-Noncoherent-ω-Semiprecategory} → + hom-Noncoherent-ω-Semiprecategory y z → + hom-Noncoherent-ω-Semiprecategory x y → + hom-Noncoherent-ω-Semiprecategory x z + comp-hom-Noncoherent-ω-Semiprecategory = + comp-1-cell-composition-Globular-Type + composition-Noncoherent-ω-Semiprecategory + + composition-hom-Noncoherent-ω-Semiprecategory : + {x y : obj-Noncoherent-ω-Semiprecategory} → + composition-Globular-Type + ( hom-globular-type-Noncoherent-ω-Semiprecategory x y) + composition-hom-Noncoherent-ω-Semiprecategory = + composition-1-cell-globular-type-Globular-Type + composition-Noncoherent-ω-Semiprecategory +``` + +The noncoherent ω-semiprecategory of morphisms between two objects in a +noncoherent ω-semiprecategory: + +```agda + hom-noncoherent-ω-semiprecategory-Noncoherent-ω-Semiprecategory : + (x y : obj-Noncoherent-ω-Semiprecategory) → + Noncoherent-ω-Semiprecategory l2 l2 + hom-noncoherent-ω-semiprecategory-Noncoherent-ω-Semiprecategory x y = + hom-globular-type-Noncoherent-ω-Semiprecategory x y , + composition-hom-Noncoherent-ω-Semiprecategory +``` + +2-Morphisms in a noncoherent ω-semiprecategory: + +```agda + 2-hom-globular-type-Noncoherent-ω-Semiprecategory : + {x y : obj-Noncoherent-ω-Semiprecategory} + (f g : hom-Noncoherent-ω-Semiprecategory x y) → Globular-Type l2 l2 + 2-hom-globular-type-Noncoherent-ω-Semiprecategory = + 2-cell-globular-type-Globular-Type + globular-type-Noncoherent-ω-Semiprecategory + + 2-hom-Noncoherent-ω-Semiprecategory : + {x y : obj-Noncoherent-ω-Semiprecategory} + (f g : hom-Noncoherent-ω-Semiprecategory x y) → UU l2 + 2-hom-Noncoherent-ω-Semiprecategory = + 2-cell-Globular-Type globular-type-Noncoherent-ω-Semiprecategory + + comp-2-hom-Noncoherent-ω-Semiprecategory : + {x y : obj-Noncoherent-ω-Semiprecategory} + {f g h : hom-Noncoherent-ω-Semiprecategory x y} → + 2-hom-Noncoherent-ω-Semiprecategory g h → + 2-hom-Noncoherent-ω-Semiprecategory f g → + 2-hom-Noncoherent-ω-Semiprecategory f h + comp-2-hom-Noncoherent-ω-Semiprecategory = + comp-2-cell-composition-Globular-Type + composition-Noncoherent-ω-Semiprecategory + + composition-2-hom-Noncoherent-ω-Semiprecategory : + {x y : obj-Noncoherent-ω-Semiprecategory} + {f g : hom-Noncoherent-ω-Semiprecategory x y} → + composition-Globular-Type + ( 2-hom-globular-type-Noncoherent-ω-Semiprecategory f g) + composition-2-hom-Noncoherent-ω-Semiprecategory = + composition-1-cell-globular-type-Globular-Type + composition-hom-Noncoherent-ω-Semiprecategory + + 2-hom-noncoherent-ω-semiprecategory-Noncoherent-ω-Semiprecategory : + {x y : obj-Noncoherent-ω-Semiprecategory} + (f g : hom-Noncoherent-ω-Semiprecategory x y) → + Noncoherent-ω-Semiprecategory l2 l2 + 2-hom-noncoherent-ω-semiprecategory-Noncoherent-ω-Semiprecategory f g = + 2-hom-globular-type-Noncoherent-ω-Semiprecategory f g , + composition-2-hom-Noncoherent-ω-Semiprecategory + + horizontal-comp-2-hom-Noncoherent-ω-Semiprecategory : + {x y z : obj-Noncoherent-ω-Semiprecategory} → + {g g' : hom-Noncoherent-ω-Semiprecategory y z} + {f f' : hom-Noncoherent-ω-Semiprecategory x y} → + 2-hom-Noncoherent-ω-Semiprecategory g g' → + 2-hom-Noncoherent-ω-Semiprecategory f f' → + 2-hom-Noncoherent-ω-Semiprecategory + ( comp-hom-Noncoherent-ω-Semiprecategory g f) + ( comp-hom-Noncoherent-ω-Semiprecategory g' f') + horizontal-comp-2-hom-Noncoherent-ω-Semiprecategory = + horizontal-comp-2-cell-composition-Globular-Type + composition-Noncoherent-ω-Semiprecategory +``` + +Higher morphisms in a noncoherent ω-semiprecategory: + +```agda + 3-hom-globular-type-Noncoherent-ω-Semiprecategory : + {x y : obj-Noncoherent-ω-Semiprecategory} + {f g : hom-Noncoherent-ω-Semiprecategory x y} + (α β : 2-hom-Noncoherent-ω-Semiprecategory f g) → Globular-Type l2 l2 + 3-hom-globular-type-Noncoherent-ω-Semiprecategory = + 3-cell-globular-type-Globular-Type + globular-type-Noncoherent-ω-Semiprecategory + + 3-hom-Noncoherent-ω-Semiprecategory : + {x y : obj-Noncoherent-ω-Semiprecategory} + {f g : hom-Noncoherent-ω-Semiprecategory x y} + (α β : 2-hom-Noncoherent-ω-Semiprecategory f g) → UU l2 + 3-hom-Noncoherent-ω-Semiprecategory = + 3-cell-Globular-Type globular-type-Noncoherent-ω-Semiprecategory + + comp-3-hom-Noncoherent-ω-Semiprecategory : + {x y : obj-Noncoherent-ω-Semiprecategory} + {f g : hom-Noncoherent-ω-Semiprecategory x y} + {α β γ : 2-hom-Noncoherent-ω-Semiprecategory f g} → + 3-hom-Noncoherent-ω-Semiprecategory β γ → + 3-hom-Noncoherent-ω-Semiprecategory α β → + 3-hom-Noncoherent-ω-Semiprecategory α γ + comp-3-hom-Noncoherent-ω-Semiprecategory = + comp-3-cell-composition-Globular-Type + composition-Noncoherent-ω-Semiprecategory + + horizontal-comp-3-hom-Noncoherent-ω-Semiprecategory : + {x y z : obj-Noncoherent-ω-Semiprecategory} + {g g' : hom-Noncoherent-ω-Semiprecategory y z} + {f f' : hom-Noncoherent-ω-Semiprecategory x y} + {α α' : 2-hom-Noncoherent-ω-Semiprecategory g g'} + {β β' : 2-hom-Noncoherent-ω-Semiprecategory f f'} → + 3-hom-Noncoherent-ω-Semiprecategory α α' → + 3-hom-Noncoherent-ω-Semiprecategory β β' → + 3-hom-Noncoherent-ω-Semiprecategory + ( horizontal-comp-2-hom-Noncoherent-ω-Semiprecategory α β) + ( horizontal-comp-2-hom-Noncoherent-ω-Semiprecategory α' β') + horizontal-comp-3-hom-Noncoherent-ω-Semiprecategory = + horizontal-comp-3-cell-composition-Globular-Type' + composition-Noncoherent-ω-Semiprecategory + + 4-hom-globular-type-Noncoherent-ω-Semiprecategory : + {x y : obj-Noncoherent-ω-Semiprecategory} + {f g : hom-Noncoherent-ω-Semiprecategory x y} + {α β : 2-hom-Noncoherent-ω-Semiprecategory f g} + (H K : 3-hom-Noncoherent-ω-Semiprecategory α β) → Globular-Type l2 l2 + 4-hom-globular-type-Noncoherent-ω-Semiprecategory = + 4-cell-globular-type-Globular-Type + globular-type-Noncoherent-ω-Semiprecategory + + 4-hom-Noncoherent-ω-Semiprecategory : + {x y : obj-Noncoherent-ω-Semiprecategory} + {f g : hom-Noncoherent-ω-Semiprecategory x y} + {α β : 2-hom-Noncoherent-ω-Semiprecategory f g} + (H K : 3-hom-Noncoherent-ω-Semiprecategory α β) → UU l2 + 4-hom-Noncoherent-ω-Semiprecategory = + 4-cell-Globular-Type globular-type-Noncoherent-ω-Semiprecategory +``` diff --git a/src/wild-category-theory/postcomposition-morphisms-noncoherent-omega-semiprecategories.lagda.md b/src/wild-category-theory/postcomposition-morphisms-noncoherent-omega-semiprecategories.lagda.md new file mode 100644 index 0000000000..9a23b5cb6d --- /dev/null +++ b/src/wild-category-theory/postcomposition-morphisms-noncoherent-omega-semiprecategories.lagda.md @@ -0,0 +1,62 @@ +# Postcomposition of morphisms in noncoherent ω-semiprecategories + +```agda +{-# OPTIONS --guardedness #-} + +module wild-category-theory.postcomposition-morphisms-noncoherent-omega-semiprecategories where +``` + +
Imports + +```agda +open import foundation.dependent-pair-types +open import foundation.universe-levels + +open import globular-types.binary-globular-maps +open import globular-types.composition-structure-globular-types +open import globular-types.globular-types +open import globular-types.points-globular-types + +open import wild-category-theory.maps-noncoherent-omega-semiprecategories +open import wild-category-theory.noncoherent-omega-semiprecategories +``` + +
+ +## Idea + +Given a morphism `f : 𝒞₁ x y` in a +[noncoherent ω-semiprecategory](wild-category-theory.noncoherent-omega-semiprecategories.md) +with the structure of a [point](globular-types.points-globular-types.md), then +we have a +{{#concept "postcomposition map" Disambiguation="noncoherent ω-semiprecategory"}} +on hom-ω-semicategories + +```text + - ∘ f : 𝒞₁ z x → 𝒞₁ z y +``` + +for every object `z`. + +## Definitions + +### The precomposition globular map + +```agda +module _ + {l1 l2 : Level} (𝒞 : Noncoherent-ω-Semiprecategory l1 l2) + {x y : obj-Noncoherent-ω-Semiprecategory 𝒞} + (f : + point-Globular-Type (hom-globular-type-Noncoherent-ω-Semiprecategory 𝒞 x y)) + where + + postcomp-globular-map-hom-Noncoherent-ω-Semiprecategory : + (z : obj-Noncoherent-ω-Semiprecategory 𝒞) → + map-Noncoherent-ω-Semiprecategory + ( hom-noncoherent-ω-semiprecategory-Noncoherent-ω-Semiprecategory 𝒞 z x) + ( hom-noncoherent-ω-semiprecategory-Noncoherent-ω-Semiprecategory 𝒞 z y) + postcomp-globular-map-hom-Noncoherent-ω-Semiprecategory z = + ev-left-binary-globular-map + ( comp-binary-globular-map-hom-Noncoherent-ω-Semiprecategory 𝒞) + ( f) +``` diff --git a/src/wild-category-theory/precomposition-morphisms-noncoherent-omega-semiprecategories.lagda.md b/src/wild-category-theory/precomposition-morphisms-noncoherent-omega-semiprecategories.lagda.md new file mode 100644 index 0000000000..9e496d135e --- /dev/null +++ b/src/wild-category-theory/precomposition-morphisms-noncoherent-omega-semiprecategories.lagda.md @@ -0,0 +1,62 @@ +# Precomposition of morphisms in noncoherent ω-semiprecategories + +```agda +{-# OPTIONS --guardedness #-} + +module wild-category-theory.precomposition-morphisms-noncoherent-omega-semiprecategories where +``` + +
Imports + +```agda +open import foundation.dependent-pair-types +open import foundation.universe-levels + +open import globular-types.binary-globular-maps +open import globular-types.composition-structure-globular-types +open import globular-types.globular-types +open import globular-types.points-globular-types + +open import wild-category-theory.maps-noncoherent-omega-semiprecategories +open import wild-category-theory.noncoherent-omega-semiprecategories +``` + +
+ +## Idea + +Given a morphism `f : 𝒞₁ x y` in a +[noncoherent ω-semiprecategory](wild-category-theory.noncoherent-omega-semiprecategories.md) +with the structure of a [point](globular-types.points-globular-types.md), then +we have a +{{#concept "precomposition map" Disambiguation="noncoherent ω-semiprecategory"}} +on hom-ω-semicategories + +```text + - ∘ f : 𝒞₁ y z → 𝒞₁ x z +``` + +for every object `z`. + +## Definitions + +### The precomposition globular map + +```agda +module _ + {l1 l2 : Level} (𝒞 : Noncoherent-ω-Semiprecategory l1 l2) + {x y : obj-Noncoherent-ω-Semiprecategory 𝒞} + (f : + point-Globular-Type (hom-globular-type-Noncoherent-ω-Semiprecategory 𝒞 x y)) + where + + precomp-globular-map-hom-Noncoherent-ω-Semiprecategory : + (z : obj-Noncoherent-ω-Semiprecategory 𝒞) → + map-Noncoherent-ω-Semiprecategory + ( hom-noncoherent-ω-semiprecategory-Noncoherent-ω-Semiprecategory 𝒞 y z) + ( hom-noncoherent-ω-semiprecategory-Noncoherent-ω-Semiprecategory 𝒞 x z) + precomp-globular-map-hom-Noncoherent-ω-Semiprecategory z = + ev-right-binary-globular-map + ( comp-binary-globular-map-hom-Noncoherent-ω-Semiprecategory 𝒞) + ( f) +``` diff --git a/src/wild-category-theory/universal-property-isomorphisms-noncoherent-omega-semiprecategories.lagda.md b/src/wild-category-theory/universal-property-isomorphisms-noncoherent-omega-semiprecategories.lagda.md new file mode 100644 index 0000000000..ae5d7bb7b7 --- /dev/null +++ b/src/wild-category-theory/universal-property-isomorphisms-noncoherent-omega-semiprecategories.lagda.md @@ -0,0 +1,64 @@ +# The universal property of isomorphisms in noncoherent ω-semiprecategories + +```agda +{-# OPTIONS --guardedness #-} + +module wild-category-theory.universal-property-isomorphisms-noncoherent-omega-semiprecategories where +``` + +
Imports + +```agda +open import foundation.cartesian-product-types +open import foundation.dependent-pair-types +open import foundation.universe-levels + +open import globular-types.binary-globular-maps +open import globular-types.composition-structure-globular-types +open import globular-types.globular-equivalences +open import globular-types.globular-types +open import globular-types.points-globular-types + +open import wild-category-theory.maps-noncoherent-omega-semiprecategories +open import wild-category-theory.noncoherent-omega-semiprecategories +open import wild-category-theory.postcomposition-morphisms-noncoherent-omega-semiprecategories +open import wild-category-theory.precomposition-morphisms-noncoherent-omega-semiprecategories +``` + +
+ +## Idea + +Given a morphism `f : 𝒞₁ x y` in a +[noncoherent ω-semiprecategory](wild-category-theory.noncoherent-omega-semiprecategories.md) +with the structure of a [point](globular-types.points-globular-types.md), then +`f` satisfies the +{{#concept "universal property of isomorphisms" Disambiguation="in a noncoherent ω-semiprecategory"}} +if +[precomposition](wild-category-theory.precomposition-morphisms-noncoherent-omega-semiprecategories.md) +and +[postcomposition](wild-category-theory.postcomposition-morphisms-noncoherent-omega-semiprecategories.md) +by `f` is a [globular equivalence](globular-types.globular-equivalences.md) for +every object `z`. + +## Definitions + +### The universal property of isomorphisms + +```agda +module _ + {l1 l2 : Level} {𝒞 : Noncoherent-ω-Semiprecategory l1 l2} + {x y : obj-Noncoherent-ω-Semiprecategory 𝒞} + (f : + point-Globular-Type (hom-globular-type-Noncoherent-ω-Semiprecategory 𝒞 x y)) + where + + universal-property-iso-Noncoherent-ω-Semiprecategory : UU (l1 ⊔ l2) + universal-property-iso-Noncoherent-ω-Semiprecategory = + ( (z : obj-Noncoherent-ω-Semiprecategory 𝒞) → + is-equiv-globular-map + ( precomp-globular-map-hom-Noncoherent-ω-Semiprecategory 𝒞 f z)) × + ( (z : obj-Noncoherent-ω-Semiprecategory 𝒞) → + is-equiv-globular-map + ( postcomp-globular-map-hom-Noncoherent-ω-Semiprecategory 𝒞 f z)) +```