module Cat.Diagram.Limit.Product {o h} (C : Precategory o h) where
Products are limitsπ
We establish the correspondence between binary products and limits over the functor out of which maps to and to . We begin by defining the functor (reusing existing infrastructure):
2-object-diagram : β {iss} β Ob β Ob β Functor (Discβ² (el Bool iss)) C 2-object-diagram a b = Disc-diagram Discrete-Bool Ξ» where true β a false β b
With that out of the way, we can establish the claimed equivalence. We start by showing that any pair of morphisms defines a cone over the discrete diagram consisting of and . This is essentially by definition of what it means to be a cone in this case, but theyβre arranged in very different ways:
PairβCone : β {iss} {q a b} β Hom q a β Hom q b β Const q => (2-object-diagram {iss} a b) PairβCone f g = Disc-natural Ξ» where true β f false β g
The two-way correspondence between products and terminal cones is then simple enough to establish by appropriately shuffling the data.
is-productβis-limit : β {iss} {x a b} {p1 : Hom x a} {p2 : Hom x b} β is-product C p1 p2 β is-limit {C = C} (2-object-diagram {iss} a b) x (PairβCone p1 p2) is-productβis-limit {x = x} {a} {b} {p1} {p2} is-prod = to-is-limitp ml Ξ» where {true} β refl {false} β refl where module is-prod = is-product is-prod open make-is-limit ml : make-is-limit (2-object-diagram a b) x ml .Ο true = p1 ml .Ο false = p2 ml .commutes {true} {true} f = ap (_β p1) (transport-refl id) β idl _ ml .commutes {true} {false} f = absurd (trueβ false f) ml .commutes {false} {true} f = absurd (trueβ false $ sym f) ml .commutes {false} {false} f = ap (_β p2) (transport-refl id) β idl _ ml .universal eta _ = is-prod.β¨ eta true , eta false β©is-prod. ml .factors {true} eta _ = is-prod.Οββfactor ml .factors {false} eta _ = is-prod.Οββfactor ml .unique eta p other q = is-prod.unique other (q true) (q false) is-limitβis-product : β {iss} {a b} {K : Functor β€Cat C} β {eta : K Fβ !F => 2-object-diagram {iss} a b} β is-ran !F (2-object-diagram {iss} a b) K eta β is-product C (eta .Ξ· true) (eta .Ξ· false) is-limitβis-product {iss = iss} {a} {b} {K} {eta} lim = prod where module lim = is-limit lim pair : β {y} β Hom y a β Hom y b β β (j : Bool) β Hom y (2-object-diagram {iss} a b .Fβ j) pair p1 p2 true = p1 pair p1 p2 false = p2 pair-commutes : β {y} {p1 : Hom y a} {p2 : Hom y b} β {i j : Bool} β (p : i β‘ j) β 2-object-diagram {iss} a b .Fβ p β pair p1 p2 i β‘ pair p1 p2 j pair-commutes {p1 = p1} {p2 = p2} = J (Ξ» _ p β 2-object-diagram {iss} a b .Fβ p β pair p1 p2 _ β‘ pair p1 p2 _) (eliml (2-object-diagram {iss} a b .F-id)) prod : is-product C (eta .Ξ· true) (eta .Ξ· false) prod .β¨_,_β© f g = lim.universal (pair f g) pair-commutes prod .Οββfactor {_} {p1'} {p2'} = lim.factors (pair p1' p2') pair-commutes prod .Οββfactor {_} {p1'} {p2'} = lim.factors (pair p1' p2') pair-commutes prod .unique other p q = lim.unique _ _ other Ξ» where true β p false β q ProductβLimit : β {iss} {a b} β Product C a b β Limit (2-object-diagram {iss} a b) ProductβLimit prod = to-limit (is-productβis-limit (has-is-product prod)) LimitβProduct : β {iss} {a b} β Limit (2-object-diagram {iss} a b) β Product C a b LimitβProduct lim .apex = Limit.apex lim LimitβProduct lim .Οβ = Limit.cone lim .Ξ· true LimitβProduct lim .Οβ = Limit.cone lim .Ξ· false LimitβProduct lim .has-is-product = is-limitβis-product (Limit.has-limit lim)
We note that any functor is canonically equal, not just naturally isomorphic, to the one we defined above.
canonical-functors : β {iss} (F : Functor (Discβ² (el Bool iss)) C) β F β‘ 2-object-diagram (Fβ F true) (Fβ F false) canonical-functors {iss = iss} F = Functor-path p q where p : β x β _ p false = refl p true = refl q : β {x y} (f : x β‘ y) β _ q {false} {false} p = Fβ F p β‘β¨ ap (Fβ F) (iss _ _ _ _) β©β‘ Fβ F refl β‘β¨ F-id F β©β‘ id β‘Λβ¨ transport-refl _ β©β‘Λ transport refl id β q {true} {true} p = Fβ F p β‘β¨ ap (Fβ F) (iss _ _ _ _) β©β‘ Fβ F refl β‘β¨ F-id F β©β‘ id β‘Λβ¨ transport-refl _ β©β‘Λ transport refl id β q {false} {true} p = absurd (trueβ false (sym p)) q {true} {false} p = absurd (trueβ false p)