open import Cat.Diagram.Product.Indexed
open import Cat.Diagram.Limit.Finite
open import Cat.Diagram.Limit.Base
open import Cat.Diagram.Equaliser
open import Cat.Diagram.Terminal
open import Cat.Diagram.Product
open import Cat.Prelude

open import Data.Fin

import Cat.Reasoning as Cr

module Cat.Diagram.Product.Finite
  {o ℓ} {C : Precategory o ℓ}
  (terminal : Terminal C)
  (products : ∀ A B → Product C A B)
  where

Computing finite products🔗

Throughout the 1lab, we have referred to categories having a terminal object and binary products as Cartesian categories, finite products categories, and other terms like these. But, a priori, there is no reason to believe that this implies all finite products exist, right? Right — which is why we have to prove it.

In this module, we prove the following theorem: If you have a sequence of objects in $\mathcal{C}$ of length $n$, then its product exists as long as $\mathcal{C}$ is Cartesian, and can be computed in terms of iterated binary products and terminal objects.

We take an opportunity to complicate the definition while we’re at it: Instead of computing the product of a one-object sequence to be $A \times \top$, we simply let it be $A$. This extra case translates to an extra case in all the proofs, but fortunately it does not complicate anything too far.

Cartesian→standard-finite-products : ∀ {n} → (F : Fin n → Ob) → Indexed-product C F
Cartesian→standard-finite-products F = prod where
  F-apex : ∀ {n} → (F : Fin n → Ob) → Ob
  F-apex {zero} F        = terminal .top
  F-apex {suc zero} F    = F fzero
  F-apex {suc (suc n)} F = F fzero ⊗ F-apex (λ e → F (fsuc e))

  F-pi : ∀ {n} (F : Fin n → Ob) (i : Fin n) → Hom (F-apex F) (F i)
  F-pi {suc zero} F fzero       = id
  F-pi {suc (suc n)} F fzero    = Cart.π₁
  F-pi {suc (suc n)} F (fsuc i) = F-pi (λ e → F (fsuc e)) i ∘ Cart.π₂

  F-mult : ∀ {Y} {n} (F : Fin n → Ob)
         → ((i : Fin n) → Hom Y (F i)) → Hom Y (F-apex F)
  F-mult {n = zero} F maps = ! terminal
  F-mult {n = suc zero} F maps = maps fzero
  F-mult {n = suc (suc n)} F maps = Cart.⟨ maps fzero , F-mult (λ z → F (fsuc z)) (λ i → maps (fsuc i)) ⟩Cart.

  F-commute : ∀ {Y} {n} (F : Fin n → Ob) (f : (i : Fin n) → Hom Y (F i))
            → ∀ i → F-pi F i ∘ F-mult F f ≡ f i
  F-commute {n = suc zero} F f fzero = idl (f fzero)
  F-commute {n = suc (suc n)} F f fzero = Cart.π₁∘⟨⟩
  F-commute {n = suc (suc n)} F f (fsuc i) = pullr Cart.π₂∘⟨⟩ ∙ F-commute (λ e → F (fsuc e)) (λ e → f (fsuc e)) i

  F-unique
    : ∀ {Y} {n} (F : Fin n → Ob) (f : (i : Fin n) → Hom Y (F i))
    → {h : Hom Y (F-apex F)} → ((i : Fin n) → F-pi F i ∘ h ≡ f i)
    → h ≡ F-mult F f
  F-unique {n = zero} F f {h} p = sym $ !-unique terminal _
  F-unique {n = suc zero} F f {h} p = sym (idl h) ∙ p fzero
  F-unique {n = suc (suc n)} F f {h} p =
    products _ _ .unique h (p fzero)
      (F-unique (λ e → F (fsuc e)) (λ i → f (fsuc i))
        λ i → assoc _ _ _ ∙ p (fsuc i))

  prod : Indexed-product C F
  prod .ΠF = F-apex F
  prod .π  = F-pi F
  prod .has-is-ip .tuple      = F-mult F
  prod .has-is-ip .commute    = F-commute F _ _
  prod .has-is-ip .unique f p = F-unique F f p