module Cat.Diagram.Product.Indexed {o β} (C : Precategory o β) where
Indexed productsπ
If a category admits a terminal object and binary products, then it admits products of any finite cardinality: iterate the binary product, and use the terminal object when there arenβt any objects. However, these two classes of limit do not let us speak of products of arbitrary cardinality, or, in the univalent context, indexed by types which are not sets.
Thatβs where -indexed products come in: Rather than having a functor giving the objects to take the limit over, we have an arbitrary map from to the space of objects of . An indexed product for this βdiagramβ is then an object admitting an universal family of maps .
record is-indexed-product (F : Idx β C.Ob) (Ο : β i β C.Hom P (F i)) : Type (o β β β level-of Idx) where no-eta-equality field tuple : β {Y} β (β i β C.Hom Y (F i)) β C.Hom Y P commute : β {i} {Y} {f : β i β C.Hom Y (F i)} β Ο i C.β tuple f β‘ f i unique : β {Y} {h : C.Hom Y P} (f : β i β C.Hom Y (F i)) β (β i β Ο i C.β h β‘ f i) β h β‘ tuple f eta : β {Y} (h : C.Hom Y P) β h β‘ tuple Ξ» i β Ο i C.β h eta h = unique _ Ξ» _ β refl hom-iso : β {Y} β C.Hom Y P β (β i β C.Hom Y (F i)) hom-iso = (Ξ» f i β Ο i C.β f) , is-isoβis-equiv Ξ» where .is-iso.inv β tuple .is-iso.rinv x β funext Ξ» i β commute .is-iso.linv x β sym (unique _ Ξ» _ β refl)
A category admits indexed products (of level ) if, for any type and family , there is an indexed product of .
record Indexed-product (F : Idx β C.Ob) : Type (o β β β level-of Idx) where no-eta-equality field {Ξ F} : C.Ob Ο : β i β C.Hom Ξ F (F i) has-is-ip : is-indexed-product F Ο open is-indexed-product has-is-ip public has-indexed-products : β β β Type _ has-indexed-products β = β {I : Type β} (F : I β C.Ob) β Indexed-product F
module _ {ββ²} {I : Type ββ²} (F : I β C .Precategory.Ob) (ip : Indexed-product F) where private module ip = Indexed-product ip tupleβ : β {A B} (f : β i β C.Hom B (F i)) {g : C.Hom A B} β ip.tuple f C.β g β‘ ip.tuple Ξ» i β f i C.β g tupleβ f = ip.unique _ Ξ» i β C.pulll ip.commute
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 β C.Ob) where open _=>_ ProjβCone : β {x} β (β i β C.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 C.β C.id β‘ subst (C.Hom (F i) β F) p C.id C.β Ο i) (C.idr _ β C.introl (transport-refl C.id)) p is-indexed-productβis-limit : β {x} {Ο : β i β C.Hom x (F i)} β is-indexed-product 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 (C.Hom (F i) β F) p C.id C.β Ο i β‘ Ο j) (C.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 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 F (eta .Ξ·) ip .tuple k = lim.universal k (J (Ξ» j p β subst (C.Hom (F _) β F) p C.id C.β k _ β‘ k j) (C.eliml (transport-refl _))) ip .commute = lim.factors _ _ ip .unique k comm = lim.unique _ _ _ comm IPβLimit : Indexed-product 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 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)
Uniquenessπ
As is traditional with universal constructions, βhaving an indexed product for a diagramβ is property of a category, not structure: Put another way, for any particular diagram, in a univalent category, there is (at most) a contractible space of indexed products of that diagram. And again as is traditional with universal constructions, the proof is surprisingly straightforward!
Indexed-product-unique : β {ββ²} {I : Type ββ²} (F : I β C.Ob) β is-category C β is-prop (Indexed-product F) Indexed-product-unique {I = I} F c-cat x y = p where module x = Indexed-product x module y = Indexed-product y
All we have to do β βallβ β is exhibit an isomorphism between the apices which commutes with the projection function in one direction, and with the product with morphisms in the other. Thatβs it! The isomorphism is induced by the universal properties, and is readily seen to commute with both projections:
apices : x.Ξ F C.β y.Ξ F apices = C.make-iso (y.tuple x.Ο) (x.tuple y.Ο) ( y.unique y.Ο (Ξ» i β C.pulll y.commute β x.commute) β sym (y.unique y.Ο Ξ» i β C.idr _) ) ( x.unique x.Ο (Ξ» i β C.pulll x.commute β y.commute) β sym (x.unique x.Ο Ξ» i β C.idr _))
By the characterisation of paths-over in Hom-sets, we get paths-over between the projection maps and the product maps:
module apices = C._β _ apices abstract pres : β j β PathP (Ξ» i β C.Hom (c-cat .to-path apices i) (F j)) (x.Ο j) (y.Ο j) pres j = Univalent.Hom-pathp-refll-iso c-cat x.commute presβ² : β {Y} (f : β j β C.Hom Y (F j)) β PathP (Ξ» i β C.Hom Y (c-cat .to-path apices i)) (x.tuple f) (y.tuple f) presβ² f = Univalent.Hom-pathp-reflr-iso c-cat (y.unique f Ξ» j β C.pulll y.commute β x.commute)
And after some munging (dealing with the axioms), thatβs exactly what we need to prove that indexed products are unique.
open Indexed-product open is-indexed-product p : x β‘ y p i .Ξ F = c-cat .to-path apices i p i .Ο j = pres j i p i .has-is-ip .tuple f = presβ² f i p i .has-is-ip .commute {i = j} {f = f} = is-propβpathp (Ξ» i β C.Hom-set _ (F j) (pres j i C.β presβ² f i) _) (x .has-is-ip .commute) (y .has-is-ip .commute) i p i .has-is-ip .unique {h = h} f = is-propβpathp (Ξ» i β Ξ -is-hlevel {A = C.Hom _ (c-cat .to-path apices i)} 1 Ξ» h β Ξ -is-hlevel {A = β j β pres j i C.β h β‘ f j} 1 Ξ» p β C.Hom-set _ (c-cat .to-path apices i) h (presβ² f i)) (Ξ» h β x.unique {h = h} f) (Ξ» h β y.unique {h = h} f) i h