From 738a7ebce61fa6907e93c96f2ac0adbd9e11e4d9 Mon Sep 17 00:00:00 2001 From: Mabel Najdovski Date: Thu, 28 Sep 2023 16:15:59 +0200 Subject: [PATCH 1/5] Add pullbacks in large precategories --- src/category-theory.lagda.md | 2 + ...omorphisms-in-large-precategories.lagda.md | 28 +++ .../pullbacks-in-large-precategories.lagda.md | 186 ++++++++++++++++++ .../pullbacks-in-precategories.lagda.md | 14 +- 4 files changed, 223 insertions(+), 7 deletions(-) create mode 100644 src/category-theory/pullbacks-in-large-precategories.lagda.md diff --git a/src/category-theory.lagda.md b/src/category-theory.lagda.md index f42fcba793..b382e46390 100644 --- a/src/category-theory.lagda.md +++ b/src/category-theory.lagda.md @@ -112,6 +112,7 @@ open import category-theory.pregroupoids public open import category-theory.presheaf-categories public open import category-theory.products-in-precategories public open import category-theory.products-of-precategories public +open import category-theory.pullbacks-in-large-precategories public open import category-theory.pullbacks-in-precategories public open import category-theory.representable-functors-categories public open import category-theory.representable-functors-large-precategories public @@ -119,6 +120,7 @@ open import category-theory.representable-functors-precategories public open import category-theory.representing-arrow-category public open import category-theory.sieves-in-categories public open import category-theory.slice-precategories public +open import category-theory.subobject-classifier-in-large-precategories public open import category-theory.subprecategories public open import category-theory.terminal-objects-precategories public open import category-theory.yoneda-lemma-categories public diff --git a/src/category-theory/monomorphisms-in-large-precategories.lagda.md b/src/category-theory/monomorphisms-in-large-precategories.lagda.md index e43fe859d6..870e70f7f1 100644 --- a/src/category-theory/monomorphisms-in-large-precategories.lagda.md +++ b/src/category-theory/monomorphisms-in-large-precategories.lagda.md @@ -11,6 +11,7 @@ open import category-theory.isomorphisms-in-large-precategories open import category-theory.large-precategories open import foundation.action-on-identifications-functions +open import foundation.dependent-pair-types open import foundation.embeddings open import foundation.equivalences open import foundation.identity-types @@ -51,6 +52,33 @@ module _ is-prop-type-Prop is-mono-prop-Large-Precategory ``` +## The type of monomorphisms in a large precategory + +```agda +module _ + {α : Level → Level} {β : Level → Level → Level} + (C : Large-Precategory α β) {l1 l2 : Level} (l3 : Level) + (X : obj-Large-Precategory C l1) (Y : obj-Large-Precategory C l2) + where + + mono-Large-Precategory : UU (α l3 ⊔ β l3 l1 ⊔ β l3 l2 ⊔ β l1 l2) + mono-Large-Precategory = + Σ + ( hom-Large-Precategory C X Y) + ( is-mono-Large-Precategory C l3 X Y) + + module _ + (f : mono-Large-Precategory) + where + + hom-mono-Large-Precategory : hom-Large-Precategory C X Y + hom-mono-Large-Precategory = pr1 f + + is-mono-mono-Large-Precategory : + is-mono-Large-Precategory C l3 X Y hom-mono-Large-Precategory + is-mono-mono-Large-Precategory = pr2 f +``` + ## Properties ### Isomorphisms are monomorphisms diff --git a/src/category-theory/pullbacks-in-large-precategories.lagda.md b/src/category-theory/pullbacks-in-large-precategories.lagda.md new file mode 100644 index 0000000000..fa350197d6 --- /dev/null +++ b/src/category-theory/pullbacks-in-large-precategories.lagda.md @@ -0,0 +1,186 @@ +# Pullbacks in large precategories + +```agda +module category-theory.pullbacks-in-large-precategories where +``` + +
Imports + +```agda +open import category-theory.large-precategories + +open import foundation.action-on-identifications-functions +open import foundation.cartesian-product-types +open import foundation.contractible-types +open import foundation.dependent-pair-types +open import foundation.identity-types +open import foundation.propositions +open import foundation.unique-existence +open import foundation.universe-levels +``` + +
+ +## Idea + +A pullback of two morphisms `f : hom y x` and `g : hom z x` in a category `C` +consists of: + +- an object `w` +- morphisms `p₁ : hom w y` and `p₂ : hom w z` such that +- `f ∘ p₁ = g ∘ p₂` together with the universal property that for every object + `w'` and pair of morphisms `p₁' : hom w' y` and `p₂' : hom w' z` such that + `f ∘ p₁' = g ∘ p₂'` there exists a unique morphism `h : hom w' w` such that +- `p₁ ∘ h = p₁'` +- `p₂ ∘ h = p₂'`. + +We say that `C` has all pullbacks if there is a choice of a pullback for each +object `x` and pair of morphisms into `x` in `C`. + +## Definition + +```agda +module _ + {α : Level → Level} {β : Level → Level → Level} + (C : Large-Precategory α β) {l1 l2 l3 l4 : Level} + where + + is-pullback-Large-Precategory : + (x : obj-Large-Precategory C l1) → + (y : obj-Large-Precategory C l2) → + (z : obj-Large-Precategory C l3) → + (f : hom-Large-Precategory C y x) → + (g : hom-Large-Precategory C z x) → + (w : obj-Large-Precategory C l4) → + (p₁ : hom-Large-Precategory C w y) → + (p₂ : hom-Large-Precategory C w z) → + comp-hom-Large-Precategory C f p₁ ＝ comp-hom-Large-Precategory C g p₂ → + UU (α l1 ⊔ β l1 l1 ⊔ β l1 l2 ⊔ β l1 l3 ⊔ β l1 l4) + is-pullback-Large-Precategory x y z f g w p₁ p₂ _ = + (w' : obj-Large-Precategory C l1) → + (p₁' : hom-Large-Precategory C w' y) → + (p₂' : hom-Large-Precategory C w' z) → + comp-hom-Large-Precategory C f p₁' ＝ comp-hom-Large-Precategory C g p₂' → + ∃! + ( hom-Large-Precategory C w' w) + ( λ h → + ( comp-hom-Large-Precategory C p₁ h ＝ p₁') × + ( comp-hom-Large-Precategory C p₂ h ＝ p₂')) + + pullback-Large-Precategory : + (x : obj-Large-Precategory C l1) → + (y : obj-Large-Precategory C l2) → + (z : obj-Large-Precategory C l3) → + hom-Large-Precategory C y x → + hom-Large-Precategory C z x → + UU (α l1 ⊔ α l4 ⊔ β l1 l1 ⊔ β l1 l2 ⊔ β l1 l3 ⊔ + β l1 l4 ⊔ β l4 l1 ⊔ β l4 l2 ⊔ β l4 l3) + pullback-Large-Precategory x y z f g = + Σ (obj-Large-Precategory C l4) λ w → + Σ (hom-Large-Precategory C w y) λ p₁ → + Σ (hom-Large-Precategory C w z) λ p₂ → + Σ (comp-hom-Large-Precategory C f p₁ + ＝ comp-hom-Large-Precategory C g p₂) λ α → + is-pullback-Large-Precategory x y z f g w p₁ p₂ α + + has-all-pullbacks-Large-Precategory : + UU (α l1 ⊔ α l2 ⊔ α l3 ⊔ α l4 ⊔ β l1 l1 ⊔ β l1 l2 ⊔ β l1 l3 ⊔ + β l1 l4 ⊔ β l2 l1 ⊔ β l3 l1 ⊔ β l4 l1 ⊔ β l4 l2 ⊔ β l4 l3) + has-all-pullbacks-Large-Precategory = + (x : obj-Large-Precategory C l1) → + (y : obj-Large-Precategory C l2) → + (z : obj-Large-Precategory C l3) → + (f : hom-Large-Precategory C y x) → + (g : hom-Large-Precategory C z x) → + pullback-Large-Precategory x y z f g + +module _ + {α : Level → Level} {β : Level → Level → Level} + (C : Large-Precategory α β) {l1 l2 : Level} + (t : has-all-pullbacks-Large-Precategory C) + (x y z : obj-Large-Precategory C l1) + (f : hom-Large-Precategory C y x) + (g : hom-Large-Precategory C z x) + where + + object-pullback-Large-Precategory : obj-Large-Precategory C l2 + object-pullback-Large-Precategory = pr1 (t x y z f g) + + pr1-pullback-Large-Precategory : + hom-Large-Precategory C object-pullback-Large-Precategory y + pr1-pullback-Large-Precategory = pr1 (pr2 (t x y z f g)) + + pr2-pullback-Large-Precategory : + hom-Large-Precategory C object-pullback-Large-Precategory z + pr2-pullback-Large-Precategory = pr1 (pr2 (pr2 (t x y z f g))) + + pullback-square-Large-Precategory-comm : + comp-hom-Large-Precategory C f pr1-pullback-Large-Precategory ＝ + comp-hom-Large-Precategory C g pr2-pullback-Large-Precategory + pullback-square-Large-Precategory-comm = pr1 (pr2 (pr2 (pr2 (t x y z f g)))) + + module _ + (w' : obj-Large-Precategory C l1) + (p₁' : hom-Large-Precategory C w' y) + (p₂' : hom-Large-Precategory C w' z) + (α : comp-hom-Large-Precategory C f p₁' + ＝ comp-hom-Large-Precategory C g p₂') + where + + morphism-into-pullback-Large-Precategory : + hom-Large-Precategory C w' object-pullback-Large-Precategory + morphism-into-pullback-Large-Precategory = + pr1 (pr1 (pr2 (pr2 (pr2 (pr2 (t x y z f g)))) w' p₁' p₂' α)) + + morphism-into-pullback-comm-pr1-Large-Precategory : + comp-hom-Large-Precategory C + pr1-pullback-Large-Precategory + morphism-into-pullback-Large-Precategory ＝ + p₁' + morphism-into-pullback-comm-pr1-Large-Precategory = + pr1 (pr2 (pr1 (pr2 (pr2 (pr2 (pr2 (t x y z f g)))) w' p₁' p₂' α))) + + morphism-into-pullback-comm-pr2-Large-Precategory : + comp-hom-Large-Precategory C + pr2-pullback-Large-Precategory + morphism-into-pullback-Large-Precategory ＝ + p₂' + morphism-into-pullback-comm-pr2-Large-Precategory = + pr2 (pr2 (pr1 (pr2 (pr2 (pr2 (pr2 (t x y z f g)))) w' p₁' p₂' α))) + + is-unique-morphism-into-pullback-Large-Precategory : + (h' : hom-Large-Precategory C w' object-pullback-Large-Precategory) → + comp-hom-Large-Precategory C pr1-pullback-Large-Precategory h' ＝ p₁' → + comp-hom-Large-Precategory C pr2-pullback-Large-Precategory h' ＝ p₂' → + morphism-into-pullback-Large-Precategory ＝ h' + is-unique-morphism-into-pullback-Large-Precategory h' α₁ α₂ = + ap + ( pr1) + ( pr2 (pr2 (pr2 (pr2 (pr2 (t x y z f g)))) w' p₁' p₂' α) (h' , α₁ , α₂)) + +module _ + {α : Level → Level} {β : Level → Level → Level} + {l1 l2 l3 l4 : Level} (C : Large-Precategory α β) + (x : obj-Large-Precategory C l1) + (y : obj-Large-Precategory C l2) + (z : obj-Large-Precategory C l3) + (f : hom-Large-Precategory C y x) + (g : hom-Large-Precategory C z x) + (w : obj-Large-Precategory C l4) + (p₁ : hom-Large-Precategory C w y) + (p₂ : hom-Large-Precategory C w z) + (α₁ : comp-hom-Large-Precategory C f p₁ ＝ comp-hom-Large-Precategory C g p₂) + where + + is-prop-is-pullback-Large-Precategory : + is-prop (is-pullback-Large-Precategory C x y z f g w p₁ p₂ α₁) + is-prop-is-pullback-Large-Precategory = + is-prop-Π³ (λ w' p₁' p₂' → is-prop-function-type is-property-is-contr) + + is-pullback-prop-Large-Precategory : + Prop (α l1 ⊔ β l1 l1 ⊔ β l1 l2 ⊔ β l1 l3 ⊔ β l1 l4) + pr1 is-pullback-prop-Large-Precategory = + is-pullback-Large-Precategory C x y z f g w p₁ p₂ α₁ + pr2 is-pullback-prop-Large-Precategory = + is-prop-is-pullback-Large-Precategory +``` diff --git a/src/category-theory/pullbacks-in-precategories.lagda.md b/src/category-theory/pullbacks-in-precategories.lagda.md index 6a5d2efeb8..9d9bef3aa1 100644 --- a/src/category-theory/pullbacks-in-precategories.lagda.md +++ b/src/category-theory/pullbacks-in-precategories.lagda.md @@ -76,8 +76,8 @@ module _ Σ (comp-hom-Precategory C f p₁ ＝ comp-hom-Precategory C g p₂) λ α → is-pullback-Precategory x y z f g w p₁ p₂ α - has-all-pullback-Precategory : UU (l1 ⊔ l2) - has-all-pullback-Precategory = + has-all-pullbacks-Precategory : UU (l1 ⊔ l2) + has-all-pullbacks-Precategory = (x y z : obj-Precategory C) → (f : hom-Precategory C y x) → (g : hom-Precategory C z x) → @@ -85,7 +85,7 @@ module _ module _ {l1 l2 : Level} (C : Precategory l1 l2) - (t : has-all-pullback-Precategory C) + (t : has-all-pullbacks-Precategory C) (x y z : obj-Precategory C) (f : hom-Precategory C y x) (g : hom-Precategory C z x) @@ -119,20 +119,20 @@ module _ morphism-into-pullback-Precategory = pr1 (pr1 (pr2 (pr2 (pr2 (pr2 (t x y z f g)))) w' p₁' p₂' α)) - morphism-into-pullback-comm-pr1 : + morphism-into-pullback-comm-pr1-Precategory : comp-hom-Precategory C pr1-pullback-Precategory morphism-into-pullback-Precategory ＝ p₁' - morphism-into-pullback-comm-pr1 = + morphism-into-pullback-comm-pr1-Precategory = pr1 (pr2 (pr1 (pr2 (pr2 (pr2 (pr2 (t x y z f g)))) w' p₁' p₂' α))) - morphism-into-pullback-comm-pr2 : + morphism-into-pullback-comm-pr2-Precategory : comp-hom-Precategory C pr2-pullback-Precategory morphism-into-pullback-Precategory ＝ p₂' - morphism-into-pullback-comm-pr2 = + morphism-into-pullback-comm-pr2-Precategory = pr2 (pr2 (pr1 (pr2 (pr2 (pr2 (pr2 (t x y z f g)))) w' p₁' p₂' α))) is-unique-morphism-into-pullback-Precategory : From 753b8edcceb7230e3a8e0aff1d7c8b2ab30429c7 Mon Sep 17 00:00:00 2001 From: Mabel Najdovski Date: Thu, 28 Sep 2023 16:43:34 +0200 Subject: [PATCH 2/5] Add missing file --- ...classifier-in-large-precategories.lagda.md | 29 +++++++++++++++++++ 1 file changed, 29 insertions(+) create mode 100644 src/category-theory/subobject-classifier-in-large-precategories.lagda.md diff --git a/src/category-theory/subobject-classifier-in-large-precategories.lagda.md b/src/category-theory/subobject-classifier-in-large-precategories.lagda.md new file mode 100644 index 0000000000..a9fa34245e --- /dev/null +++ b/src/category-theory/subobject-classifier-in-large-precategories.lagda.md @@ -0,0 +1,29 @@ +# The subobject classifier in large precategories + +```agda +module category-theory.subobject-classifier-in-large-precategories where +``` + +
Imports + +```agda +open import category-theory.large-precategories +open import category-theory.monomorphisms-in-large-precategories + +open import foundation.equivalence-relations +open import foundation.equivalences +open import foundation.universe-levels +``` + +
+ +## Definition + +```agda +module _ + {α : Level → Level} {β : Level → Level → Level} + (C : Large-Precategory α β) {l1 l2 : Level} (l3 : Level) + (S : obj-Large-Precategory C l1) (X : obj-Large-Precategory C l2) + (m : mono-Large-Precategory C l3 S X) + where +``` From 8f2b187278c02fc6c4af9c65d30a8d6130838fce Mon Sep 17 00:00:00 2001 From: maybemabeline <142519092+maybemabeline@users.noreply.github.com> Date: Thu, 28 Sep 2023 16:52:28 +0200 Subject: [PATCH 3/5] Update src/category-theory/pullbacks-in-large-precategories.lagda.md Co-authored-by: Fredrik Bakke --- .../pullbacks-in-large-precategories.lagda.md | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/category-theory/pullbacks-in-large-precategories.lagda.md b/src/category-theory/pullbacks-in-large-precategories.lagda.md index fa350197d6..581b2ef4b1 100644 --- a/src/category-theory/pullbacks-in-large-precategories.lagda.md +++ b/src/category-theory/pullbacks-in-large-precategories.lagda.md @@ -46,12 +46,12 @@ module _ where is-pullback-Large-Precategory : - (x : obj-Large-Precategory C l1) → - (y : obj-Large-Precategory C l2) → - (z : obj-Large-Precategory C l3) → - (f : hom-Large-Precategory C y x) → + {x : obj-Large-Precategory C l1} + {y : obj-Large-Precategory C l2} + {z : obj-Large-Precategory C l3} + {w : obj-Large-Precategory C l4} + (f : hom-Large-Precategory C y x) (g : hom-Large-Precategory C z x) → - (w : obj-Large-Precategory C l4) → (p₁ : hom-Large-Precategory C w y) → (p₂ : hom-Large-Precategory C w z) → comp-hom-Large-Precategory C f p₁ ＝ comp-hom-Large-Precategory C g p₂ → From 92031c956ecdf3667e03c4ac5f46187adb0d92ac Mon Sep 17 00:00:00 2001 From: Mabel Najdovski Date: Fri, 29 Sep 2023 10:53:42 +0200 Subject: [PATCH 4/5] Deindex variables and unnest module --- ...omorphisms-in-large-precategories.lagda.md | 18 ++-- .../pullbacks-in-large-precategories.lagda.md | 86 +++++++++---------- .../pullbacks-in-precategories.lagda.md | 74 ++++++++-------- 3 files changed, 88 insertions(+), 90 deletions(-) diff --git a/src/category-theory/monomorphisms-in-large-precategories.lagda.md b/src/category-theory/monomorphisms-in-large-precategories.lagda.md index 870e70f7f1..afbc98dfaf 100644 --- a/src/category-theory/monomorphisms-in-large-precategories.lagda.md +++ b/src/category-theory/monomorphisms-in-large-precategories.lagda.md @@ -67,16 +67,14 @@ module _ ( hom-Large-Precategory C X Y) ( is-mono-Large-Precategory C l3 X Y) - module _ - (f : mono-Large-Precategory) - where - - hom-mono-Large-Precategory : hom-Large-Precategory C X Y - hom-mono-Large-Precategory = pr1 f - - is-mono-mono-Large-Precategory : - is-mono-Large-Precategory C l3 X Y hom-mono-Large-Precategory - is-mono-mono-Large-Precategory = pr2 f + hom-mono-Large-Precategory : + (f : mono-Large-Precategory) → hom-Large-Precategory C X Y + hom-mono-Large-Precategory f = pr1 f + + is-mono-mono-Large-Precategory : + (f : mono-Large-Precategory) → + is-mono-Large-Precategory C l3 X Y (hom-mono-Large-Precategory f) + is-mono-mono-Large-Precategory f = pr2 f ``` ## Properties diff --git a/src/category-theory/pullbacks-in-large-precategories.lagda.md b/src/category-theory/pullbacks-in-large-precategories.lagda.md index 581b2ef4b1..16500013ba 100644 --- a/src/category-theory/pullbacks-in-large-precategories.lagda.md +++ b/src/category-theory/pullbacks-in-large-precategories.lagda.md @@ -27,12 +27,12 @@ A pullback of two morphisms `f : hom y x` and `g : hom z x` in a category `C` consists of: - an object `w` -- morphisms `p₁ : hom w y` and `p₂ : hom w z` such that -- `f ∘ p₁ = g ∘ p₂` together with the universal property that for every object - `w'` and pair of morphisms `p₁' : hom w' y` and `p₂' : hom w' z` such that - `f ∘ p₁' = g ∘ p₂'` there exists a unique morphism `h : hom w' w` such that -- `p₁ ∘ h = p₁'` -- `p₂ ∘ h = p₂'`. +- morphisms `p : hom w y` and `q : hom w z` such that +- `f ∘ p = g ∘ q` together with the universal property that for every object + `w'` and pair of morphisms `p' : hom w' y` and `q' : hom w' z` such that + `f ∘ p' = g ∘ q'` there exists a unique morphism `h : hom w' w` such that +- `p ∘ h = p'` +- `q ∘ h = q'`. We say that `C` has all pullbacks if there is a choice of a pullback for each object `x` and pair of morphisms into `x` in `C`. @@ -46,26 +46,26 @@ module _ where is-pullback-Large-Precategory : - {x : obj-Large-Precategory C l1} - {y : obj-Large-Precategory C l2} - {z : obj-Large-Precategory C l3} - {w : obj-Large-Precategory C l4} + (x : obj-Large-Precategory C l1) + (y : obj-Large-Precategory C l2) + (z : obj-Large-Precategory C l3) (f : hom-Large-Precategory C y x) (g : hom-Large-Precategory C z x) → - (p₁ : hom-Large-Precategory C w y) → - (p₂ : hom-Large-Precategory C w z) → - comp-hom-Large-Precategory C f p₁ ＝ comp-hom-Large-Precategory C g p₂ → + (w : obj-Large-Precategory C l4) + (p : hom-Large-Precategory C w y) → + (q : hom-Large-Precategory C w z) → + comp-hom-Large-Precategory C f p ＝ comp-hom-Large-Precategory C g q → UU (α l1 ⊔ β l1 l1 ⊔ β l1 l2 ⊔ β l1 l3 ⊔ β l1 l4) - is-pullback-Large-Precategory x y z f g w p₁ p₂ _ = + is-pullback-Large-Precategory x y z f g w p q _ = (w' : obj-Large-Precategory C l1) → - (p₁' : hom-Large-Precategory C w' y) → - (p₂' : hom-Large-Precategory C w' z) → - comp-hom-Large-Precategory C f p₁' ＝ comp-hom-Large-Precategory C g p₂' → + (p' : hom-Large-Precategory C w' y) → + (q' : hom-Large-Precategory C w' z) → + comp-hom-Large-Precategory C f p' ＝ comp-hom-Large-Precategory C g q' → ∃! ( hom-Large-Precategory C w' w) ( λ h → - ( comp-hom-Large-Precategory C p₁ h ＝ p₁') × - ( comp-hom-Large-Precategory C p₂ h ＝ p₂')) + ( comp-hom-Large-Precategory C p h ＝ p') × + ( comp-hom-Large-Precategory C q h ＝ q')) pullback-Large-Precategory : (x : obj-Large-Precategory C l1) → @@ -77,11 +77,11 @@ module _ β l1 l4 ⊔ β l4 l1 ⊔ β l4 l2 ⊔ β l4 l3) pullback-Large-Precategory x y z f g = Σ (obj-Large-Precategory C l4) λ w → - Σ (hom-Large-Precategory C w y) λ p₁ → - Σ (hom-Large-Precategory C w z) λ p₂ → - Σ (comp-hom-Large-Precategory C f p₁ - ＝ comp-hom-Large-Precategory C g p₂) λ α → - is-pullback-Large-Precategory x y z f g w p₁ p₂ α + Σ (hom-Large-Precategory C w y) λ p → + Σ (hom-Large-Precategory C w z) λ q → + Σ (comp-hom-Large-Precategory C f p + ＝ comp-hom-Large-Precategory C g q) λ α → + is-pullback-Large-Precategory x y z f g w p q α has-all-pullbacks-Large-Precategory : UU (α l1 ⊔ α l2 ⊔ α l3 ⊔ α l4 ⊔ β l1 l1 ⊔ β l1 l2 ⊔ β l1 l3 ⊔ @@ -121,42 +121,42 @@ module _ module _ (w' : obj-Large-Precategory C l1) - (p₁' : hom-Large-Precategory C w' y) - (p₂' : hom-Large-Precategory C w' z) - (α : comp-hom-Large-Precategory C f p₁' - ＝ comp-hom-Large-Precategory C g p₂') + (p' : hom-Large-Precategory C w' y) + (q' : hom-Large-Precategory C w' z) + (ε : comp-hom-Large-Precategory C f p' + ＝ comp-hom-Large-Precategory C g q') where morphism-into-pullback-Large-Precategory : hom-Large-Precategory C w' object-pullback-Large-Precategory morphism-into-pullback-Large-Precategory = - pr1 (pr1 (pr2 (pr2 (pr2 (pr2 (t x y z f g)))) w' p₁' p₂' α)) + pr1 (pr1 (pr2 (pr2 (pr2 (pr2 (t x y z f g)))) w' p' q' ε)) morphism-into-pullback-comm-pr1-Large-Precategory : comp-hom-Large-Precategory C pr1-pullback-Large-Precategory morphism-into-pullback-Large-Precategory ＝ - p₁' + p' morphism-into-pullback-comm-pr1-Large-Precategory = - pr1 (pr2 (pr1 (pr2 (pr2 (pr2 (pr2 (t x y z f g)))) w' p₁' p₂' α))) + pr1 (pr2 (pr1 (pr2 (pr2 (pr2 (pr2 (t x y z f g)))) w' p' q' ε))) morphism-into-pullback-comm-pr2-Large-Precategory : comp-hom-Large-Precategory C pr2-pullback-Large-Precategory morphism-into-pullback-Large-Precategory ＝ - p₂' + q' morphism-into-pullback-comm-pr2-Large-Precategory = - pr2 (pr2 (pr1 (pr2 (pr2 (pr2 (pr2 (t x y z f g)))) w' p₁' p₂' α))) + pr2 (pr2 (pr1 (pr2 (pr2 (pr2 (pr2 (t x y z f g)))) w' p' q' ε))) is-unique-morphism-into-pullback-Large-Precategory : (h' : hom-Large-Precategory C w' object-pullback-Large-Precategory) → - comp-hom-Large-Precategory C pr1-pullback-Large-Precategory h' ＝ p₁' → - comp-hom-Large-Precategory C pr2-pullback-Large-Precategory h' ＝ p₂' → + comp-hom-Large-Precategory C pr1-pullback-Large-Precategory h' ＝ p' → + comp-hom-Large-Precategory C pr2-pullback-Large-Precategory h' ＝ q' → morphism-into-pullback-Large-Precategory ＝ h' - is-unique-morphism-into-pullback-Large-Precategory h' α₁ α₂ = + is-unique-morphism-into-pullback-Large-Precategory h' η θ = ap ( pr1) - ( pr2 (pr2 (pr2 (pr2 (pr2 (t x y z f g)))) w' p₁' p₂' α) (h' , α₁ , α₂)) + ( pr2 (pr2 (pr2 (pr2 (pr2 (t x y z f g)))) w' p' q' ε) (h' , η , θ)) module _ {α : Level → Level} {β : Level → Level → Level} @@ -167,20 +167,20 @@ module _ (f : hom-Large-Precategory C y x) (g : hom-Large-Precategory C z x) (w : obj-Large-Precategory C l4) - (p₁ : hom-Large-Precategory C w y) - (p₂ : hom-Large-Precategory C w z) - (α₁ : comp-hom-Large-Precategory C f p₁ ＝ comp-hom-Large-Precategory C g p₂) + (p : hom-Large-Precategory C w y) + (q : hom-Large-Precategory C w z) + (ε : comp-hom-Large-Precategory C f p ＝ comp-hom-Large-Precategory C g q) where is-prop-is-pullback-Large-Precategory : - is-prop (is-pullback-Large-Precategory C x y z f g w p₁ p₂ α₁) + is-prop (is-pullback-Large-Precategory C x y z f g w p q ε) is-prop-is-pullback-Large-Precategory = - is-prop-Π³ (λ w' p₁' p₂' → is-prop-function-type is-property-is-contr) + is-prop-Π³ (λ w' p' q' → is-prop-function-type is-property-is-contr) is-pullback-prop-Large-Precategory : Prop (α l1 ⊔ β l1 l1 ⊔ β l1 l2 ⊔ β l1 l3 ⊔ β l1 l4) pr1 is-pullback-prop-Large-Precategory = - is-pullback-Large-Precategory C x y z f g w p₁ p₂ α₁ + is-pullback-Large-Precategory C x y z f g w p q ε pr2 is-pullback-prop-Large-Precategory = is-prop-is-pullback-Large-Precategory ``` diff --git a/src/category-theory/pullbacks-in-precategories.lagda.md b/src/category-theory/pullbacks-in-precategories.lagda.md index 9d9bef3aa1..e529c81d9a 100644 --- a/src/category-theory/pullbacks-in-precategories.lagda.md +++ b/src/category-theory/pullbacks-in-precategories.lagda.md @@ -27,12 +27,12 @@ A pullback of two morphisms `f : hom y x` and `g : hom z x` in a category `C` consists of: - an object `w` -- morphisms `p₁ : hom w y` and `p₂ : hom w z` such that -- `f ∘ p₁ = g ∘ p₂` together with the universal property that for every object - `w'` and pair of morphisms `p₁' : hom w' y` and `p₂' : hom w' z` such that - `f ∘ p₁' = g ∘ p₂'` there exists a unique morphism `h : hom w' w` such that -- `p₁ ∘ h = p₁'` -- `p₂ ∘ h = p₂'`. +- morphisms `p : hom w y` and `q : hom w z` such that +- `f ∘ p = g ∘ q` together with the universal property that for every object + `w'` and pair of morphisms `p' : hom w' y` and `q' : hom w' z` such that + `f ∘ p' = g ∘ q'` there exists a unique morphism `h : hom w' w` such that +- `p ∘ h = p'` +- `q ∘ h = q'`. We say that `C` has all pullbacks if there is a choice of a pullback for each object `x` and pair of morphisms into `x` in `C`. @@ -49,20 +49,20 @@ module _ (f : hom-Precategory C y x) → (g : hom-Precategory C z x) → (w : obj-Precategory C) → - (p₁ : hom-Precategory C w y) → - (p₂ : hom-Precategory C w z) → - comp-hom-Precategory C f p₁ ＝ comp-hom-Precategory C g p₂ → + (p : hom-Precategory C w y) → + (q : hom-Precategory C w z) → + comp-hom-Precategory C f p ＝ comp-hom-Precategory C g q → UU (l1 ⊔ l2) - is-pullback-Precategory x y z f g w p₁ p₂ _ = + is-pullback-Precategory x y z f g w p q _ = (w' : obj-Precategory C) → - (p₁' : hom-Precategory C w' y) → - (p₂' : hom-Precategory C w' z) → - comp-hom-Precategory C f p₁' ＝ comp-hom-Precategory C g p₂' → + (p' : hom-Precategory C w' y) → + (q' : hom-Precategory C w' z) → + comp-hom-Precategory C f p' ＝ comp-hom-Precategory C g q' → ∃! ( hom-Precategory C w' w) ( λ h → - ( comp-hom-Precategory C p₁ h ＝ p₁') × - ( comp-hom-Precategory C p₂ h ＝ p₂')) + ( comp-hom-Precategory C p h ＝ p') × + ( comp-hom-Precategory C q h ＝ q')) pullback-Precategory : (x y z : obj-Precategory C) → @@ -71,10 +71,10 @@ module _ UU (l1 ⊔ l2) pullback-Precategory x y z f g = Σ (obj-Precategory C) λ w → - Σ (hom-Precategory C w y) λ p₁ → - Σ (hom-Precategory C w z) λ p₂ → - Σ (comp-hom-Precategory C f p₁ ＝ comp-hom-Precategory C g p₂) λ α → - is-pullback-Precategory x y z f g w p₁ p₂ α + Σ (hom-Precategory C w y) λ p → + Σ (hom-Precategory C w z) λ q → + Σ (comp-hom-Precategory C f p ＝ comp-hom-Precategory C g q) λ α → + is-pullback-Precategory x y z f g w p q α has-all-pullbacks-Precategory : UU (l1 ⊔ l2) has-all-pullbacks-Precategory = @@ -109,41 +109,41 @@ module _ module _ (w' : obj-Precategory C) - (p₁' : hom-Precategory C w' y) - (p₂' : hom-Precategory C w' z) - (α : comp-hom-Precategory C f p₁' ＝ comp-hom-Precategory C g p₂') + (p' : hom-Precategory C w' y) + (q' : hom-Precategory C w' z) + (ε : comp-hom-Precategory C f p' ＝ comp-hom-Precategory C g q') where morphism-into-pullback-Precategory : hom-Precategory C w' object-pullback-Precategory morphism-into-pullback-Precategory = - pr1 (pr1 (pr2 (pr2 (pr2 (pr2 (t x y z f g)))) w' p₁' p₂' α)) + pr1 (pr1 (pr2 (pr2 (pr2 (pr2 (t x y z f g)))) w' p' q' ε)) morphism-into-pullback-comm-pr1-Precategory : comp-hom-Precategory C pr1-pullback-Precategory morphism-into-pullback-Precategory ＝ - p₁' + p' morphism-into-pullback-comm-pr1-Precategory = - pr1 (pr2 (pr1 (pr2 (pr2 (pr2 (pr2 (t x y z f g)))) w' p₁' p₂' α))) + pr1 (pr2 (pr1 (pr2 (pr2 (pr2 (pr2 (t x y z f g)))) w' p' q' ε))) morphism-into-pullback-comm-pr2-Precategory : comp-hom-Precategory C pr2-pullback-Precategory morphism-into-pullback-Precategory ＝ - p₂' + q' morphism-into-pullback-comm-pr2-Precategory = - pr2 (pr2 (pr1 (pr2 (pr2 (pr2 (pr2 (t x y z f g)))) w' p₁' p₂' α))) + pr2 (pr2 (pr1 (pr2 (pr2 (pr2 (pr2 (t x y z f g)))) w' p' q' ε))) is-unique-morphism-into-pullback-Precategory : (h' : hom-Precategory C w' object-pullback-Precategory) → - comp-hom-Precategory C pr1-pullback-Precategory h' ＝ p₁' → - comp-hom-Precategory C pr2-pullback-Precategory h' ＝ p₂' → + comp-hom-Precategory C pr1-pullback-Precategory h' ＝ p' → + comp-hom-Precategory C pr2-pullback-Precategory h' ＝ q' → morphism-into-pullback-Precategory ＝ h' - is-unique-morphism-into-pullback-Precategory h' α₁ α₂ = + is-unique-morphism-into-pullback-Precategory h' η θ = ap ( pr1) - ( pr2 (pr2 (pr2 (pr2 (pr2 (t x y z f g)))) w' p₁' p₂' α) (h' , α₁ , α₂)) + ( pr2 (pr2 (pr2 (pr2 (pr2 (t x y z f g)))) w' p' q' ε) (h' , η , θ)) module _ {l1 l2 : Level} (C : Precategory l1 l2) @@ -151,19 +151,19 @@ module _ (f : hom-Precategory C y x) (g : hom-Precategory C z x) (w : obj-Precategory C) - (p₁ : hom-Precategory C w y) - (p₂ : hom-Precategory C w z) - (α : comp-hom-Precategory C f p₁ ＝ comp-hom-Precategory C g p₂) + (p : hom-Precategory C w y) + (q : hom-Precategory C w z) + (ε : comp-hom-Precategory C f p ＝ comp-hom-Precategory C g q) where is-prop-is-pullback-Precategory : - is-prop (is-pullback-Precategory C x y z f g w p₁ p₂ α) + is-prop (is-pullback-Precategory C x y z f g w p q ε) is-prop-is-pullback-Precategory = - is-prop-Π³ (λ w' p₁' p₂' → is-prop-function-type is-property-is-contr) + is-prop-Π³ (λ w' p' q' → is-prop-function-type is-property-is-contr) is-pullback-prop-Precategory : Prop (l1 ⊔ l2) pr1 is-pullback-prop-Precategory = - is-pullback-Precategory C x y z f g w p₁ p₂ α + is-pullback-Precategory C x y z f g w p q ε pr2 is-pullback-prop-Precategory = is-prop-is-pullback-Precategory ``` From bff8acd1dea930e4da737f506452bc98c4a5936f Mon Sep 17 00:00:00 2001 From: Mabel Najdovski Date: Fri, 29 Sep 2023 11:09:57 +0200 Subject: [PATCH 5/5] Reformat path algebra --- ...omorphisms-in-large-precategories.lagda.md | 36 +++++++++---------- 1 file changed, 18 insertions(+), 18 deletions(-) diff --git a/src/category-theory/monomorphisms-in-large-precategories.lagda.md b/src/category-theory/monomorphisms-in-large-precategories.lagda.md index afbc98dfaf..ad4e1ae3c1 100644 --- a/src/category-theory/monomorphisms-in-large-precategories.lagda.md +++ b/src/category-theory/monomorphisms-in-large-precategories.lagda.md @@ -96,34 +96,34 @@ module _ ( λ P → ( inv ( left-unit-law-comp-hom-Large-Precategory C g)) ∙ - ( ( ap + ( ap ( λ h' → comp-hom-Large-Precategory C h' g) ( inv (is-retraction-hom-inv-iso-Large-Precategory C f))) ∙ - ( ( associative-comp-hom-Large-Precategory C + ( associative-comp-hom-Large-Precategory C + ( hom-inv-iso-Large-Precategory C f) + ( hom-iso-Large-Precategory C f) + ( g)) ∙ + ( ap + ( comp-hom-Large-Precategory C + ( hom-inv-iso-Large-Precategory C f)) + ( P)) ∙ + ( inv + ( associative-comp-hom-Large-Precategory C ( hom-inv-iso-Large-Precategory C f) ( hom-iso-Large-Precategory C f) - ( g)) ∙ - ( ( ap - ( comp-hom-Large-Precategory C - ( hom-inv-iso-Large-Precategory C f)) - ( P)) ∙ - ( ( inv - ( associative-comp-hom-Large-Precategory C - ( hom-inv-iso-Large-Precategory C f) - ( hom-iso-Large-Precategory C f) - ( h))) ∙ - ( ( ap - ( λ h' → comp-hom-Large-Precategory C h' h) - ( is-retraction-hom-inv-iso-Large-Precategory C f)) ∙ - ( left-unit-law-comp-hom-Large-Precategory C h))))))) + ( h))) ∙ + ( ap + ( λ h' → comp-hom-Large-Precategory C h' h) + ( is-retraction-hom-inv-iso-Large-Precategory C f)) ∙ + ( left-unit-law-comp-hom-Large-Precategory C h)) ( λ p → - eq-is-prop + ( eq-is-prop ( is-set-hom-Large-Precategory C Z Y ( comp-hom-Large-Precategory C ( hom-iso-Large-Precategory C f) ( g)) ( comp-hom-Large-Precategory C ( hom-iso-Large-Precategory C f) - ( h)))) + ( h))))) ( λ p → eq-is-prop (is-set-hom-Large-Precategory C Z X g h)) ```