diff --git a/src/Cat/Displayed/Diagram/Total/Product.lagda.md b/src/Cat/Displayed/Diagram/Total/Product.lagda.md new file mode 100644 index 000000000..66039bd2a --- /dev/null +++ b/src/Cat/Displayed/Diagram/Total/Product.lagda.md @@ -0,0 +1,245 @@ +--- +description: | + Total products. +--- + +```agda +module Cat.Displayed.Diagram.Total.Product where +``` + + + +# Total Products + + + +:::{.definition #total-product-diagram} +Let $\cE \liesover \cB$ be a [[displayed category]], and +$P, \pi_1 : P \to X, \pi_2 : P \to Y$ be a [[product diagram|product]] in $\cB$. +A diagram $P', \pi_{1}', \pi_{2}'$ of the shape + +~~~{.quiver} +\begin{tikzcd} + {P'} && {Y'} \\ + & {X'} \\ + P && Y \\ + & X + \arrow["{\pi_2'}"{description, pos=0.4}, from=1-1, to=1-3] + \arrow["{\pi_1'}"{description}, from=1-1, to=2-2] + \arrow[from=1-1, lies over, to=3-1] + \arrow[from=1-3, lies over, to=3-3] + \arrow[from=2-2, lies over, to=4-2] + \arrow["{\pi_2}"{description, pos=0.3}, from=3-1, to=3-3] + \arrow["{\pi_1}"{description}, from=3-1, to=4-2] +\end{tikzcd} +~~~ + +is a **total product diagram** if it satisfies a displayed version of the +universal property of the product. + + +```agda + record is-total-product + {π₁ : Hom p x} {π₂ : Hom p y} + (prod : is-product B π₁ π₂) + (π₁' : Hom[ π₁ ] p' x') (π₂' : Hom[ π₂ ] p' y') + : Type (ob ⊔ ℓb ⊔ oe ⊔ ℓe) + where + no-eta-equality + open is-product prod +``` + +More explicitly, suppose that we had a triple $(A', f', g')$ displayed +over $(A, f, g)$, as in the following diagram. + +~~~{.quiver} +\begin{tikzcd} + \textcolor{rgb,255:red,92;green,92;blue,214}{{A'}} \\ + && {P'} && {Y'} \\ + \textcolor{rgb,255:red,92;green,92;blue,214}{A} &&& {X'} \\ + && P && Y \\ + &&& X + \arrow[color={rgb,255:red,92;green,92;blue,214}, curve={height=-12pt}, from=1-1, to=2-5] + \arrow[color={rgb,255:red,92;green,92;blue,214}, lies over, from=1-1, to=3-1] + \arrow["{f'}"{description}, color={rgb,255:red,92;green,92;blue,214}, curve={height=18pt}, from=1-1, to=3-4] + \arrow["{\pi_2'}"{description, pos=0.4}, from=2-3, to=2-5] + \arrow["{\pi_1'}"{description}, from=2-3, to=3-4] + \arrow[from=2-3, lies over, to=4-3] + \arrow[from=2-5, lies over, to=4-5] + \arrow["g"{description, pos=0.3}, color={rgb,255:red,92;green,92;blue,214}, curve={height=-12pt}, from=3-1, to=4-5] + \arrow["f"{description}, color={rgb,255:red,92;green,92;blue,214}, curve={height=18pt}, from=3-1, to=5-4] + \arrow[from=3-4, lies over, to=5-4] + \arrow["{\pi_2}"{description, pos=0.3}, from=4-3, to=4-5] + \arrow["{\pi_1}"{description}, from=4-3, to=5-4] +\end{tikzcd} +~~~ + +$P$ is a product, so there exists a unique $\langle f, g \rangle : A \to P$ +that commutes with $\pi_1$ and $\pi_2$. + +~~~{.quiver} +\begin{tikzcd} + \textcolor{rgb,255:red,92;green,92;blue,214}{{A'}} \\ + && {P'} && {Y'} \\ + \textcolor{rgb,255:red,92;green,92;blue,214}{A} &&& {X'} \\ + && P && Y \\ + &&& X + \arrow[color={rgb,255:red,92;green,92;blue,214}, curve={height=-12pt}, from=1-1, to=2-5] + \arrow[color={rgb,255:red,92;green,92;blue,214}, lies over, from=1-1, to=3-1] + \arrow["{f'}"{description}, color={rgb,255:red,92;green,92;blue,214}, curve={height=18pt}, from=1-1, to=3-4] + \arrow["{\pi_2'}"{description, pos=0.4}, from=2-3, to=2-5] + \arrow["{\pi_1'}"{description}, from=2-3, to=3-4] + \arrow[from=2-3, lies over, to=4-3] + \arrow[from=2-5, lies over, to=4-5] + \arrow["{\langle f,g \rangle}"{description}, color={rgb,255:red,214;green,92;blue,92}, from=3-1, to=4-3] + \arrow["g"{description, pos=0.3}, color={rgb,255:red,92;green,92;blue,214}, curve={height=-12pt}, from=3-1, to=4-5] + \arrow["f"{description}, color={rgb,255:red,92;green,92;blue,214}, curve={height=18pt}, from=3-1, to=5-4] + \arrow[from=3-4, lies over, to=5-4] + \arrow["{\pi_2}"{description, pos=0.3}, from=4-3, to=4-5] + \arrow["{\pi_1}"{description}, from=4-3, to=5-4] +\end{tikzcd} +~~~ + +This leaves a conspicuous gap in the upstairs portion of the diagram between +$A'$ and $P'$; $(P', \pi_1', \pi_2')$ is a total product precisely when we +have a unique lift of $\langle f, g \rangle$ that commutes with $\pi_1'$ +and $\pi_2'$. + + +```agda + field + ⟨_,_⟩' + : (f' : Hom[ f ] a' x') (g' : Hom[ g ] a' y') + → Hom[ ⟨ f , g ⟩ ] a' p' + π₁∘⟨⟩' + : π₁' ∘' ⟨ f' , g' ⟩' ≡[ π₁∘⟨⟩ ] f' + π₂∘⟨⟩' + : π₂' ∘' ⟨ f' , g' ⟩' ≡[ π₂∘⟨⟩ ] g' + unique' + : {p1 : π₁ ∘ other ≡ f} {p2 : π₂ ∘ other ≡ g} + → {other' : Hom[ other ] a' p'} + → (p1' : (π₁' ∘' other') ≡[ p1 ] f') + → (p2' : (π₂' ∘' other') ≡[ p2 ] g') + → other' ≡[ unique p1 p2 ] ⟨ f' , g' ⟩' +``` +::: + +:::{.definition #total-product} +A **total product** of $A'$ and $B'$ in $\cE$ consists of a choice +of a total product diagram. +::: + + +```agda + record Total-product + {x y} + (prod : Product B x y) + (x' : Ob[ x ]) (y' : Ob[ y ]) + : Type (ob ⊔ ℓb ⊔ oe ⊔ ℓe) where + no-eta-equality + open Product prod + field + apex' : Ob[ apex ] + π₁' : Hom[ π₁ ] apex' x' + π₂' : Hom[ π₂ ] apex' y' + has-is-total-product : is-total-product has-is-product π₁' π₂' + + open is-total-product has-is-total-product +``` + +## Total products and total categories + + + +As the name suggests, a total product diagram in $\cE$ induces +to a product diagram in the [[total category]] of $\cE$. + +```agda + is-total-product→total-is-product + : ∀ {x y p} {x' : Ob[ x ]} {y' : Ob[ y ]} {p' : Ob[ p ]} + → {π₁ : ∫E.Hom (p , p') (x , x')} {π₂ : ∫E.Hom (p , p') (y , y')} + → {prod : is-product B (π₁ .hom) (π₂ .hom)} + → is-total-product E prod (π₁ .preserves) (π₂ .preserves) + → is-product (∫ E) π₁ π₂ +``` + +
+The proof is largely shuffling data about, so we elide the details. + +```agda + is-total-product→total-is-product {π₁ = π₁} {π₂ = π₂} {prod = prod} total-prod = ∫prod where + open is-product prod + open is-total-product total-prod + + ∫prod : is-product (∫ E) π₁ π₂ + ∫prod .is-product.⟨_,_⟩ f g = + total-hom ⟨ f .hom , g .hom ⟩ ⟨ f .preserves , g .preserves ⟩' + ∫prod .is-product.π₁∘⟨⟩ = + total-hom-path E π₁∘⟨⟩ π₁∘⟨⟩' + ∫prod .is-product.π₂∘⟨⟩ = + total-hom-path E π₂∘⟨⟩ π₂∘⟨⟩' + ∫prod .is-product.unique p1 p2 = + total-hom-path E + (unique (ap hom p1) (ap hom p2)) + (unique' (ap preserves p1) (ap preserves p2)) +``` +
+ +::: warning +Note that a product diagram in a total category does **not** necessarily +yield a product diagram in the base category. For a counterexample, consider +the following displayed category: + +~~~{.quiver} +\begin{tikzcd} + \bullet \\ + \\ + \bullet + \arrow[from=1-1, lies over, to=3-1] + \arrow["f"', from=3-1, to=3-1, loop, in=305, out=235, distance=10mm] +\end{tikzcd} +~~~ + +The total category is equivalent to the [[terminal category]], and thus has +products. However, the base category does not have products, as the uniqueness +condition fails! +::: diff --git a/src/Cat/Displayed/Instances/Family.lagda.md b/src/Cat/Displayed/Instances/Family.lagda.md index 0f1af00e5..1746d1334 100644 --- a/src/Cat/Displayed/Instances/Family.lagda.md +++ b/src/Cat/Displayed/Instances/Family.lagda.md @@ -30,7 +30,7 @@ open _=>_ ``` --> -# The family fibration +# The family fibration {defines="family-fibration"} We can canonically treat any `Precategory`{.Agda} $\mathcal{C}$ as being displayed over `Sets`{.Agda}, regardless of the size of the object- and diff --git a/src/Cat/Displayed/Instances/Family/Properties.lagda.md b/src/Cat/Displayed/Instances/Family/Properties.lagda.md new file mode 100644 index 000000000..447bcfe70 --- /dev/null +++ b/src/Cat/Displayed/Instances/Family/Properties.lagda.md @@ -0,0 +1,81 @@ +--- +description: | + Properties of family fibrations. +--- + +```agda +module Cat.Displayed.Instances.Family.Properties where +``` + +# Properties of family fibrations + +This module proves a collection of useful properties about the [[family fibration]]. + +# Total products + + + +A [[total product]] in the family fibration of $\cC$ corresponds to a family +of [[products]] in $\cC$. + +```agda + fam-total-product + : ∀ {I J : Set κ} {Xᵢ : ⌞ I ⌟ → C.Ob} {Yⱼ : ⌞ J ⌟ → C.Ob} + → (∀ i j → Product C (Xᵢ i) (Yⱼ j)) + → Total-product (Family C) (Sets-products I J) Xᵢ Yⱼ +``` + +All of the relevant morphisms come directly from products in $\cC$. + +```agda + fam-total-product {I = I} {J = J} {Xᵢ = Xᵢ} {Yⱼ = Yⱼ} C-prods = total-prod where + open is-total-product + open Total-product + + module _ i j where + open Product (C-prods i j) renaming (apex to Xᵢ×Yⱼ) using () public + + module _ {i j} where + open Product (C-prods i j) hiding (apex) public + + total-prod : Total-product (Family C) (Sets-products I J) Xᵢ Yⱼ + total-prod .apex' (i , j) = Xᵢ×Yⱼ i j + total-prod .π₁' (i , j) = π₁ + total-prod .π₂' (i , j) = π₂ + total-prod .has-is-total-product .⟨_,_⟩' fₖ gₖ k = ⟨ fₖ k , gₖ k ⟩ +``` + +The $\beta$ laws are easy applications of function extensionality, but +the $\eta$ law requires a bit of cubical-fu to get the types to line +up. + +```agda + total-prod .has-is-total-product .π₁∘⟨⟩' = ext (λ k → π₁∘⟨⟩) + total-prod .has-is-total-product .π₂∘⟨⟩' = ext (λ k → π₂∘⟨⟩) + total-prod .has-is-total-product .unique' {a' = Zₖ} {p1 = p1} {p2 = p2} {other' = other'} p q i k = + unique + (coe0→i (λ i → π₁ C.∘ other-line k i ≡ p i k) i refl) + (coe0→i (λ i → π₂ C.∘ other-line k i ≡ q i k) i refl) + i + where + other-line : ∀ k i → C.Hom (Zₖ k) (Xᵢ×Yⱼ (p1 i k) (p2 i k)) + other-line k i = coe0→i (λ i → C.Hom (Zₖ k) (Xᵢ×Yⱼ (p1 i k) (p2 i k))) i (other' k) +``` diff --git a/src/Cat/Displayed/Instances/Simple.lagda.md b/src/Cat/Displayed/Instances/Simple.lagda.md index 7ff51af9e..30ad13232 100644 --- a/src/Cat/Displayed/Instances/Simple.lagda.md +++ b/src/Cat/Displayed/Instances/Simple.lagda.md @@ -25,7 +25,7 @@ open Cat.Reasoning B open Binary-products B has-prods ``` -# Simple fibrations +# Simple fibrations {defines="simple-fibration"} One reason to be interested in fibrations is that they provide an excellent setting to study logical and type-theoretical phenomena. diff --git a/src/Cat/Displayed/Instances/Simple/Properties.lagda.md b/src/Cat/Displayed/Instances/Simple/Properties.lagda.md new file mode 100644 index 000000000..f3b095f7e --- /dev/null +++ b/src/Cat/Displayed/Instances/Simple/Properties.lagda.md @@ -0,0 +1,74 @@ +--- +description: | + Properties of simple fibrations. +--- + +```agda +module Cat.Displayed.Instances.Simple.Properties + {o ℓ} (B : Precategory o ℓ) + (has-prods : ∀ X Y → Product B X Y) + where +``` + + + +# Properties of simple fibrations + +This module collects some useful properties of [[simple fibrations]]. + +## Total products in simple fibrations + +Every simple fibration has all [[total products]]. + +```agda +simple-total-product + : ∀ {Γ Δ A B : Ob} + → Total-product Simple[B] (has-prods Γ Δ) A B +``` + +```agda +simple-total-product {Γ} {Δ} {A} {B} = total-prod where + open is-total-product + open Total-product + + total-prod : Total-product Simple[B] (has-prods Γ Δ) A B +``` + +The apex of the total product is simply given by a product in $\cB$. +We can obtain the projections $(\Gamma \times \Delta) \times (A \times B) \to A$ +and $(\Gamma \times \Delta) \times (A \times B) \to B$ by composing projections. + +```agda + total-prod .apex' = A ⊗₀ B + total-prod .π₁' = π₁ ∘ π₂ + total-prod .π₂' = π₂ ∘ π₂ +``` + +The universal property follows from some straightforward algebra. + +```agda + total-prod .has-is-total-product .⟨_,_⟩' f g = ⟨ f , g ⟩ + total-prod .has-is-total-product .π₁∘⟨⟩' = + pullr π₂∘⟨⟩ ∙ π₁∘⟨⟩ + total-prod .has-is-total-product .π₂∘⟨⟩' = + pullr π₂∘⟨⟩ ∙ π₂∘⟨⟩ + total-prod .has-is-total-product .unique' p q = + ⟨⟩-unique (pushr (sym π₂∘⟨⟩) ∙ p) (pushr (sym π₂∘⟨⟩) ∙ q) +``` diff --git a/src/Cat/Displayed/Instances/Slice/Properties.lagda.md b/src/Cat/Displayed/Instances/Slice/Properties.lagda.md new file mode 100644 index 000000000..679a97c32 --- /dev/null +++ b/src/Cat/Displayed/Instances/Slice/Properties.lagda.md @@ -0,0 +1,81 @@ +--- +description: | + +--- + +```agda +module Cat.Displayed.Instances.Slice.Properties where +``` + +# Properties of slice categories + +This module gathers together some useful properties of [[slice categories]]. + + + +## Total products in slice categories + +A [[total product]] in a slice category is given by a [[product]] of +the domains of the slices. + +```agda + slice-total-product + : ∀ {I J X Y} {f : Hom X I} {g : Hom Y J} + → (X×Y : Product B X Y) + → (I×J : Product B I J) + → Total-product (Slices B) I×J (cut f) (cut g) + slice-total-product {f = f} {g = g} X×Y I×J = total-prod where + open is-total-product + open Total-product + + module X×Y = Product X×Y + module I×J = Product I×J + + total-prod : Total-product (Slices B) I×J (cut f) (cut g) + total-prod .apex' .domain = X×Y.apex + total-prod .apex' .map = I×J.⟨ f ∘ X×Y.π₁ , g ∘ X×Y.π₂ ⟩ + total-prod .π₁' .to = X×Y.π₁ + total-prod .π₁' .commute = I×J.π₁∘⟨⟩ + total-prod .π₂' .to = X×Y.π₂ + total-prod .π₂' .commute = I×J.π₂∘⟨⟩ +``` + +The universal property follows from a bit of routine algebra involving +products. + +```agda + total-prod .has-is-total-product .⟨_,_⟩' f g .to = X×Y.⟨ f. to , g .to ⟩ + total-prod .has-is-total-product .⟨_,_⟩' f g .commute = + I×J.unique₂ + (pulll I×J.π₁∘⟨⟩ ∙ f .commute) + (pulll I×J.π₂∘⟨⟩ ∙ g .commute) + (pulll I×J.π₁∘⟨⟩ ∙ pullr X×Y.π₁∘⟨⟩) + (pulll I×J.π₂∘⟨⟩ ∙ pullr X×Y.π₂∘⟨⟩) + total-prod .has-is-total-product .π₁∘⟨⟩' = + Slice-pathp B _ X×Y.π₁∘⟨⟩ + total-prod .has-is-total-product .π₂∘⟨⟩' = + Slice-pathp B _ X×Y.π₂∘⟨⟩ + total-prod .has-is-total-product .unique' p q = + Slice-pathp B _ (X×Y.unique (λ i → p i .to) λ i → q i .to) +``` diff --git a/src/Cat/Instances/Poly.lagda.md b/src/Cat/Instances/Poly.lagda.md index 605db1b6f..129ebf79d 100644 --- a/src/Cat/Instances/Poly.lagda.md +++ b/src/Cat/Instances/Poly.lagda.md @@ -41,17 +41,22 @@ $$ [family fibration]: Cat.Displayed.Instances.Family.html ```agda -Poly : ∀ ℓ → Precategory (lsuc ℓ) ℓ -Poly ℓ = ∫ {ℓ = ℓ} (Family (Sets ℓ ^op)) +Poly : ∀ ℓ ℓ' → Precategory (lsuc ℓ ⊔ lsuc ℓ') (ℓ ⊔ ℓ') +Poly ℓ ℓ' = ∫ (Family (Sets ℓ' ^op) {ℓ = ℓ}) -module Poly {ℓ} = Cat.Reasoning (Poly ℓ) +module Poly where + module _ ℓ ℓ' where + open Precategory (Poly ℓ ℓ') using (Ob) public + + module _ {ℓ ℓ'} where + open Cat.Reasoning (Poly ℓ ℓ') hiding (Ob) public ``` Our standard toolkit for showing [[univalence of total categories]] applies here: ```agda -Poly-is-category : ∀ {ℓ} → is-category (Poly ℓ) +Poly-is-category : ∀ {ℓ ℓ'} → is-category (Poly ℓ ℓ') Poly-is-category = is-category-total _ Sets-is-category $ is-category-fibrewise' _ @@ -64,9 +69,11 @@ are given by pairs of a reindexing together with a contravariant action on the families. It is _so_ mechanical that we can do it automatically: ```agda -poly-maps : ∀ {ℓ} {A B} → Iso - (Poly.Hom {ℓ} A B) - (Σ[ f ∈ (⌞ A ⌟ → ⌞ B ⌟) ] (∀ x → B .snd ʻ f x → A .snd ʻ x)) +poly-maps + : ∀ {ℓ ℓ'} {A B : Poly.Ob ℓ ℓ'} + → Iso + (Poly.Hom A B) + (Σ[ f ∈ (⌞ A ⌟ → ⌞ B ⌟) ] (∀ x → B .snd ʻ f x → A .snd ʻ x)) unquoteDef poly-maps = define-record-iso poly-maps (quote Total-hom) ``` @@ -75,7 +82,7 @@ using regularity: ```agda poly-map-path - : ∀ {ℓ A B} {f g : Poly.Hom {ℓ} A B} + : ∀ {ℓ ℓ'} {A B : Poly.Ob ℓ ℓ'} {f g : Poly.Hom A B} → (hom≡ : f .hom ≡ g .hom) → (pre≡ : ∀ a b → f .preserves a (subst (λ hom → B .snd ʻ hom a) (sym hom≡) b) ≡ g .preserves a b) @@ -93,7 +100,7 @@ possible to evaluate it at a set $X$ and get back a set. We take the interpretation above _literally_: ```agda -Polynomial-functor : ∀ {ℓ} → Poly.Ob {ℓ} → Functor (Sets ℓ) (Sets ℓ) +Polynomial-functor : ∀ {ℓ ℓ'} → Poly.Ob ℓ ℓ' → Functor (Sets ℓ) (Sets (ℓ ⊔ ℓ')) Polynomial-functor (I , A) .F₀ X = el (Σ[ i ∈ I ] (A ʻ i → ⌞ X ⌟)) (hlevel 2) Polynomial-functor (I , A) .F₁ f (a , g) = a , λ z → f (g z) Polynomial-functor (I , A) .F-id = refl @@ -116,9 +123,10 @@ we recover the usual definition of the Haskell type `Lens s t a b`: Lens : ∀ {ℓ} (S T A B : Set ℓ) → Type ℓ Lens S T A B = Poly.Hom (S , λ _ → T) (A , λ _ → B) -_ : ∀ {ℓ} {S T A B : Set ℓ} → Iso - (Lens S T A B) - ((∣ S ∣ → ∣ A ∣) × (∣ S ∣ → ∣ B ∣ → ∣ T ∣)) +_ : ∀ {ℓ} {S T A B : Set ℓ} + → Iso + (Lens S T A B) + ((∣ S ∣ → ∣ A ∣) × (∣ S ∣ → ∣ B ∣ → ∣ T ∣)) _ = poly-maps ```