defn: total products (#459)

This PR implements total products in displayed categories, as a step
towards a nice definition of Hadamard products.

src/Cat/Displayed/Diagram/Total/Product.lagda.md

@@ -0,0 +1,245 @@
+---
+description: |
+  Total products.
+---
+<!--
+```agda
+open import Cat.Diagram.Product
+open import Cat.Displayed.Total
+open import Cat.Displayed.Base
+open import Cat.Prelude
+
+import Cat.Reasoning
+```
+-->
+```agda
+module Cat.Displayed.Diagram.Total.Product where
+```
+
+<!--
+```agda
+open Total-hom
+```
+-->
+
+# Total Products
+
+<!--
+```agda
+module _
+  {ob ℓb oe ℓe} {B : Precategory ob ℓb}
+  (E : Displayed B oe ℓe)
+  where
+  open Cat.Reasoning B
+  open Displayed E
+
+  private variable
+    a x y p : Ob
+    a' x' y' p' : Ob[ a ]
+    f g other : Hom a x
+    f' g' : Hom[ f ] a' x'
+```
+-->
+
+:::{.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
+
+<!--
+```agda
+module _
+  {ob ℓb oe ℓe} {B : Precategory ob ℓb}
+  {E : Displayed B oe ℓe}
+  where
+  open Cat.Reasoning B
+  open Displayed E
+
+  private module ∫E = Cat.Reasoning (∫ E)
+```
+-->
+
+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) π₁ π₂
+```
+
+<details>
+<summary>The proof is largely shuffling data about, so we elide the details.
+</summary>
+```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))
+```
+</details>
+
+::: 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!
+:::

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

src/Cat/Displayed/Instances/Family/Properties.lagda.md

@@ -0,0 +1,81 @@
+---
+description: |
+  Properties of family fibrations.
+---
+<!--
+```agda
+open import Cat.Displayed.Diagram.Total.Product
+open import Cat.Displayed.Instances.Family
+open import Cat.Instances.Sets.Complete
+open import Cat.Diagram.Product
+open import Cat.Displayed.Base
+open import Cat.Prelude
+
+import Cat.Reasoning
+```
+-->
+```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
+
+<!--
+```agda
+module _ {o ℓ κ} (C : Precategory o ℓ) where
+  private
+    module C = Cat.Reasoning C
+    module Fam[C] = Displayed (Family C {κ})
+```
+-->
+
+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)
+```

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.