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-diagram : βˆ€ {iss} β†’ Ob β†’ Ob β†’ Functor (Discβ€² (el Bool iss)) C
2-object-diagram a b = Disc-diagram Discrete-Bool Ξ» 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
  : βˆ€ {iss} {q a b} β†’ Hom q a β†’ Hom q b
  β†’ Const q => (2-object-diagram {iss} 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
  : βˆ€ {iss} {x a b} {p1 : Hom x a} {p2 : Hom x b}
  β†’ is-product C p1 p2
  → is-limit {C = C} (2-object-diagram {iss} 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 = ap (_∘ p1) (transport-refl id) βˆ™ idl _
    ml .commutes {true} {false} f = absurd (true≠false f)
    ml .commutes {false} {true} f = absurd (true≠false $ sym f)
    ml .commutes {false} {false} f = ap (_∘ p2) (transport-refl id) βˆ™ idl _
    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
  : βˆ€ {iss} {a b} {K : Functor ⊀Cat C}
  β†’ {eta : K F∘ !F => 2-object-diagram {iss} a b}
  β†’ is-ran !F (2-object-diagram {iss} a b) K eta
  β†’ is-product C (eta .Ξ· true) (eta .Ξ· false)
is-limit→is-product {iss = iss} {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 {iss} 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 {iss} a b .F₁ p ∘ pair p1 p2 i ≑ pair p1 p2 j
  pair-commutes {p1 = p1} {p2 = p2} =
      J (Ξ» _ p β†’ 2-object-diagram {iss} a b .F₁ p ∘ pair p1 p2 _ ≑ pair p1 p2 _)
        (eliml (2-object-diagram {iss} 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 : βˆ€ {iss} {a b} β†’ Product C a b β†’ Limit (2-object-diagram {iss} a b)
Product→Limit prod = to-limit (is-product→is-limit (has-is-product prod))

Limitβ†’Product : βˆ€ {iss} {a b} β†’ Limit (2-object-diagram {iss} 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
  : βˆ€ {iss} (F : Functor (Discβ€² (el Bool iss)) C)
  β†’ F ≑ 2-object-diagram (Fβ‚€ F true) (Fβ‚€ F false)
canonical-functors {iss = iss} 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) (iss _ _ _ _) βŸ©β‰‘
    F₁ F refl         β‰‘βŸ¨ F-id F βŸ©β‰‘
    id                β‰‘Λ˜βŸ¨ transport-refl _ βŸ©β‰‘Λ˜
    transport refl id ∎
  q {true} {true} p =
    F₁ F p            β‰‘βŸ¨ ap (F₁ F) (iss _ _ _ _) βŸ©β‰‘
    F₁ F refl         β‰‘βŸ¨ F-id F βŸ©β‰‘
    id                β‰‘Λ˜βŸ¨ transport-refl _ βŸ©β‰‘Λ˜
    transport refl id ∎
  q {false} {true} p = absurd (true≠false (sym p))
  q {true} {false} p = absurd (true≠false p)