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 \times B$ and limits over the functor out of $\id{Disc}(\{0,1\})$ which maps $0$ to $A$ and $1$ to $B$. We begin by defining the functor (reusing existing infrastructure):

2-object-diagram : ∀ {iss} → Ob → Ob → Functor (Disc′ (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 $A \ot Q \to B$ defines a cone over the discrete diagram consisting of $A$ and $B$. 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 : \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′ (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)