open import Cat.Diagram.Limit.Base
open import Cat.Instances.Discrete
open import Cat.Instances.Functor
open import Cat.Diagram.Terminal
open import Cat.Diagram.Product
open import Cat.Prelude

open import Data.Bool

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})\id{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
  false  A
  true   B

With that out of the way, we can establish the claimed equivalence. We start by showing that any pair of morphisms AQBA \ot 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
   Cone (2-object-diagram {iss = iss} A B)
Pair→Cone {Q = Q} _ _ .apex  = Q
Pair→Cone p1 p2 .ψ false = p1
Pair→Cone p1 p2 .ψ true  = p2
Pair→Cone _ _ .commutes {false} {false} f = ap (_∘ _) (transport-refl _)  idl _
Pair→Cone _ _ .commutes {false} {true}  f = absurd (true≠false (sym f))
Pair→Cone _ _ .commutes {true}  {false} f = absurd (true≠false f)
Pair→Cone _ _ .commutes {true}  {true}  f = ap (_∘ _) (transport-refl _)  idl _

The two-way correspondence between products and terminal cones is then simple enough to establish by appropriately shuffling the data.

Prod→Lim :  {iss} {A B}  Product C A B  Limit (2-object-diagram {iss = iss} A B)
Prod→Lim prod .top = Pair→Cone (prod .π₁) (prod .π₂)
Prod→Lim prod .has⊤ x .centre .hom = prod .⟨_,_⟩ (x .ψ false) (x .ψ true)
Prod→Lim prod .has⊤ x .centre .commutes false = prod .π₁∘factor
Prod→Lim prod .has⊤ x .centre .commutes true  = prod .π₂∘factor
Prod→Lim prod .has⊤ x .paths y = Cone-hom-path (2-object-diagram _ _)
  (sym (prod .unique (y .hom) (y .commutes _) (y .commutes _)))

Lim→Prod :  {iss} {A B}  Limit (2-object-diagram {iss = iss} A B)  Product C A B
Lim→Prod x .apex = x .top .apex
Lim→Prod x .π₁   = x .top .ψ false
Lim→Prod x .π₂   = x .top .ψ true
Lim→Prod x .has-is-product .⟨_,_⟩ p1 p2 = x .has⊤ (Pair→Cone p1 p2) .centre .hom
Lim→Prod x .has-is-product .π₁∘factor = x .has⊤ (Pair→Cone _ _) .centre .commutes _
Lim→Prod x .has-is-product .π₂∘factor = x .has⊤ (Pair→Cone _ _) .centre .commutes _
Lim→Prod x .has-is-product .unique f p q =
  sym (ap hom (x .has⊤ (Pair→Cone _ _) .paths other))
  where
    other : Cone-hom (2-object-diagram _ _) _ _
    other .hom = f
    other .commutes false = p
    other .commutes true  = q

We note that any functor F:Disc({0,1})CF : \id{Disc}(\{0,1\}) \to \ca{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 false) (F₀ F true)
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)