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-category : Precategory _ _ 2-object-category = Disc' (el Bool Bool-is-set) 2-object-diagram : Ob β Ob β Functor 2-object-category C 2-object-diagram a b = Disc-diagram Ξ» 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 : β {q a b} β Hom q a β Hom q b β Const q => (2-object-diagram 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 : β {x a b} {p1 : Hom x a} {p2 : Hom x b} β is-product C p1 p2 β is-limit {C = C} (2-object-diagram 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 = idl p1 ml .commutes {true} {false} f = absurd (trueβ false f) ml .commutes {false} {true} f = absurd (trueβ false $ sym f) ml .commutes {false} {false} f = idl p2 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 : β {a b} {K : Functor β€Cat C} β {eta : K Fβ !F => 2-object-diagram a b} β is-ran !F (2-object-diagram a b) K eta β is-product C (eta .Ξ· true) (eta .Ξ· false) is-limitβis-product {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 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 a b .Fβ p β pair p1 p2 i β‘ pair p1 p2 j pair-commutes {p1 = p1} {p2 = p2} = J (Ξ» _ p β 2-object-diagram a b .Fβ p β pair p1 p2 _ β‘ pair p1 p2 _) (eliml (2-object-diagram 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 : β {a b} β Product C a b β Limit (2-object-diagram a b) ProductβLimit prod = to-limit (is-productβis-limit (has-is-product prod)) LimitβProduct : β {a b} β Limit (2-object-diagram 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 : β (F : Functor 2-object-category C) β F β‘ 2-object-diagram (Fβ F true) (Fβ F false) canonical-functors 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) (Bool-is-set _ _ _ _) β©β‘ Fβ F refl β‘β¨ F-id F β©β‘ id β q {true} {true} p = Fβ F p β‘β¨ ap (Fβ F) (Bool-is-set _ _ _ _) β©β‘ Fβ F refl β‘β¨ F-id F β©β‘ id β q {false} {true} p = absurd (trueβ false (sym p)) q {true} {false} p = absurd (trueβ false p)
Indexed products as limitsπ
In the particular case where
is a groupoid, e.g.Β because it arises as the space of objects of a univalent category,
an indexed
product for
is the same thing as a limit over
,
considered as a functor
.
We can not lift this restriction: If
is not a groupoid, then its path spaces
are not necessarily sets, and so the Disc
construction does not apply to
it.
module _ {β} {I : Type β} (i-is-grpd : is-groupoid I) (F : I β Ob) where open _=>_ ProjβCone : β {x} β (β i β Hom x (F i)) β Const x => Disc-adjunct {C = C} {iss = i-is-grpd} F ProjβCone Ο .Ξ· i = Ο i ProjβCone Ο .is-natural i j p = J (Ξ» j p β Ο j β id β‘ subst (Hom (F i) β F) p id β Ο i) (idr _ β introl (transport-refl id)) p is-indexed-productβis-limit : β {x} {Ο : β i β Hom x (F i)} β is-indexed-product C F Ο β is-limit (Disc-adjunct F) x (ProjβCone Ο) is-indexed-productβis-limit {x = x} {Ο} ip = to-is-limitp ml refl where module ip = is-indexed-product ip open make-is-limit ml : make-is-limit (Disc-adjunct F) x ml .Ο j = Ο j ml .commutes {i} {j} p = J (Ξ» j p β subst (Hom (F i) β F) p id β Ο i β‘ Ο j) (eliml (transport-refl _)) p ml .universal eta p = ip.tuple eta ml .factors eta p = ip.commute ml .unique eta p other q = ip.unique eta q is-limitβis-indexed-product : β {K : Functor β€Cat C} β {eta : K Fβ !F => Disc-adjunct {iss = i-is-grpd} F} β is-ran !F (Disc-adjunct F) K eta β is-indexed-product C F (eta .Ξ·) is-limitβis-indexed-product {K = K} {eta} lim = ip where module lim = is-limit lim open is-indexed-product hiding (eta) ip : is-indexed-product C F (eta .Ξ·) ip .tuple k = lim.universal k (J (Ξ» j p β subst (Hom (F _) β F) p id β k _ β‘ k j) (eliml (transport-refl _))) ip .commute = lim.factors _ _ ip .unique k comm = lim.unique _ _ _ comm IPβLimit : Indexed-product C F β Limit {C = C} (Disc-adjunct {iss = i-is-grpd} F) IPβLimit ip = to-limit (is-indexed-productβis-limit has-is-ip) where open Indexed-product ip LimitβIP : Limit {C = C} (Disc-adjunct {iss = i-is-grpd} F) β Indexed-product C F LimitβIP lim .Indexed-product.Ξ F = _ LimitβIP lim .Indexed-product.Ο = _ LimitβIP lim .Indexed-product.has-is-ip = is-limitβis-indexed-product (Limit.has-limit lim)