Dependent products in categories

src/Cat/Diagram/DependentProduct.lagda.md

@@ -0,0 +1,168 @@
+<!--
+```agda
+open import Cat.CartesianClosed.Locally
+open import Cat.Diagram.Limit.Finite
+open import Cat.Functor.Pullback
+open import Cat.Functor.Adjoint
+open import Cat.Instances.Slice
+open import Cat.Prelude
+
+import Cat.Reasoning
+```
+-->
+
+```agda
+module Cat.Diagram.DependentProduct
+  {o ℓ} (C : Precategory o ℓ) (fc : Finitely-complete C) where
+```
+
+# Dependent products {defines="dependent-product"}
+
+Analogously to [[Exponential Objects]], we can define **dependent
+products** in a category. We mimic the design of the module
+[`Cat.Diagram.Exponential`](Cat.Diagram.Exponential.html).
+
+<!--
+```agda
+open Cat.Reasoning C
+open Finitely-complete fc
+```
+-->
+
+```agda
+module _ {A B : Ob} {f : Hom A B} where
+  private
+    module C/A = Cat.Reasoning (Slice C A)
+    module C/B = Cat.Reasoning (Slice C B)
+    module pb = Functor (Base-change pullbacks f)
+  record is-dependent-product {X : C/A.Ob}
+    (Π : C/B.Ob) (ev : C/A.Hom (pb.₀ Π) X) : Type (o ⊔ ℓ) where
+    no-eta-equality
+    field
+      ƛ        : ∀ {Γ} (m : C/A.Hom (pb.₀ Γ) X) → C/B.Hom Γ Π
+      commutes : ∀ {Γ} (m : C/A.Hom (pb.₀ Γ) X) → ev C/A.∘ pb.₁ (ƛ m) ≡ m
+      unique
+        : ∀ {Γ} {m : C/A.Hom (pb.₀ Γ) X} m'
+        → ev C/A.∘ pb.₁ m' ≡ m
+        → m' ≡ ƛ m
+```
+
+Just as exponentiation induces an equivalence between
+$\hom_\cC(\Gamma, B^A)$ and $\hom_\cC(A × \Gamma, B)$,
+dependent products induce an equivalence between
+$\hom_{\cC/B}(\Gamma, \prod_f X)$ and
+$\hom_{\cC/A}(A \times_B \Gamma, X)$.
+
+```agda
+    unlambda : ∀ {C} (m : C/B.Hom C Π) → C/A.Hom (pb.₀ C) X
+    unlambda m = ev C/A.∘ pb.₁ m
+
+    lambda-is-equiv : ∀ {C} → is-equiv (ƛ {C})
+    lambda-is-equiv .is-eqv x .centre = unlambda x , sym (unique x refl)
+    lambda-is-equiv .is-eqv x .paths (y , p) =
+      Σ-prop-path! (ap unlambda (sym p) ∙ commutes y)
+```
+
+<!--
+```agda
+    unique₂
+      : ∀ {C} {m : C/A.Hom (pb.₀ C) _} m₁ m₂
+      → ev C/A.∘ pb.₁ m₁ ≡ m
+      → ev C/A.∘ pb.₁ m₂ ≡ m
+      → m₁ ≡ m₂
+    unique₂ _ _ p q = unique _ p ∙ sym (unique _ q)
+
+    lambda-ev : ƛ ev ≡ C/B.id
+    lambda-ev = sym (unique C/B.id (C/A.elimr pb.F-id))
+
+  module _ where
+    is-dependent-product-is-prop
+      : ∀ {X Π ev} → is-prop (is-dependent-product {X} Π ev)
+    is-dependent-product-is-prop {X} {Π} {ev} x y = q where
+      open is-dependent-product
+
+      p : Path (∀ {C} m → C/B.Hom C Π) (x .ƛ) (y .ƛ)
+      p i m = y .unique (x .ƛ m) (x .commutes m) i
+
+      q : x ≡ y
+      q i .is-dependent-product.ƛ = p i
+      q i .is-dependent-product.commutes m =
+        is-prop→pathp (λ i → C/A.Hom-set _ _ (ev C/A.∘ pb.₁ (p i m)) m)
+          (x .commutes m) (y .commutes m) i
+      q i .is-dependent-product.unique {m = m} m' q =
+        is-prop→pathp (λ i → C/B.Hom-set _ _ m' (p i m))
+          (x .unique m' q) (y .unique m' q) i
+```
+-->
+
+We bundle this data together.
+
+```agda
+record DependentProduct {A B : Ob} (f : Hom A B) (X : /-Obj {C = C} A) :
+  Type (o ⊔ ℓ) where
+  field
+    Π : /-Obj {C = C} B
+    ev : /-Hom (Base-change pullbacks f .Functor.F₀ Π) X
+    has-is-Π : is-dependent-product Π ev
+  open is-dependent-product has-is-Π public
+```
+
+## Exponentiable Maps {defines=exponentiable-map}
+
+A map $f : A \xto{\cC} B$ is **exponentiable** if $\prod_f X$ exists for
+every $X : \cC/A$. Such a map induces a dependent product *functor*,
+$\prod_f : \cC/A \to \cC/B$, right adjoint to the [[pullback functor]]
+$A \times_B - : \cC/B \to \cC/A$.
+
+<!--
+```agda
+module _ {A B : Ob} (f : Hom A B) (dp : ∀ X → DependentProduct f X) where
+  private
+    module C/A = Cat.Reasoning (Slice C A)
+    module C/B = Cat.Reasoning (Slice C B)
+    module pb = Functor (Base-change pullbacks f)
+    module _ {X} where open DependentProduct (dp X) public
+```
+-->
+
+```agda
+  Πf : Functor (Slice C A) (Slice C B)
+  Πf .Functor.F₀ X = Π {X}
+  Πf .Functor.F₁ h = ƛ (h C/A.∘ ev)
+  Πf .Functor.F-id = ap ƛ (C/A.idl ev) ∙ lambda-ev
+  Πf .Functor.F-∘ f g = sym $ unique _ $
+    ev C/A.∘ pb.₁ (ƛ (f C/A.∘ ev) C/B.∘ ƛ (g C/A.∘ ev))         ≡⟨ C/A.refl⟩∘⟨ pb.F-∘ _ _ ⟩
+    ev C/A.∘ pb.₁ (ƛ (f C/A.∘ ev)) C/A.∘ pb.₁ (ƛ (g C/A.∘ ev))  ≡⟨ C/A.extendl (commutes _) ⟩
+    f C/A.∘ ev C/A.∘ pb.₁ (ƛ (g C/A.∘ ev))                      ≡⟨ C/A.refl⟩∘⟨ commutes _ ⟩
+    f C/A.∘ g C/A.∘ ev                                          ≡⟨ C/A.assoc _ _ _ ⟩
+    (f C/A.∘ g) C/A.∘ ev
+    ∎
+
+  f*⊣Πf : Base-change pullbacks f ⊣ Πf
+  f*⊣Πf ._⊣_.unit ._=>_.η _ = ƛ C/A.id
+  f*⊣Πf ._⊣_.unit ._=>_.is-natural x y f = unique₂ _ _
+    ( ev C/A.∘ pb.₁ (ƛ C/A.id C/B.∘ f)                          ≡⟨ C/A.refl⟩∘⟨ pb.F-∘ _ _ ⟩
+      ev C/A.∘ pb.₁ (ƛ C/A.id) C/A.∘ pb.₁ f                     ≡⟨ C/A.cancell (commutes _) ⟩
+      pb.₁ f                                                    ∎)
+    ( ev C/A.∘ pb.₁ (ƛ (pb.₁ f C/A.∘ ev) C/B.∘ ƛ C/A.id)        ≡⟨ C/A.refl⟩∘⟨ pb.F-∘ _ _ ⟩
+      ev C/A.∘ pb.₁ (ƛ (pb.₁ f C/A.∘ ev)) C/A.∘ pb.₁ (ƛ C/A.id) ≡⟨ C/A.extendl (commutes _) ⟩
+      pb.₁ f C/A.∘ ev C/A.∘ pb.₁ (ƛ C/A.id)                     ≡⟨ C/A.elimr (commutes _) ⟩
+      pb.₁ f                                                    ∎)
+  f*⊣Πf ._⊣_.counit ._=>_.η _ = ev
+  f*⊣Πf ._⊣_.counit ._=>_.is-natural x y f = commutes _
+  f*⊣Πf ._⊣_.zig = commutes _
+  f*⊣Πf ._⊣_.zag = unique₂ _ _
+    ( ev C/A.∘ pb.₁ (ƛ (ev C/A.∘ ev) C/B.∘ ƛ C/A.id)            ≡⟨ C/A.refl⟩∘⟨ pb.F-∘ _ _ ⟩
+      ev C/A.∘ pb.₁ (ƛ (ev C/A.∘ ev)) C/A.∘ pb.₁ (ƛ C/A.id)     ≡⟨ C/A.extendl (commutes _) ⟩
+      ev C/A.∘ ev C/A.∘ pb.₁ (ƛ C/A.id)                         ≡⟨ C/A.elimr (commutes _) ⟩
+      ev                                                        ∎)
+    (C/A.elimr pb.F-id)
+```
+
+In particular, if all morphisms are exponentiable, then the category is
+[[locally cartesian closed]].
+
+```agda
+dependent-products→lccc : (∀ {A B} (f : Hom A B) X → DependentProduct f X) → Locally-cartesian-closed C
+dependent-products→lccc dp = dependent-product→lcc C fc (λ f → Πf f (dp f)) (λ f → f*⊣Πf f (dp f))
+```

