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 # true) (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 .F-id β©β‘ id β q {true} {true} p = F .Fβ p β‘β¨ ap (F .Fβ) (Bool-is-set _ _ _ _) β©β‘ F .Fβ refl β‘β¨ F .F-id β©β‘ 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)