From 14cdcc9d025db72c8af238c2f9ea0d4d1e64c798 Mon Sep 17 00:00:00 2001 From: Patrick Nicodemus Date: Tue, 14 Nov 2023 23:58:57 -0500 Subject: [PATCH 1/2] Defined the total product of two displayed categories. --- .../Displayed/Instances/TotalProduct.lagda.md | 79 +++++++++++++++++++ 1 file changed, 79 insertions(+) create mode 100644 src/Cat/Displayed/Instances/TotalProduct.lagda.md diff --git a/src/Cat/Displayed/Instances/TotalProduct.lagda.md b/src/Cat/Displayed/Instances/TotalProduct.lagda.md new file mode 100644 index 000000000..473f069a0 --- /dev/null +++ b/src/Cat/Displayed/Instances/TotalProduct.lagda.md @@ -0,0 +1,79 @@ + + +```agda +module Cat.Displayed.Instances.TotalProduct + {o₁ ℓ₁ o₂ ℓ₂ o₃ ℓ₃ o₄ ℓ₄} + (C : Precategory o₁ ℓ₁) + (D : Precategory o₂ ℓ₂) + (EC : Displayed C o₃ ℓ₃) (ED : Displayed D o₄ ℓ₄) where +``` +# The Total Product of Displayed Categories + +If $p : \mathbb{E}C\to C$ and $q :\mathbb{E}D\to \mathbb{D}$ are +displayed categories, then we can define their **total product** +$p \times q : \mathbb{E}C\times \mathbb{E}D\to C\times D$, +which is again a displayed category. The name + +```agda + _×ᵀᴰ_ : Displayed (C ×ᶜ D) (o₃ ⊔ o₄) (ℓ₃ ⊔ ℓ₄) +``` +If displayed categories are regarded as functors, then the product of +displayed categories can be regarded as the usual product of functors. +```agda + _×ᵀᴰ_ .Displayed.Ob[_] p = + Displayed.Ob[ EC ] (fst p) × Displayed.Ob[ ED ] (snd p) + _×ᵀᴰ_ .Displayed.Hom[_] c d e = + Displayed.Hom[ EC ] (fst c) (fst d) (fst e) × + Displayed.Hom[ ED ] (snd c) (snd d) (snd e) + _×ᵀᴰ_ .Displayed.id' = ( Displayed.id' EC , Displayed.id' ED ) +``` + +We establish that the hom sets of the product fibration are actually +sets. + +If $x, y : \operatorname{Ob}[C \times D]$ +(so $x = (x_C, x_D), y = (y_C, y_D)$) and +$f : x \to y$ (so $f$ is $(f_C, f_D)$) +then for any two morphisms $f_1,f_2$ lying over $f$, +and any $p, q : f_1 = f_2$, $p=q$. + +```agda + _×ᵀᴰ_ .Displayed.Hom[_]-set f x' y' = ×-is-hlevel 2 + (Displayed.Hom[ EC ]-set (fst f) (fst x') (fst y')) + (Displayed.Hom[ ED ]-set (snd f) (snd x') (snd y')) +``` +Composition is pairwise. +```agda + _×ᵀᴰ_ .Displayed._∘'_ f g = + EC .Displayed._∘'_ (fst f) (fst g) , + ED .Displayed._∘'_ (snd f) (snd g) +``` + +Associativity and left/right identity laws can be proved +starting from the intuition that paths are functions from +the unit interval: a function into a product $X\times Y$ is a +pair of functions into $X$ and $Y$ respectively. + +```agda + _×ᵀᴰ_ .Displayed.idr' f = λ i → + EC .Displayed.idr' (fst f) i , ED .Displayed.idr' (snd f) i + _×ᵀᴰ_ .Displayed.idl' f = λ i → + EC .Displayed.idl' (fst f) i , ED .Displayed.idl' (snd f) i + _×ᵀᴰ_ .Displayed.assoc' f g h = λ i → + EC .Displayed.assoc' (fst f) (fst g) (fst h) i , + ED .Displayed.assoc' (snd f) (snd g) (snd h) i +``` From e06939d615b770177149217a451e96727c227e0e Mon Sep 17 00:00:00 2001 From: Patrick Nicodemus Date: Wed, 15 Nov 2023 11:43:53 -0500 Subject: [PATCH 2/2] Changes in response to feedback --- .../Displayed/Instances/TotalProduct.lagda.md | 48 +++++++++---------- src/index.lagda.md | 3 ++ 2 files changed, 25 insertions(+), 26 deletions(-) diff --git a/src/Cat/Displayed/Instances/TotalProduct.lagda.md b/src/Cat/Displayed/Instances/TotalProduct.lagda.md index 473f069a0..a4d80299b 100644 --- a/src/Cat/Displayed/Instances/TotalProduct.lagda.md +++ b/src/Cat/Displayed/Instances/TotalProduct.lagda.md @@ -20,13 +20,15 @@ module Cat.Displayed.Instances.TotalProduct (C : Precategory o₁ ℓ₁) (D : Precategory o₂ ℓ₂) (EC : Displayed C o₃ ℓ₃) (ED : Displayed D o₄ ℓ₄) where + private module EC = Displayed EC + private module ED = Displayed ED ``` # The Total Product of Displayed Categories -If $p : \mathbb{E}C\to C$ and $q :\mathbb{E}D\to \mathbb{D}$ are +If $\cE\to \cB$ and $q :\cD \to \cC$ are displayed categories, then we can define their **total product** -$p \times q : \mathbb{E}C\times \mathbb{E}D\to C\times D$, -which is again a displayed category. The name +$\cE\times \cD\to \cB\times \cC$, +which is again a displayed category. ```agda _×ᵀᴰ_ : Displayed (C ×ᶜ D) (o₃ ⊔ o₄) (ℓ₃ ⊔ ℓ₄) @@ -34,12 +36,12 @@ which is again a displayed category. The name If displayed categories are regarded as functors, then the product of displayed categories can be regarded as the usual product of functors. ```agda - _×ᵀᴰ_ .Displayed.Ob[_] p = - Displayed.Ob[ EC ] (fst p) × Displayed.Ob[ ED ] (snd p) - _×ᵀᴰ_ .Displayed.Hom[_] c d e = - Displayed.Hom[ EC ] (fst c) (fst d) (fst e) × - Displayed.Hom[ ED ] (snd c) (snd d) (snd e) - _×ᵀᴰ_ .Displayed.id' = ( Displayed.id' EC , Displayed.id' ED ) + _×ᵀᴰ_ .Displayed.Ob[_] (p₁ , p₂) = + EC.Ob[ p₁ ] × ED.Ob[ p₂ ] + _×ᵀᴰ_ .Displayed.Hom[_] (f₁ , f₂) (c₁ , c₂) (d₁ , d₂) = + EC.Hom[ f₁ ] c₁ d₁ × + ED.Hom[ f₂ ] c₂ d₂ + _×ᵀᴰ_ .Displayed.id' = (EC.id' , ED.id') ``` We establish that the hom sets of the product fibration are actually @@ -52,28 +54,22 @@ then for any two morphisms $f_1,f_2$ lying over $f$, and any $p, q : f_1 = f_2$, $p=q$. ```agda - _×ᵀᴰ_ .Displayed.Hom[_]-set f x' y' = ×-is-hlevel 2 - (Displayed.Hom[ EC ]-set (fst f) (fst x') (fst y')) - (Displayed.Hom[ ED ]-set (snd f) (snd x') (snd y')) + _×ᵀᴰ_ .Displayed.Hom[_]-set (f₁ , f₂) (x'₁ , x'₂) (y'₁ , y'₂) = + ×-is-hlevel 2 + (EC.Hom[ f₁ ]-set x'₁ y'₁) (ED.Hom[ f₂ ]-set x'₂ y'₂) ``` Composition is pairwise. ```agda - _×ᵀᴰ_ .Displayed._∘'_ f g = - EC .Displayed._∘'_ (fst f) (fst g) , - ED .Displayed._∘'_ (snd f) (snd g) + _×ᵀᴰ_ .Displayed._∘'_ (f₁ , f₂) (g₁ , g₂) = + EC._∘'_ f₁ g₁ , ED._∘'_ f₂ g₂ ``` -Associativity and left/right identity laws can be proved -starting from the intuition that paths are functions from -the unit interval: a function into a product $X\times Y$ is a -pair of functions into $X$ and $Y$ respectively. +Associativity and left/right identity laws hold because +they hold for the components of the ordered pairs. ```agda - _×ᵀᴰ_ .Displayed.idr' f = λ i → - EC .Displayed.idr' (fst f) i , ED .Displayed.idr' (snd f) i - _×ᵀᴰ_ .Displayed.idl' f = λ i → - EC .Displayed.idl' (fst f) i , ED .Displayed.idl' (snd f) i - _×ᵀᴰ_ .Displayed.assoc' f g h = λ i → - EC .Displayed.assoc' (fst f) (fst g) (fst h) i , - ED .Displayed.assoc' (snd f) (snd g) (snd h) i + _×ᵀᴰ_ .Displayed.idr' (f₁ , f₂) = EC.idr' f₁ ,ₚ ED.idr' f₂ + _×ᵀᴰ_ .Displayed.idl' (f₁ , f₂) = EC.idl' f₁ ,ₚ ED.idl' f₂ + _×ᵀᴰ_ .Displayed.assoc' (f₁ , f₂) (g₁ , g₂) (h₁ , h₂) = + EC.assoc' f₁ g₁ h₁ ,ₚ ED.assoc' f₂ g₂ h₂ ``` diff --git a/src/index.lagda.md b/src/index.lagda.md index 7ecdad566..7e2e1edc9 100644 --- a/src/index.lagda.md +++ b/src/index.lagda.md @@ -679,6 +679,9 @@ open import Cat.Displayed.Instances.Elements -- The category of elements of a presheaf, instantiated as being -- displayed over the domain. +open import Cat.Displayed.Instances.TotalProduct +-- The total product of two displayed categories. + open import Cat.Displayed.Composition -- Composition of displayed categories ```