From 690125246012397492da3e61c907f18c47326f3b Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sun, 27 Oct 2024 13:03:19 +0100 Subject: [PATCH] Displayed precategories (#922) Defines displayed precategories. --- references.bib | 16 + src/category-theory.lagda.md | 2 + ...ion-operations-over-precategories.lagda.md | 269 ++++++++++ .../displayed-precategories.lagda.md | 470 ++++++++++++++++++ src/category-theory/precategories.lagda.md | 66 +++ .../dependent-identifications.lagda.md | 22 +- .../simple-type-theories.lagda.md | 6 +- 7 files changed, 835 insertions(+), 16 deletions(-) create mode 100644 src/category-theory/dependent-composition-operations-over-precategories.lagda.md create mode 100644 src/category-theory/displayed-precategories.lagda.md diff --git a/references.bib b/references.bib index d709f0c64f..33606e9ae6 100644 --- a/references.bib +++ b/references.bib @@ -28,6 +28,22 @@ @article{AKS15 langid = {english} } +@article{AL19, + title = {Displayed Categories}, + author = {Ahrens, Benedikt and {{LeFanu}} Lumsdaine, Peter}, + doi = {10.23638/LMCS-15(1:20)2019}, + journal = {{Logical Methods in Computer Science}}, + volume = {15}, + issue = {1}, + year = {2019}, + month = {03}, + keywords = {Mathematics - Category Theory ; Mathematics - Logic ; 18A15, 03B15, 03B70 ; F.4.1}, + eprint = {1705.04296}, + eprinttype = {arxiv}, + eprintclass = {math}, + langid = {english} +} + @online{BCDE21, title = {Free groups in HoTT/UF in Agda}, author = {Bezem, Marc and Coquand, Thierry and Dybjer, Peter and Escardó, Martín}, diff --git a/src/category-theory.lagda.md b/src/category-theory.lagda.md index e4bb19aab7..4e0084b390 100644 --- a/src/category-theory.lagda.md +++ b/src/category-theory.lagda.md @@ -38,11 +38,13 @@ open import category-theory.coproducts-in-precategories public open import category-theory.cores-categories public open import category-theory.cores-precategories public open import category-theory.coslice-precategories public +open import category-theory.dependent-composition-operations-over-precategories public open import category-theory.dependent-products-of-categories public open import category-theory.dependent-products-of-large-categories public open import category-theory.dependent-products-of-large-precategories public open import category-theory.dependent-products-of-precategories public open import category-theory.discrete-categories public +open import category-theory.displayed-precategories public open import category-theory.embedding-maps-precategories public open import category-theory.embeddings-precategories public open import category-theory.endomorphisms-in-categories public diff --git a/src/category-theory/dependent-composition-operations-over-precategories.lagda.md b/src/category-theory/dependent-composition-operations-over-precategories.lagda.md new file mode 100644 index 0000000000..8f663b706e --- /dev/null +++ b/src/category-theory/dependent-composition-operations-over-precategories.lagda.md @@ -0,0 +1,269 @@ +# Dependent composition operations over precategories + +```agda +module category-theory.dependent-composition-operations-over-precategories where +``` + +
Imports + +```agda +open import category-theory.composition-operations-on-binary-families-of-sets +open import category-theory.nonunital-precategories +open import category-theory.precategories +open import category-theory.set-magmoids + +open import foundation.cartesian-product-types +open import foundation.dependent-identifications +open import foundation.dependent-pair-types +open import foundation.function-types +open import foundation.identity-types +open import foundation.iterated-dependent-product-types +open import foundation.propositions +open import foundation.sets +open import foundation.transport-along-identifications +open import foundation.truncated-types +open import foundation.truncation-levels +open import foundation.universe-levels +``` + +
+ +## Idea + +Given a [precategory](category-theory.precategories.md) `C`, a +{{#concept "dependent composition structure" Disambiguation="over a precategory"}} +`D` over `C` is a family of types `obj D` over `obj C` and a family of +_hom-[sets](foundation-core.sets.md)_ + +```text +hom D : hom C x y → obj D x → obj D y → Set +``` + +for every pair `x y : obj C`, equipped with a +{{#concept "dependent composition operation" Disambiguation="over a precategory" Agda=dependent-composition-operation-Precategory}} + +```text + comp D : hom D g y' z' → hom D f x' y' → hom D (g ∘ f) x' z'. +``` + +## Definitions + +### The type of dependent composition operations over a precategory + +```agda +module _ + {l1 l2 : Level} (C : Precategory l1 l2) + where + + dependent-composition-operation-Precategory : + { l3 l4 : Level} + ( obj-D : obj-Precategory C → UU l3) → + ( hom-set-D : + {x y : obj-Precategory C} + (f : hom-Precategory C x y) + (x' : obj-D x) (y' : obj-D y) → Set l4) → + UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) + dependent-composition-operation-Precategory obj-D hom-set-D = + {x y z : obj-Precategory C} + (g : hom-Precategory C y z) (f : hom-Precategory C x y) → + {x' : obj-D x} {y' : obj-D y} {z' : obj-D z} → + (g' : type-Set (hom-set-D g y' z')) (f' : type-Set (hom-set-D f x' y')) → + type-Set (hom-set-D (comp-hom-Precategory C g f) x' z') +``` + +### The predicate of being associative on dependent composition operations over a precategory + +```agda +module _ + {l1 l2 l3 l4 : Level} (C : Precategory l1 l2) + ( obj-D : obj-Precategory C → UU l3) + ( hom-set-D : + {x y : obj-Precategory C} + (f : hom-Precategory C x y) (x' : obj-D x) (y' : obj-D y) → Set l4) + ( comp-hom-D : dependent-composition-operation-Precategory C obj-D hom-set-D) + where + + is-associative-dependent-composition-operation-Precategory : + UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) + is-associative-dependent-composition-operation-Precategory = + {x y z w : obj-Precategory C} + (h : hom-Precategory C z w) + (g : hom-Precategory C y z) + (f : hom-Precategory C x y) + {x' : obj-D x} {y' : obj-D y} {z' : obj-D z} {w' : obj-D w} + (h' : type-Set (hom-set-D h z' w')) + (g' : type-Set (hom-set-D g y' z')) + (f' : type-Set (hom-set-D f x' y')) → + dependent-identification + ( λ i → type-Set (hom-set-D i x' w')) + ( associative-comp-hom-Precategory C h g f) + ( comp-hom-D (comp-hom-Precategory C h g) f (comp-hom-D h g h' g') f') + ( comp-hom-D h (comp-hom-Precategory C g f) h' (comp-hom-D g f g' f')) + + is-prop-is-associative-dependent-composition-operation-Precategory : + is-prop is-associative-dependent-composition-operation-Precategory + is-prop-is-associative-dependent-composition-operation-Precategory = + is-prop-iterated-implicit-Π 4 + ( λ x y z w → + is-prop-iterated-Π 3 + ( λ h g f → + is-prop-iterated-implicit-Π 4 + ( λ x' y' z' w' → + is-prop-iterated-Π 3 + ( λ h' g' f' → + is-set-type-Set + ( hom-set-D + ( comp-hom-Precategory C h (comp-hom-Precategory C g f)) + ( x') + ( w')) + ( tr + ( λ i → type-Set (hom-set-D i x' w')) + ( associative-comp-hom-Precategory C h g f) + ( comp-hom-D + ( comp-hom-Precategory C h g) + ( f) + ( comp-hom-D h g h' g') + ( f'))) + ( comp-hom-D + ( h) + ( comp-hom-Precategory C g f) + ( h') + ( comp-hom-D g f g' f')))))) + + is-associative-prop-dependent-composition-operation-Precategory : + Prop (l1 ⊔ l2 ⊔ l3 ⊔ l4) + pr1 is-associative-prop-dependent-composition-operation-Precategory = + is-associative-dependent-composition-operation-Precategory + pr2 is-associative-prop-dependent-composition-operation-Precategory = + is-prop-is-associative-dependent-composition-operation-Precategory +``` + +### The predicate of being unital on dependent composition operations over a precategory + +```agda +module _ + {l1 l2 l3 l4 : Level} (C : Precategory l1 l2) + ( obj-D : obj-Precategory C → UU l3) + ( hom-set-D : + {x y : obj-Precategory C} + (f : hom-Precategory C x y) (x' : obj-D x) (y' : obj-D y) → Set l4) + ( comp-hom-D : dependent-composition-operation-Precategory C obj-D hom-set-D) + ( id-hom-D : + {x : obj-Precategory C} (x' : obj-D x) → + type-Set (hom-set-D (id-hom-Precategory C {x}) x' x')) + where + + is-left-unit-dependent-composition-operation-Precategory : + UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) + is-left-unit-dependent-composition-operation-Precategory = + {x y : obj-Precategory C} (f : hom-Precategory C x y) + {x' : obj-D x} {y' : obj-D y} (f' : type-Set (hom-set-D f x' y')) → + dependent-identification + ( λ i → type-Set (hom-set-D i x' y')) + ( left-unit-law-comp-hom-Precategory C f) + ( comp-hom-D (id-hom-Precategory C) f (id-hom-D y') f') + ( f') + + is-prop-is-left-unit-dependent-composition-operation-Precategory : + is-prop is-left-unit-dependent-composition-operation-Precategory + is-prop-is-left-unit-dependent-composition-operation-Precategory = + is-prop-iterated-implicit-Π 2 + ( λ x y → + is-prop-Π + ( λ f → + is-prop-iterated-implicit-Π 2 + ( λ x' y' → + is-prop-Π + ( λ f' → + is-set-type-Set + ( hom-set-D f x' y') + ( tr + ( λ i → type-Set (hom-set-D i x' y')) + ( left-unit-law-comp-hom-Precategory C f) + ( comp-hom-D (id-hom-Precategory C) f (id-hom-D y') f')) + ( f'))))) + + is-left-unit-prop-dependent-composition-operation-Precategory : + Prop (l1 ⊔ l2 ⊔ l3 ⊔ l4) + pr1 is-left-unit-prop-dependent-composition-operation-Precategory = + is-left-unit-dependent-composition-operation-Precategory + pr2 is-left-unit-prop-dependent-composition-operation-Precategory = + is-prop-is-left-unit-dependent-composition-operation-Precategory + + is-right-unit-dependent-composition-operation-Precategory : + UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) + is-right-unit-dependent-composition-operation-Precategory = + {x y : obj-Precategory C} (f : hom-Precategory C x y) + {x' : obj-D x} {y' : obj-D y} (f' : type-Set (hom-set-D f x' y')) → + dependent-identification + ( λ i → type-Set (hom-set-D i x' y')) + ( right-unit-law-comp-hom-Precategory C f) + ( comp-hom-D f (id-hom-Precategory C) f' (id-hom-D x')) + ( f') + + is-prop-is-right-unit-dependent-composition-operation-Precategory : + is-prop is-right-unit-dependent-composition-operation-Precategory + is-prop-is-right-unit-dependent-composition-operation-Precategory = + is-prop-iterated-implicit-Π 2 + ( λ x y → + is-prop-Π + ( λ f → + is-prop-iterated-implicit-Π 2 + ( λ x' y' → + is-prop-Π + ( λ f' → + is-set-type-Set + ( hom-set-D f x' y') + ( tr + ( λ i → type-Set (hom-set-D i x' y')) + ( right-unit-law-comp-hom-Precategory C f) + ( comp-hom-D f (id-hom-Precategory C) f' (id-hom-D x'))) + ( f'))))) + + is-right-unit-prop-dependent-composition-operation-Precategory : + Prop (l1 ⊔ l2 ⊔ l3 ⊔ l4) + pr1 is-right-unit-prop-dependent-composition-operation-Precategory = + is-right-unit-dependent-composition-operation-Precategory + pr2 is-right-unit-prop-dependent-composition-operation-Precategory = + is-prop-is-right-unit-dependent-composition-operation-Precategory + + is-unit-dependent-composition-operation-Precategory : + UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) + is-unit-dependent-composition-operation-Precategory = + ( is-left-unit-dependent-composition-operation-Precategory) × + ( is-right-unit-dependent-composition-operation-Precategory) + + is-prop-is-unit-dependent-composition-operation-Precategory : + is-prop is-unit-dependent-composition-operation-Precategory + is-prop-is-unit-dependent-composition-operation-Precategory = + is-prop-product + ( is-prop-is-left-unit-dependent-composition-operation-Precategory) + ( is-prop-is-right-unit-dependent-composition-operation-Precategory) + + is-unit-prop-dependent-composition-operation-Precategory : + Prop (l1 ⊔ l2 ⊔ l3 ⊔ l4) + pr1 is-unit-prop-dependent-composition-operation-Precategory = + is-unit-dependent-composition-operation-Precategory + pr2 is-unit-prop-dependent-composition-operation-Precategory = + is-prop-is-unit-dependent-composition-operation-Precategory + +module _ + {l1 l2 l3 l4 : Level} (C : Precategory l1 l2) + ( obj-D : obj-Precategory C → UU l3) + ( hom-set-D : + {x y : obj-Precategory C} + (f : hom-Precategory C x y) (x' : obj-D x) (y' : obj-D y) → Set l4) + ( comp-hom-D : dependent-composition-operation-Precategory C obj-D hom-set-D) + where + + is-unital-dependent-composition-operation-Precategory : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) + is-unital-dependent-composition-operation-Precategory = + Σ ( {x : obj-Precategory C} (x' : obj-D x) → + type-Set (hom-set-D (id-hom-Precategory C {x}) x' x')) + ( is-unit-dependent-composition-operation-Precategory C + obj-D hom-set-D comp-hom-D) +``` + +## See also + +- [Displayed precategories](category-theory.displayed-precategories.md) diff --git a/src/category-theory/displayed-precategories.lagda.md b/src/category-theory/displayed-precategories.lagda.md new file mode 100644 index 0000000000..959ce0871a --- /dev/null +++ b/src/category-theory/displayed-precategories.lagda.md @@ -0,0 +1,470 @@ +# Displayed precategories + +```agda +module category-theory.displayed-precategories where +``` + +
Imports + +```agda +open import category-theory.composition-operations-on-binary-families-of-sets +open import category-theory.dependent-composition-operations-over-precategories +open import category-theory.nonunital-precategories +open import category-theory.precategories +open import category-theory.set-magmoids + +open import foundation.cartesian-product-types +open import foundation.dependent-identifications +open import foundation.dependent-pair-types +open import foundation.equality-dependent-pair-types +open import foundation.function-types +open import foundation.identity-types +open import foundation.iterated-dependent-product-types +open import foundation.propositions +open import foundation.sets +open import foundation.strictly-involutive-identity-types +open import foundation.subsingleton-induction +open import foundation.transport-along-identifications +open import foundation.truncated-types +open import foundation.truncation-levels +open import foundation.universe-levels +``` + +
+ +## Idea + +Given a [precategory](category-theory.precategories.md) `𝒞`, a +{{#concept "displayed precategory" Agda=Displayed-Precategory}} over `𝒞` is an +associative and unital +[dependent composition structure](category-theory.dependent-composition-operations-over-precategories.md) +over it. + +Thus, a displayed precategory `𝒟` over `𝒞` consists of + +- a family of objects `obj 𝒟` indexed by `obj 𝒞`, +- a family of hom-[sets](foundation-core.sets.md) + + ```text + hom 𝒟 : hom 𝒞 x y → obj 𝒟 x → obj 𝒟 y → Set, + ``` + + for every pair `x y : obj 𝒞`, and + +- a dependent composition operation + + ```text + comp 𝒟 : hom 𝒟 g y' z' → hom 𝒟 f x' y' → hom 𝒟 (g ∘ f) x' z' + ``` + + such that + +- The dependent associativity condition + + ```text + comp 𝒟 (comp 𝒟 h' g') f' = comp 𝒟 h' (comp 𝒟 g' f') + ``` + + over the associativity witness `(h ∘ g) ∘ f = h ∘ (g ∘ f)` in `𝒞` holds, and + +- the composition operation is dependent unital, meaning there is a family of + identity morphisms + + ```text + id 𝒟 : (x : obj 𝒞) (x' : obj 𝒟 x) → hom 𝒟 (id 𝒞 x) x' x' + ``` + + which is a dependent left and right unit in the sense that the dependent + identities `comp 𝒟 (id 𝒟) f = f` and `comp 𝒟 f (id 𝒟) = f` hold over the + respective witnesses of left and right unitality in `𝒞`. + +## Definitions + +### The predicate of being a displayed precategory + +```agda +module _ + {l1 l2 l3 l4 : Level} (𝒞 : Precategory l1 l2) + ( obj-𝒟 : obj-Precategory 𝒞 → UU l3) + ( hom-set-𝒟 : + {x y : obj-Precategory 𝒞} + (f : hom-Precategory 𝒞 x y) (x' : obj-𝒟 x) (y' : obj-𝒟 y) → Set l4) + ( comp-hom-𝒟 : dependent-composition-operation-Precategory 𝒞 obj-𝒟 hom-set-𝒟) + where + + is-displayed-precategory : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) + is-displayed-precategory = + ( is-associative-dependent-composition-operation-Precategory 𝒞 + obj-𝒟 hom-set-𝒟 comp-hom-𝒟) × + ( is-unital-dependent-composition-operation-Precategory 𝒞 + obj-𝒟 hom-set-𝒟 comp-hom-𝒟) +``` + +### The type of displayed precategories over a precategory + +```agda +module _ + {l1 l2 : Level} (l3 l4 : Level) (𝒞 : Precategory l1 l2) + where + + Displayed-Precategory : UU (l1 ⊔ l2 ⊔ lsuc l3 ⊔ lsuc l4) + Displayed-Precategory = + Σ ( obj-Precategory 𝒞 → UU l3) + ( λ obj-𝒟 → + Σ ( {x y : obj-Precategory 𝒞} + (f : hom-Precategory 𝒞 x y) (x' : obj-𝒟 x) (y' : obj-𝒟 y) → Set l4) + ( λ hom-set-𝒟 → + Σ ( dependent-composition-operation-Precategory 𝒞 obj-𝒟 hom-set-𝒟) + ( is-displayed-precategory 𝒞 obj-𝒟 hom-set-𝒟))) + +module _ + {l1 l2 l3 l4 : Level} + (𝒞 : Precategory l1 l2) (𝒟 : Displayed-Precategory l3 l4 𝒞) + where + + obj-Displayed-Precategory : obj-Precategory 𝒞 → UU l3 + obj-Displayed-Precategory = pr1 𝒟 + + hom-set-Displayed-Precategory : + {x y : obj-Precategory 𝒞} (f : hom-Precategory 𝒞 x y) + (x' : obj-Displayed-Precategory x) (y' : obj-Displayed-Precategory y) → + Set l4 + hom-set-Displayed-Precategory = pr1 (pr2 𝒟) + + hom-Displayed-Precategory : + {x y : obj-Precategory 𝒞} (f : hom-Precategory 𝒞 x y) + (x' : obj-Displayed-Precategory x) (y' : obj-Displayed-Precategory y) → + UU l4 + hom-Displayed-Precategory f x' y' = + type-Set (hom-set-Displayed-Precategory f x' y') + + is-set-hom-Displayed-Precategory : + {x y : obj-Precategory 𝒞} (f : hom-Precategory 𝒞 x y) + (x' : obj-Displayed-Precategory x) (y' : obj-Displayed-Precategory y) → + is-set (hom-Displayed-Precategory f x' y') + is-set-hom-Displayed-Precategory f x' y' = + is-set-type-Set (hom-set-Displayed-Precategory f x' y') + + comp-hom-Displayed-Precategory : + dependent-composition-operation-Precategory 𝒞 + ( obj-Displayed-Precategory) + ( hom-set-Displayed-Precategory) + comp-hom-Displayed-Precategory = pr1 (pr2 (pr2 𝒟)) + + associative-comp-hom-Displayed-Precategory : + is-associative-dependent-composition-operation-Precategory 𝒞 + ( obj-Displayed-Precategory) + ( hom-set-Displayed-Precategory) + ( comp-hom-Displayed-Precategory) + associative-comp-hom-Displayed-Precategory = pr1 (pr2 (pr2 (pr2 𝒟))) + + is-unital-comp-hom-Displayed-Precategory : + is-unital-dependent-composition-operation-Precategory 𝒞 + ( obj-Displayed-Precategory) + ( hom-set-Displayed-Precategory) + ( comp-hom-Displayed-Precategory) + is-unital-comp-hom-Displayed-Precategory = pr2 (pr2 (pr2 (pr2 𝒟))) + + id-hom-Displayed-Precategory : + {x : obj-Precategory 𝒞} (x' : obj-Displayed-Precategory x) → + hom-Displayed-Precategory (id-hom-Precategory 𝒞) x' x' + id-hom-Displayed-Precategory = pr1 is-unital-comp-hom-Displayed-Precategory + + left-unit-law-comp-hom-Displayed-Precategory : + is-left-unit-dependent-composition-operation-Precategory 𝒞 + obj-Displayed-Precategory + hom-set-Displayed-Precategory + comp-hom-Displayed-Precategory + id-hom-Displayed-Precategory + left-unit-law-comp-hom-Displayed-Precategory = + pr1 (pr2 is-unital-comp-hom-Displayed-Precategory) + + right-unit-law-comp-hom-Displayed-Precategory : + is-right-unit-dependent-composition-operation-Precategory 𝒞 + obj-Displayed-Precategory + hom-set-Displayed-Precategory + comp-hom-Displayed-Precategory + id-hom-Displayed-Precategory + right-unit-law-comp-hom-Displayed-Precategory = + pr2 (pr2 is-unital-comp-hom-Displayed-Precategory) +``` + +### The total precategory associated to a displayed precategory + +Given a displayed precategory `𝒟` over `𝒞`, the total structure `∫D` whose +objects are + +```text + obj ∫D := Σ (x : obj 𝒞) (obj 𝒟 x) +``` + +and hom-sets are + +```text + hom ∫D (x , x') (y , y') := Σ (f : hom 𝒞 x y) (hom 𝒟 f x' y') +``` + +form a precategory called the +{{#concept "total precategory" Disambiguation="of a displayed precategory" Agda=total-precategory-Displayed-Precategory}} +of `𝒟`. + +```agda +module _ + {l1 l2 l3 l4 : Level} + (𝒞 : Precategory l1 l2) (𝒟 : Displayed-Precategory l3 l4 𝒞) + where + + obj-total-precategory-Displayed-Precategory : UU (l1 ⊔ l3) + obj-total-precategory-Displayed-Precategory = + Σ (obj-Precategory 𝒞) (obj-Displayed-Precategory 𝒞 𝒟) + + hom-set-total-precategory-Displayed-Precategory : + (x y : obj-total-precategory-Displayed-Precategory) → Set (l2 ⊔ l4) + hom-set-total-precategory-Displayed-Precategory (x , x') (y , y') = + Σ-Set + ( hom-set-Precategory 𝒞 x y) + ( λ f → hom-set-Displayed-Precategory 𝒞 𝒟 f x' y') + + hom-total-precategory-Displayed-Precategory : + (x y : obj-total-precategory-Displayed-Precategory) → UU (l2 ⊔ l4) + hom-total-precategory-Displayed-Precategory x y = + type-Set (hom-set-total-precategory-Displayed-Precategory x y) + + comp-hom-total-precategory-Displayed-Precategory : + {x y z : obj-total-precategory-Displayed-Precategory} → + hom-total-precategory-Displayed-Precategory y z → + hom-total-precategory-Displayed-Precategory x y → + hom-total-precategory-Displayed-Precategory x z + pr1 (comp-hom-total-precategory-Displayed-Precategory (g , g') (f , f')) = + comp-hom-Precategory 𝒞 g f + pr2 (comp-hom-total-precategory-Displayed-Precategory (g , g') (f , f')) = + comp-hom-Displayed-Precategory 𝒞 𝒟 g f g' f' + + associative-comp-hom-total-precategory-Displayed-Precategory : + {x y z w : obj-total-precategory-Displayed-Precategory} + (h : hom-total-precategory-Displayed-Precategory z w) + (g : hom-total-precategory-Displayed-Precategory y z) + (f : hom-total-precategory-Displayed-Precategory x y) → + ( comp-hom-total-precategory-Displayed-Precategory + ( comp-hom-total-precategory-Displayed-Precategory h g) + ( f)) = + ( comp-hom-total-precategory-Displayed-Precategory + ( h) + ( comp-hom-total-precategory-Displayed-Precategory g f)) + associative-comp-hom-total-precategory-Displayed-Precategory + ( h , h') (g , g') (f , f') = + eq-pair-Σ + ( associative-comp-hom-Precategory 𝒞 h g f) + ( associative-comp-hom-Displayed-Precategory 𝒞 𝒟 h g f h' g' f') + + associative-composition-operation-total-precategory-Displayed-Precategory : + associative-composition-operation-binary-family-Set + ( hom-set-total-precategory-Displayed-Precategory) + associative-composition-operation-total-precategory-Displayed-Precategory = + ( comp-hom-total-precategory-Displayed-Precategory) , + ( λ h g f → + involutive-eq-eq + ( associative-comp-hom-total-precategory-Displayed-Precategory h g f)) + + id-hom-total-precategory-Displayed-Precategory : + {x : obj-total-precategory-Displayed-Precategory} → + hom-total-precategory-Displayed-Precategory x x + pr1 (id-hom-total-precategory-Displayed-Precategory {x , x'}) = + id-hom-Precategory 𝒞 + pr2 (id-hom-total-precategory-Displayed-Precategory {x , x'}) = + id-hom-Displayed-Precategory 𝒞 𝒟 x' + + left-unit-law-comp-hom-total-precategory-Displayed-Precategory : + {x y : obj-total-precategory-Displayed-Precategory} → + (f : hom-total-precategory-Displayed-Precategory x y) → + comp-hom-total-precategory-Displayed-Precategory + ( id-hom-total-precategory-Displayed-Precategory) + ( f) = + f + left-unit-law-comp-hom-total-precategory-Displayed-Precategory (f , f') = + eq-pair-Σ + ( left-unit-law-comp-hom-Precategory 𝒞 f) + ( left-unit-law-comp-hom-Displayed-Precategory 𝒞 𝒟 f f') + + right-unit-law-comp-hom-total-precategory-Displayed-Precategory : + {x y : obj-total-precategory-Displayed-Precategory} → + (f : hom-total-precategory-Displayed-Precategory x y) → + comp-hom-total-precategory-Displayed-Precategory + ( f) + ( id-hom-total-precategory-Displayed-Precategory) = + f + right-unit-law-comp-hom-total-precategory-Displayed-Precategory (f , f') = + eq-pair-Σ + ( right-unit-law-comp-hom-Precategory 𝒞 f) + ( right-unit-law-comp-hom-Displayed-Precategory 𝒞 𝒟 f f') + + is-unital-composition-operation-total-precategory-Displayed-Precategory : + is-unital-composition-operation-binary-family-Set + ( hom-set-total-precategory-Displayed-Precategory) + ( comp-hom-total-precategory-Displayed-Precategory) + pr1 + is-unital-composition-operation-total-precategory-Displayed-Precategory x = + id-hom-total-precategory-Displayed-Precategory + pr1 + ( pr2 + is-unital-composition-operation-total-precategory-Displayed-Precategory) = + left-unit-law-comp-hom-total-precategory-Displayed-Precategory + pr2 + ( pr2 + is-unital-composition-operation-total-precategory-Displayed-Precategory) = + right-unit-law-comp-hom-total-precategory-Displayed-Precategory + + total-precategory-Displayed-Precategory : Precategory (l1 ⊔ l3) (l2 ⊔ l4) + pr1 total-precategory-Displayed-Precategory = + obj-total-precategory-Displayed-Precategory + pr1 (pr2 total-precategory-Displayed-Precategory) = + hom-set-total-precategory-Displayed-Precategory + pr1 (pr2 (pr2 total-precategory-Displayed-Precategory)) = + associative-composition-operation-total-precategory-Displayed-Precategory + pr2 (pr2 (pr2 total-precategory-Displayed-Precategory)) = + is-unital-composition-operation-total-precategory-Displayed-Precategory +``` + +### The fiber precategory of a displayed precategory over an object + +Given a displayed precategory `𝒟` over `𝒞`, the fiber of `𝒟` over `x : obj 𝒞` +defines a precategory. + +```agda +module _ + {l1 l2 l3 l4 : Level} + (𝒞 : Precategory l1 l2) (𝒟 : Displayed-Precategory l3 l4 𝒞) + (c : obj-Precategory 𝒞) + where + + obj-fiber-precategory-Displayed-Precategory : UU l3 + obj-fiber-precategory-Displayed-Precategory = obj-Displayed-Precategory 𝒞 𝒟 c + + hom-set-fiber-precategory-Displayed-Precategory : + (x y : obj-fiber-precategory-Displayed-Precategory) → Set l4 + hom-set-fiber-precategory-Displayed-Precategory = + hom-set-Displayed-Precategory 𝒞 𝒟 (id-hom-Precategory 𝒞 {c}) + + hom-fiber-precategory-Displayed-Precategory : + (x y : obj-fiber-precategory-Displayed-Precategory) → UU l4 + hom-fiber-precategory-Displayed-Precategory x y = + type-Set (hom-set-fiber-precategory-Displayed-Precategory x y) + + comp-hom-fiber-precategory-Displayed-Precategory : + {x y z : obj-fiber-precategory-Displayed-Precategory} → + hom-fiber-precategory-Displayed-Precategory y z → + hom-fiber-precategory-Displayed-Precategory x y → + hom-fiber-precategory-Displayed-Precategory x z + comp-hom-fiber-precategory-Displayed-Precategory {x} {y} {z} g f = + tr + ( λ i → hom-Displayed-Precategory 𝒞 𝒟 i x z) + ( left-unit-law-comp-hom-Precategory 𝒞 (id-hom-Precategory 𝒞)) + ( comp-hom-Displayed-Precategory 𝒞 𝒟 + ( id-hom-Precategory 𝒞) (id-hom-Precategory 𝒞) g f) +``` + +By associativity in `𝒟`, composition in the fiber is dependently associative + +```text + f g h + x ----> y ----> z ----> w + + c ===== c ===== c ===== c +``` + +The proof remains to be formalized. + +```text + associative-comp-hom-fiber-precategory-Displayed-Precategory : + {x y z w : obj-fiber-precategory-Displayed-Precategory} + (h : hom-fiber-precategory-Displayed-Precategory z w) + (g : hom-fiber-precategory-Displayed-Precategory y z) + (f : hom-fiber-precategory-Displayed-Precategory x y) → + ( comp-hom-fiber-precategory-Displayed-Precategory + ( comp-hom-fiber-precategory-Displayed-Precategory h g) + ( f)) = + ( comp-hom-fiber-precategory-Displayed-Precategory + ( h) + ( comp-hom-fiber-precategory-Displayed-Precategory g f)) + associative-comp-hom-fiber-precategory-Displayed-Precategory + {x} {y} {z} {w} h g f = + {! associative-comp-hom-Displayed-Precategory 𝒞 𝒟 _ _ _ h g f !} +``` + +```text + associative-composition-operation-fiber-precategory-Displayed-Precategory : + associative-composition-operation-binary-family-Set + ( hom-set-fiber-precategory-Displayed-Precategory) + pr1 + associative-composition-operation-fiber-precategory-Displayed-Precategory = + comp-hom-fiber-precategory-Displayed-Precategory + pr2 + associative-composition-operation-fiber-precategory-Displayed-Precategory = + associative-comp-hom-fiber-precategory-Displayed-Precategory + + id-hom-fiber-precategory-Displayed-Precategory : + {x : obj-fiber-precategory-Displayed-Precategory} → + hom-fiber-precategory-Displayed-Precategory x x + id-hom-fiber-precategory-Displayed-Precategory {x} = + id-hom-Displayed-Precategory 𝒞 𝒟 x + + left-unit-law-comp-hom-fiber-precategory-Displayed-Precategory : + {x y : obj-fiber-precategory-Displayed-Precategory} → + (f : hom-fiber-precategory-Displayed-Precategory x y) → + comp-hom-fiber-precategory-Displayed-Precategory + ( id-hom-fiber-precategory-Displayed-Precategory) + ( f) = + f + left-unit-law-comp-hom-fiber-precategory-Displayed-Precategory = + left-unit-law-comp-hom-Displayed-Precategory 𝒞 𝒟 (id-hom-Precategory 𝒞 {c}) + + right-unit-law-comp-hom-fiber-precategory-Displayed-Precategory : + {x y : obj-fiber-precategory-Displayed-Precategory} → + (f : hom-fiber-precategory-Displayed-Precategory x y) → + comp-hom-fiber-precategory-Displayed-Precategory + ( f) + ( id-hom-fiber-precategory-Displayed-Precategory) = + f + right-unit-law-comp-hom-fiber-precategory-Displayed-Precategory = + right-unit-law-comp-hom-Displayed-Precategory 𝒞 𝒟 (id-hom-Precategory 𝒞 {c}) + + is-unital-composition-operation-fiber-precategory-Displayed-Precategory : + is-unital-composition-operation-binary-family-Set + ( hom-set-fiber-precategory-Displayed-Precategory) + ( comp-hom-fiber-precategory-Displayed-Precategory) + pr1 + is-unital-composition-operation-fiber-precategory-Displayed-Precategory x = + id-hom-fiber-precategory-Displayed-Precategory + pr1 + ( pr2 + is-unital-composition-operation-fiber-precategory-Displayed-Precategory) = + left-unit-law-comp-hom-fiber-precategory-Displayed-Precategory + pr2 + ( pr2 + is-unital-composition-operation-fiber-precategory-Displayed-Precategory) = + right-unit-law-comp-hom-fiber-precategory-Displayed-Precategory + + fiber-precategory-Displayed-Precategory : Precategory l3 l4 + pr1 fiber-precategory-Displayed-Precategory = + obj-fiber-precategory-Displayed-Precategory + pr1 (pr2 fiber-precategory-Displayed-Precategory) = + hom-set-fiber-precategory-Displayed-Precategory + pr1 (pr2 (pr2 fiber-precategory-Displayed-Precategory)) = + associative-composition-operation-fiber-precategory-Displayed-Precategory + pr2 (pr2 (pr2 fiber-precategory-Displayed-Precategory)) = + is-unital-composition-operation-fiber-precategory-Displayed-Precategory +``` + +## References + +{{#bibliography}} {{#reference AL19}} + +## External links + +- [Displayed Categories](https://1lab.dev/Cat.Displayed.Base.html) at 1lab +- [displayed category](https://ncatlab.org/nlab/show/displayed+category) at + $n$Lab +- [Displayed categories](https://www.epatters.org/wiki/algebra/displayed-categories) + at Evan Patterson's blog + +A wikidata identifier was not available for this concept. diff --git a/src/category-theory/precategories.lagda.md b/src/category-theory/precategories.lagda.md index dc2e72e23a..1eb71cad75 100644 --- a/src/category-theory/precategories.lagda.md +++ b/src/category-theory/precategories.lagda.md @@ -11,6 +11,7 @@ open import category-theory.composition-operations-on-binary-families-of-sets open import category-theory.nonunital-precategories open import category-theory.set-magmoids +open import foundation.action-on-identifications-functions open import foundation.cartesian-product-types open import foundation.dependent-pair-types open import foundation.function-types @@ -316,6 +317,71 @@ module _ ( nonunital-precategory-Precategory C) ``` +### Coherence between the left and right unit law of a precategory + +```agda +module _ + {l1 l2 : Level} (C : Precategory l1 l2) + where + + coh-unit-laws-comp-hom-Precategory : + {x : obj-Precategory C} → + left-unit-law-comp-hom-Precategory C (id-hom-Precategory C {x = x}) = + right-unit-law-comp-hom-Precategory C (id-hom-Precategory C {x = x}) + coh-unit-laws-comp-hom-Precategory {x} = + eq-is-prop + ( is-set-hom-Precategory C x x + ( comp-hom-Precategory C (id-hom-Precategory C) (id-hom-Precategory C)) + ( id-hom-Precategory C)) +``` + +### Coherence between the associativity law and the unit laws of a precategory + +```agda +module _ + {l1 l2 : Level} (C : Precategory l1 l2) + where + + coh-associative-left-unit-law-comp-hom-Precategory : + {x y z : obj-Precategory C} + {f : hom-Precategory C x y} {g : hom-Precategory C y z} → + ( associative-comp-hom-Precategory C (id-hom-Precategory C) g f) ∙ + ( left-unit-law-comp-hom-Precategory C (comp-hom-Precategory C g f)) = + ( ap + ( comp-hom-Precategory' C f) + ( left-unit-law-comp-hom-Precategory C g)) + coh-associative-left-unit-law-comp-hom-Precategory {x} {y} {z} {f} {g} = + eq-is-prop + ( is-set-hom-Precategory C x z + ( comp-hom-Precategory C + ( comp-hom-Precategory C (id-hom-Precategory C) g) + ( f)) + ( comp-hom-Precategory C g f)) + + coh-associative-left-unit-law-comp-hom-Precategory'' : + {x y : obj-Precategory C} {f : hom-Precategory C x y} → + ( associative-comp-hom-Precategory C + ( id-hom-Precategory C) + ( id-hom-Precategory C) + ( f)) ∙ + left-unit-law-comp-hom-Precategory C + ( comp-hom-Precategory C (id-hom-Precategory C) f) ∙ + left-unit-law-comp-hom-Precategory C f = + ( ap + ( comp-hom-Precategory' C f) + ( left-unit-law-comp-hom-Precategory C (id-hom-Precategory C))) ∙ + ( left-unit-law-comp-hom-Precategory C f) + coh-associative-left-unit-law-comp-hom-Precategory'' {x} {y} {f} = + eq-is-prop + ( is-set-hom-Precategory C x y + ( comp-hom-Precategory C + ( comp-hom-Precategory C + ( id-hom-Precategory C) + ( id-hom-Precategory C)) + ( f)) + ( f)) +``` + ## See also - [Categories](category-theory.categories.md) are univalent precategories. diff --git a/src/foundation/dependent-identifications.lagda.md b/src/foundation/dependent-identifications.lagda.md index 0db1b41f3c..fa4dda4374 100644 --- a/src/foundation/dependent-identifications.lagda.md +++ b/src/foundation/dependent-identifications.lagda.md @@ -46,8 +46,7 @@ module _ (p' : dependent-identification B p x' y') (q' : dependent-identification B q x' y') → p' = tr² B α x' ∙ q' → dependent-identification² B α p' q' - map-compute-dependent-identification² refl ._ refl refl = - refl + map-compute-dependent-identification² refl q p' q' = q' map-inv-compute-dependent-identification² : {x y : A} {p q : x = y} (α : p = q) @@ -55,8 +54,7 @@ module _ (p' : dependent-identification B p x' y') (q' : dependent-identification B q x' y') → dependent-identification² B α p' q' → p' = tr² B α x' ∙ q' - map-inv-compute-dependent-identification² refl refl ._ refl = - refl + map-inv-compute-dependent-identification² refl q p' q' = q' is-section-map-inv-compute-dependent-identification² : {x y : A} {p q : x = y} (α : p = q) @@ -65,8 +63,7 @@ module _ (q' : dependent-identification B q x' y') → ( map-compute-dependent-identification² α p' q' ∘ map-inv-compute-dependent-identification² α p' q') ~ id - is-section-map-inv-compute-dependent-identification² refl refl ._ refl = - refl + is-section-map-inv-compute-dependent-identification² refl q p' q' = refl is-retraction-map-inv-compute-dependent-identification² : {x y : A} {p q : x = y} (α : p = q) @@ -75,8 +72,7 @@ module _ (q' : dependent-identification B q x' y') → ( map-inv-compute-dependent-identification² α p' q' ∘ map-compute-dependent-identification² α p' q') ~ id - is-retraction-map-inv-compute-dependent-identification² refl ._ refl refl = - refl + is-retraction-map-inv-compute-dependent-identification² refl q p' q' = refl is-equiv-map-compute-dependent-identification² : {x y : A} {p q : x = y} (α : p = q) @@ -104,9 +100,9 @@ module _ ### The groupoidal structure of dependent identifications -We show that there is groupoidal structure on the dependent identifications. The -statement of the groupoid laws use dependent identifications, due to the -dependent nature of dependent identifications. +We show that there is a dependent groupoidal structure on the dependent +identifications. The statement of the groupoid laws use dependent +identifications, due to the dependent nature of dependent identifications. #### Concatenation of dependent identifications @@ -164,7 +160,7 @@ module _ {x y : A} (p : x = y) {x' : B x} {y' : B y} → dependent-identification B p x' y' → dependent-identification B (inv p) y' x' - inv-dependent-identification refl refl = refl + inv-dependent-identification refl = inv ``` #### Associativity of concatenation of dependent identifications @@ -276,7 +272,7 @@ module _ ( inv p) ( inv-dependent-identification B p q)) ( q) - inv-inv-dependent-identification refl refl = refl + inv-inv-dependent-identification refl = inv-inv ``` ### The inverse distributes over concatenation of dependent identifications diff --git a/src/type-theories/simple-type-theories.lagda.md b/src/type-theories/simple-type-theories.lagda.md index 98461a1a5e..b8e45f3112 100644 --- a/src/type-theories/simple-type-theories.lagda.md +++ b/src/type-theories/simple-type-theories.lagda.md @@ -54,9 +54,9 @@ module simple where coinductive field element : - {X : T} (x : system.element A X) → - fibered-system.element B (f X) x - slice : (X : T) → section-system (fibered-system.slice B (f X)) f + {X : T} (x : system.element A X) → fibered-system.element B (f X) x + slice : + (X : T) → section-system (fibered-system.slice B (f X)) f ------------------------------------------------------------------------------ ```