src/Cat/Instances/Presheaf/DependentProducts.lagda.md

@@ -0,0 +1,166 @@
+<!--
+```agda
+open import Cat.Instances.Presheaf.Limits
+open import Cat.Diagram.DependentProduct
+open import Cat.CartesianClosed.Locally
+open import Cat.Diagram.Limit.Finite
+open import Cat.Functor.Hom.Yoneda
+open import Cat.Functor.Pullback
+open import Cat.Instances.Slice
+open import Cat.Functor.Base
+open import Cat.Functor.Hom
+open import Cat.Prelude
+
+import Cat.Reasoning
+```
+-->
+
+```agda
+module Cat.Instances.Presheaf.DependentProducts
+  {o} ℓ (C : Precategory o (o ⊔ ℓ)) where
+```
+
+<!--
+```agda
+private
+  module C = Cat.Reasoning C
+  module PSh where
+    open Cat.Reasoning (PSh (o ⊔ ℓ) C) public
+    open Finitely-complete (PSh-finite-limits (o ⊔ ℓ) C) public
+  fc = PSh-finite-limits (o ⊔ ℓ) C
+
+  open Functor
+  open _=>_
+  open /-Obj
+  open /-Hom
+  open DependentProduct
+  open is-dependent-product
+```
+-->
+
+# Dependent products in presheaf categories
+
+We explicitly describe the construction of dependent products in
+presheaf categories. Just as for [exponentials], we use the
+[[Yoneda lemma]] to divine the correct answer.
+
+[exponentials]: Cat.Instances.Presheaf.Exponentials.html
+
+Fix a natural transformation $\alpha : F \Rightarrow G$ of presheaves.
+Given $X \in \psh(\cC)/F$, we wish to compute
+$\prod\limits_\alpha X \in \psh(\cC)/G$.
+
+$$
+\begin{align*}
+  (\prod_\alpha X)(c)
+  &= \hom_{\psh(\cC)}(\yo c, \prod_\alpha X)
+  \\ &= \hom_{\psh(\cC)}(\yo c, G)
+    \times \hom_{\psh(\cC)/G}(\yo c, \prod_\alpha X)
+  \\ &= G(c) \times \hom_{\psh(\cC)/F}(F \times_G \yo c, X)
+\end{align*}
+$$
+
+This explains how to evaluate $\prod_\alpha X$ at objects. The rest is
+straightforward, though the path algebra is tedious.
+
+```agda
+module _ {F G : PSh.Ob} (α : PSh.Hom F G) (X : /-Obj {C = PSh (o ⊔ ℓ) C} F) where
+  private
+    module /F = Cat.Reasoning (Slice (PSh (o ⊔ ℓ) C) F)
+    module /G = Cat.Reasoning (Slice (PSh (o ⊔ ℓ) C) G)
+    module F = Functor F
+    module G = Functor G
+    module pb = Functor (Base-change (PSh-pullbacks (o ⊔ ℓ) C) α)
+
+    PShΠ₀ : C.Ob → Type (o ⊔ ℓ)
+    PShΠ₀ c = Σ ∣ G.₀ c ∣ λ g → /F.Hom (pb.₀ (cut (yo G g))) X
+
+    abstract
+      PShΠ₀-path
+        : ∀ {c} {x y : PShΠ₀ c}
+        → (p : x .fst ≡ y .fst)
+        → x .snd /F.∘ pb.₁ (record { map = PSh.id ; com = PSh.idr _ ∙ ap (yo G) p })
+          ≡ y .snd
+        → x ≡ y
+      PShΠ₀-path {c} {g , β} {g′ , β′} p q = J
+        (λ g′ p →
+          ∀ {β′}
+          → β /F.∘ pb.₁ (record { map = PSh.id ; com = PSh.idr _ ∙ ap (yo G) p }) ≡ β′
+          → (g , β) ≡ (g′ , β′))
+        (λ p → ap (g ,_) (/F.intror (ap pb.₁ (/-Hom-path refl) ∙ pb.F-id) ∙ p))
+        p
+        q
+
+    PShΠ-Π : /G.Ob
+    PShΠ-Π .dom .F₀ c = el! (PShΠ₀ c)
+    PShΠ-Π .dom .F₁ f (g , β) =
+      G.₁ f g , (β /F.∘ pb.₁ (record { map = よ C .F₁ f ; com = yo-naturalr }))
+    PShΠ-Π .dom .F-id = funext λ (g , β) →
+      PShΠ₀-path (happly G.F-id g) $ /F.cancelr $ /-Hom-path
+      $ Nat-path λ _ → funext λ _ → Σ-pathp (C.idl _) (Σ-prop-pathp! refl)
+    PShΠ-Π .dom .F-∘ f₁ f₂ = funext λ (g , β) →
+      PShΠ₀-path (happly (G.F-∘ _ _) g) $ /F.extendr
+      $ sym (pb.F-∘ _ _)
+      ∙∙ ap pb.₁ (/-Hom-path (PSh.idr _ ∙ よ C .F-∘ _ _))
+      ∙∙ pb.F-∘ _ _
+    PShΠ-Π .map .η _ (g , _) = g
+    PShΠ-Π .map .is-natural _ _ _ = refl
+
+    PShΠ-ev : /F.Hom (pb.₀ PShΠ-Π) X
+    PShΠ-ev .map .η c ((g , β) , f , p) = β .map .η c (C.id , f , happly G.F-id g ∙ p)
+    PShΠ-ev .map .is-natural c c′ h = funext λ ((_ , β) , _) →
+      ap (map β .η c′) (Σ-pathp C.id-comm (Σ-prop-pathp! refl))
+      ∙ happly (β .map .is-natural c c′ h) _
+    PShΠ-ev .com = Nat-path λ c → funext λ ((_ , β) , _) → happly (β .com ηₚ c) _
+
+    PShΠ-ƛ : ∀ {Γ : /G.Ob} → /F.Hom (pb.₀ Γ) X → /G.Hom Γ PShΠ-Π
+    PShΠ-ƛ {Γ} m .map .η c γ =
+      Γ .map .η c γ , m /F.∘ pb.₁ (record { map = yo (dom Γ) γ ; com = yo-naturall })
+    PShΠ-ƛ {Γ} m .map .is-natural c c′ h = funext λ γ →
+      PShΠ₀-path (happly (map Γ .is-natural c c′ h) γ)
+      $ /F.pullr (sym (pb.F-∘ _ _))
+      ∙∙ ap (λ x → m /F.∘ pb.F₁ x) (/-Hom-path (PSh.idr _ ∙ sym yo-naturalr))
+      ∙∙ /F.pushr (pb.F-∘ _ _)
+    PShΠ-ƛ {Γ} m .com = Nat-path λ _ → refl
+```
+
+<!--
+```agda
+    abstract
+      PShΠ-ƛ-commutes
+        : ∀ {Γ} (m : /F.Hom (pb.₀ Γ) X) → PShΠ-ev /F.∘ pb.₁ (PShΠ-ƛ m) ≡ m
+      PShΠ-ƛ-commutes {Γ} m = /-Hom-path $ Nat-path λ c → funext λ (γ , f , p) →
+        ap (map m .η c) (Σ-pathp (happly (dom Γ .F-id) γ) (Σ-prop-pathp! refl))
+
+      PShΠ-ƛ-unique
+        : ∀ {Γ m} (m' : /G.Hom Γ PShΠ-Π) → PShΠ-ev /F.∘ pb.₁ m' ≡ m → m' ≡ PShΠ-ƛ m
+      PShΠ-ƛ-unique {Γ} m′ p = /-Hom-path $ Nat-path λ c → funext λ γ →
+        PShΠ₀-path (ap (λ x → x .η c γ) (m′ .com))
+        $ (/-Hom-path $ Nat-path λ c′ → funext λ (h , f , q) →
+          _ ≡⟨ ap (map (map m′ .η c γ .snd) .η c′) (Σ-pathp (sym (C.idr h)) (Σ-prop-pathp! refl)) ⟩
+          _ ≡⟨(λ i → m′ .map .is-natural c c′ h (~ i) γ .snd .map .η c′ (C.id , f , (λ j → G.₁ C.id (m′ .map .is-natural c c′ h (~ i ∧ ~ j) γ .fst)) ∙ happly G.F-id _ ∙ ap fst (happly (m′ .map .is-natural c c′ h) γ) ∙ ap (G.₁ h) (λ i → m′ .com i .η c γ) ∙ q))⟩
+          _ ≡⟨ ap (λ x → map (map m′ .η c′ (F₁ (dom Γ) h γ) .snd) .η c′ (C.id , f , x)) prop! ⟩
+          _ ∎)
+        ∙∙ /F.refl⟩∘⟨ pb.F-∘ _ _
+        ∙∙ /F.pulll p
+```
+-->
+
+```agda
+    PShΠ-is-Π : is-dependent-product (PSh (o ⊔ ℓ) C) fc PShΠ-Π PShΠ-ev
+    PShΠ-is-Π .ƛ = PShΠ-ƛ
+    PShΠ-is-Π .commutes = PShΠ-ƛ-commutes
+    PShΠ-is-Π .unique = PShΠ-ƛ-unique
+
+  PShΠ : DependentProduct (PSh (o ⊔ ℓ) C) fc α X
+  PShΠ .Π = PShΠ-Π
+  PShΠ .ev = PShΠ-ev
+  PShΠ .has-is-Π = PShΠ-is-Π
+```
+
+We conclude that presheaf categories are locally cartesian closed.
+
+```agda
+PSh-lccc : Locally-cartesian-closed (PSh (o ⊔ ℓ) C)
+PSh-lccc = dependent-products→lccc (PSh (o ⊔ ℓ) C) fc PShΠ
+```