module Cat.Diagram.Limit.Product {o h} (C : Precategory o h) where

Products are limitsπŸ”—

We establish the correspondence between binary products AΓ—BA \times B and limits over the functor out of Disc({0,1})\mathrm{Disc}(\{0,1\}) which maps 00 to AA and 11 to BB. 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 A←Qβ†’BA \leftarrow Q \to B defines a cone over the discrete diagram consisting of AA and BB. 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 F:Disc({0,1})β†’CF : \mathrm{Disc}(\{0,1\}) \to \mathcal{C} 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 II is a groupoid, e.g. because it arises as the space of objects of a univalent category, an indexed product for F:I→CF : I \to \mathcal{C} is the same thing as a limit over FF, considered as a functor DiscI→C\mathrm{Disc}{I} \to \mathcal{C}. We can not lift this restriction: If II is not a groupoid, then its path spaces x=yx = y 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)