diff --git a/src/Cat/Diagram/DependentProduct.lagda.md b/src/Cat/Diagram/DependentProduct.lagda.md new file mode 100644 index 000000000..91ac8b26f --- /dev/null +++ b/src/Cat/Diagram/DependentProduct.lagda.md @@ -0,0 +1,168 @@ + + +```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 +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) +``` + + + +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 + Π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)) +``` diff --git a/src/Cat/Instances/Presheaf/DependentProducts.lagda.md b/src/Cat/Instances/Presheaf/DependentProducts.lagda.md new file mode 100644 index 000000000..764d16e6d --- /dev/null +++ b/src/Cat/Instances/Presheaf/DependentProducts.lagda.md @@ -0,0 +1,166 @@ + + +```agda +module Cat.Instances.Presheaf.DependentProducts + {o} ℓ (C : Precategory o (o ⊔ ℓ)) where +``` + + + +# 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 + 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Π +```