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 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

  uniqueβ‚‚ : βˆ€ {Y} {g h : C.Hom Y P} β†’ (βˆ€ i β†’ Ο€ i C.∘ g ≑ Ο€ i C.∘ h) β†’ g ≑ h
  uniqueβ‚‚ {g = g} {h} eq = eta g βˆ™ ap tuple (funext eq) βˆ™ sym (eta h)

  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-products-indexed-by : βˆ€ {β„“} (I : Type β„“) β†’ Type _
has-products-indexed-by I = βˆ€ (F : I β†’ C.Ob) β†’ Indexed-product F

has-indexed-products : βˆ€ β„“ β†’ Type _
has-indexed-products β„“ = βˆ€ {I : Type β„“} β†’ has-products-indexed-by I

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

We can also prove the converse direction: if indexed products in are unique, then is univalent. In fact, we only need limits of one-object diagrams to be unique.

unique-products→is-category
  : ({x : C.Ob} β†’ is-prop (Indexed-product {Idx = ⊀} (Ξ» _ β†’ x)))
  β†’ is-category C
unique-products→is-category prop = cat where

Given an isomorphism we build two products for the one-object diagram one with apex itself and identity as projection, and one with apex and the given isomorphism as projection.

  module _ {a b : C.Ob} (is : a C.β‰… b) where
    open Indexed-product
    open is-indexed-product

    Pa : Indexed-product {Idx = ⊀} (Ξ» _ β†’ a)
    Pa .Ξ F = a
    Pa .Ο€ _ = C.id
    Pa .has-is-ip .tuple f = f _
    Pa .has-is-ip .commute = C.idl _
    Pa .has-is-ip .unique f p = sym (C.idl _) βˆ™ p _

    Pb : Indexed-product {Idx = ⊀} (Ξ» _ β†’ a)
    Pb .Ξ F = b
    Pb .Ο€ _ = is .C.from
    Pb .has-is-ip .tuple f = is .C.to C.∘ f _
    Pb .has-is-ip .commute = C.cancell (is .C.invr)
    Pb .has-is-ip .unique f p = sym (C.lswizzle (sym (p _)) (is .C.invl))

By uniqueness, the two products are equal, which gives us an equality lying over our isomorphism.

    path : a ≑ b
    path = ap Ξ F (prop Pa Pb)

    path-over : PathP (Ξ» i β†’ a C.β‰… path i) C.id-iso is
    path-over = C.β‰…-pathp-from _ _ (ap (Ξ» p β†’ p .Ο€ _) (prop Pa Pb))

  cat : is-category C
  cat .to-path = path
  cat .to-path-over = path-over