{-# OPTIONS --without-K --safe #-}
module Cats.Category.Constructions.Product where

open import Data.Bool using (Bool ; true ; false ; not)
open import Level

open import Cats.Category.Base
open import Cats.Category.Constructions.Terminal as Terminal using (HasTerminal)
open import Cats.Functor using (Functor)
open import Cats.Util.Conv
open import Cats.Util.Logic.Constructive

import Cats.Category.Constructions.Iso as Iso
import Cats.Category.Constructions.Unique as Unique


Bool-elim : ∀ {a} {A : Bool → Set a} → A true → A false → (i : Bool) → A i
Bool-elim x y true = x
Bool-elim x y false = y


module Build {lo la l≈} (Cat : Category lo la l≈) where

  private open module Cat = Category Cat
  open Cat.≈-Reasoning
  open Iso.Build Cat
  open Unique.Build Cat
  open Terminal.Build Cat
  open _≅_


  IsProduct : ∀ {li} {I : Set li} (O : I → Obj) P → (∀ i → P ⇒ O i)
    → Set (lo ⊔ la ⊔ l≈ ⊔ li)
  IsProduct O P proj
      = ∀ {X} (x : ∀ i → X ⇒ O i) → ∃![ u ] (∀ i → x i ≈ proj i ∘ u)


  -- TODO The types of the equalities in IsBinaryProducts are backwards, since
  -- we want the RHS to be simpler than the LHS. So, projl ∘ u ≈ xl instead
  -- of xl ≈ projl ∘ u.
  IsBinaryProduct : ∀ {A B} P → (P ⇒ A) → (P ⇒ B) → Set (lo ⊔ la ⊔ l≈)
  IsBinaryProduct {A} {B} P projl projr
      = ∀ {X} (xl : X ⇒ A) (xr : X ⇒ B)
        → ∃![ u ] (xl ≈ projl ∘ u ∧ xr ≈ projr ∘ u)


  IsBinaryProduct→IsProduct : ∀ {A B P} {pl : P ⇒ A} {pr : P ⇒ B}
    → IsBinaryProduct P pl pr
    → IsProduct (Bool-elim A B) P (Bool-elim pl pr)
  IsBinaryProduct→IsProduct isBinProd x = record
      { arr = f ⃗
      ; prop = Bool-elim (∧-eliml (∃!′.prop f)) (∧-elimr (∃!′.prop f))
      ; unique = λ eq → ∃!′.unique f (eq true , eq false)
      }
    where
      f = isBinProd (x true) (x false)


  record Product {li} {I : Set li} (O : I → Obj) : Set (lo ⊔ la ⊔ l≈ ⊔ li) where
    field
      prod : Obj
      proj : ∀ i → prod ⇒ O i
      isProduct : IsProduct O prod proj


  open Product using (proj ; isProduct)


  instance
    HasObj-Product : ∀ {li} {I : Set li} {O : I → Obj}
      → HasObj (Product O) lo la l≈
    HasObj-Product = record { Cat = Cat ; _ᴼ = Product.prod }


  BinaryProduct : Obj → Obj → Set (lo ⊔ la ⊔ l≈)
  BinaryProduct A B = Product (Bool-elim A B)


  mkBinaryProduct : ∀ {A B P} (pl : P ⇒ A) (pr : P ⇒ B)
    → IsBinaryProduct P pl pr
    → BinaryProduct A B
  mkBinaryProduct {P = P} pl pr isBinProd = record
      { isProduct = IsBinaryProduct→IsProduct isBinProd }


  nullaryProduct-Terminal : (P : Product {I = ⊥} (λ())) → IsTerminal (P ᴼ)
  nullaryProduct-Terminal P X with isProduct P {X = X} λ()
  ... | ∃!-intro arr _ unique = ∃!-intro arr _ (λ _ → unique λ())


  module _ {li} {I : Set li} {O : I → Obj} (P : Product O) where

    factorizer : ∀ {X} → (∀ i → X ⇒ O i) → X ⇒ P ᴼ
    factorizer proj = isProduct P proj ⃗


    factorizer-unique : ∀ {X} (fact : X ⇒ P ᴼ)
      → {x : ∀ i → X ⇒ O i}
      → (∀ i → x i ≈ proj P i ∘ fact)
      → factorizer x ≈ fact
    factorizer-unique fact {x} eq = ∃!′.unique (isProduct P x) eq


    factorizer-proj : ∀ {X} {x : ∀ i → X ⇒ O i} {i}
      → proj P i ∘ factorizer x ≈ x i
    factorizer-proj {x = x} {i} = ≈.sym (∃!′.prop (isProduct P x) i)


    factorizer-resp : ∀ {X} {x y : ∀ i → X ⇒ O i}
      → (∀ i → x i ≈ y i)
      → factorizer x ≈ factorizer y
    factorizer-resp {x = x} {y} eq = factorizer-unique (factorizer y)
      λ i → ≈.trans (eq _) (≈.sym factorizer-proj)


    factorizer-∘ : ∀ {X} {x : ∀ i → X ⇒ O i} {Z} {f : Z ⇒ X}
      → factorizer x ∘ f ≈ factorizer (λ i → x i ∘ f)
    factorizer-∘ {x = x} {f = f} = ≈.sym
      (factorizer-unique (factorizer x ∘ f)
        λ _ → ≈.sym (≈.trans unassoc (∘-resp-l factorizer-proj)))


    factorizer-id : factorizer (proj P) ≈ id
    factorizer-id = factorizer-unique id λ i → ≈.sym id-r


  module _ {li} {I : Set li}
    {O : I → Obj}  (P : Product O)
    {O′ : I → Obj} (P′ : Product O′)
    where

    times : (∀ i → O i ⇒ O′ i) → P ᴼ ⇒ P′ ᴼ
    times x = factorizer P′ (λ i → x i ∘ proj P i)


    times-proj : ∀ {x : ∀ i → O i ⇒ O′ i} {i}
      → proj P′ i ∘ times x ≈ x i ∘ proj P i
    times-proj = factorizer-proj P′


    times-resp : {x y : ∀ i → O i ⇒ O′ i}
      → (∀ i → x i ≈ y i)
      → times x ≈ times y
    times-resp {x} {y} eq = factorizer-resp P′ (λ i → ∘-resp-l (eq i))


  times-id : ∀ {li} {I : Set li} {O : I → Obj} (P : Product O)
    → times P P (λ _ → id) ≈ id
  times-id P = factorizer-unique P id λ _ → ≈.trans id-l (≈.sym id-r)


  times-∘ : ∀ {li} {I : Set li}
    → {O O′ O″ : I → Obj}
    → (P : Product O) (P′ : Product O′) (P″ : Product O″)
    → {x : ∀ i → O i ⇒ O′ i} {y : ∀ i → O′ i ⇒ O″ i}
    → times P′ P″ y ∘ times P P′ x ≈ times P P″ (λ i → y i ∘ x i)
  times-∘ P P′ P″ {x} {y} =
    begin
      times P′ P″ y ∘ times P P′ x
    ≈⟨ factorizer-∘ P″ ⟩
      factorizer P″ (λ i → (y i ∘ proj P′ i) ∘ times P P′ x)
    ≈⟨ factorizer-resp P″ (λ i → assoc) ⟩
      factorizer P″ (λ i → y i ∘ proj P′ i ∘ times P P′ x)
    ≈⟨ factorizer-resp P″ (λ i → ∘-resp-r (times-proj P P′)) ⟩
      factorizer P″ (λ i → y i ∘ x i ∘ proj P i)
    ≈⟨ factorizer-resp P″ (λ i → unassoc) ⟩
      times P P″ (λ i → y i ∘ x i)
    ∎


  times-factorizer : ∀ {li} {I : Set li}
    → {O O′ : I → Obj}
    → (P : Product O) (P′ : Product O′)
    → ∀ {X} {x : ∀ i → X ⇒ O i} {y : ∀ i → O i ⇒ O′ i}
    → times P P′ y ∘ factorizer P x ≈ factorizer P′ (λ i → y i ∘ x i)
  times-factorizer P P′
    = ≈.trans (factorizer-∘ P′)
        (factorizer-resp P′ λ i → ≈.trans assoc (∘-resp-r (factorizer-proj P)))


  proj-cancel : ∀ {li} {I : Set li} {O : I → Obj} {P proj}
    → IsProduct O P proj
    → ∀ {X} {f g : X ⇒ P}
    → (∀ i → proj i ∘ f ≈ proj i ∘ g)
    → f ≈ g
  proj-cancel {proj = proj} prod {f = f} {g} eq with prod (λ i → proj i ∘ g)
  ... | ∃!-intro u _ u-uniq
      = begin
          f
        ≈⟨ ≈.sym (u-uniq (λ i → ≈.sym (eq i))) ⟩
          u
        ≈⟨ u-uniq (λ i → ≈.refl) ⟩
          g
        ∎


  Product-resp-≅ : ∀ {li} {I : Set li} {O O′ : I → Obj}
    → (∀ i → O i ≅ O′ i)
    → (P : Product O) (P′ : Product O′)
    → P ᴼ ≅ P′ ᴼ
  Product-resp-≅ O≅O′ P P′ = record
    { forth = factorizer P′ (λ i → O≅O′ i .forth ∘ proj P i)
    ; back = factorizer P (λ i → O≅O′ i .back ∘ proj P′ i)
    ; back-forth = ≈.trans (factorizer-∘ P)
        (factorizer-unique P id λ i →
          ≈.trans assoc (≈.trans (∘-resp-r (factorizer-proj P′))
            (≈.trans unassoc (≈.trans (∘-resp-l (O≅O′ i .back-forth))
              (≈.trans id-l (≈.sym id-r))))))
    ; forth-back = ≈.trans (factorizer-∘ P′)
        (factorizer-unique P′ id λ i →
          ≈.trans assoc (≈.trans (∘-resp-r (factorizer-proj P))
            (≈.trans unassoc (≈.trans (∘-resp-l (O≅O′ i .forth-back))
              (≈.trans id-l (≈.sym id-r))))))
    }


open Build public using
  (IsProduct ; IsBinaryProduct ; Product ; BinaryProduct ; HasObj-Product)


record HasProducts {lo la l≈} li (C : Category lo la l≈)
  : Set (suc li ⊔ lo ⊔ la ⊔ l≈ )
  where
  private module Bld = Build C
  open Category C
  open Iso.Build C

  field
    Π′ : {I : Set li} (O : I → Obj) → Product C O


  module _ {I : Set li} where

    Π : ∀ (O : I → Obj) → Obj
    Π O = Product.prod (Π′ O)


    syntax Π (λ i → O) = Π[ i ] O


    proj : ∀ {O : I → Obj} i → Π O ⇒ O i
    proj {O} = Bld.Product.proj (Π′ O)


    factorizer : ∀ {O : I → Obj} {X} → (∀ i → X ⇒ O i) → X ⇒ Π O
    factorizer {O} = Bld.factorizer (Π′ O)


    times : ∀ {O O′ : I → Obj} → (∀ i → O i ⇒ O′ i) → Π O ⇒ Π O′
    times {O} {O′} = Bld.times (Π′ O) (Π′ O′)


    factorizer-proj : ∀ {O : I → Obj} {X} {x : ∀ i → X ⇒ O i} {i}
      → proj i ∘ factorizer x ≈ x i
    factorizer-proj {O} = Bld.factorizer-proj (Π′ O)


    factorizer-resp : ∀ {O : I → Obj} {X} {x y : ∀ i → X ⇒ O i}
      → (∀ i → x i ≈ y i)
      → factorizer x ≈ factorizer y
    factorizer-resp {O} = Bld.factorizer-resp (Π′ O)


    factorizer-unique : ∀ {O : I → Obj} {X} {x : ∀ i → X ⇒ O i} {u}
      → (∀ i → x i ≈ proj i ∘ u)
      → factorizer x ≈ u
    factorizer-unique {O} eq = Bld.factorizer-unique (Π′ O) _ eq


    factorizer-∘ : ∀ {O : I → Obj} {X} {x : ∀ i → X ⇒ O i} {Z} {f : Z ⇒ X}
      → factorizer x ∘ f ≈ factorizer (λ i → x i ∘ f)
    factorizer-∘ {O} = Bld.factorizer-∘ (Π′ O)


    factorizer-id : ∀ {O} → factorizer {O} proj ≈ id
    factorizer-id {O} = Bld.factorizer-id (Π′ O)


    times-proj : ∀ {O O′ : I → Obj} {x : ∀ i → O i ⇒ O′ i} {i}
      → proj i ∘ times x ≈ x i ∘ proj i
    times-proj {O} {O′} = Bld.times-proj (Π′ O) (Π′ O′)


    times-resp : ∀ {O O′ : I → Obj} {x y : ∀ i → O i ⇒ O′ i}
      → (∀ i → x i ≈ y i)
      → times x ≈ times y
    times-resp {O} {O′} = Bld.times-resp (Π′ O) (Π′ O′)


    times-id : ∀ {O : I → Obj} → times {O} (λ _ → id) ≈ id
    times-id {O} = Bld.times-id (Π′ O)


    times-∘ : ∀ {O O′ O″ : I → Obj} {x : ∀ i → O i ⇒ O′ i} {y : ∀ i → O′ i ⇒ O″ i}
      → times y ∘ times x ≈ times (λ i → y i ∘ x i)
    times-∘ {O} {O′} {O″} = Bld.times-∘ (Π′ O) (Π′ O′) (Π′ O″)


    times-factorizer : ∀ {O O′ : I → Obj} {X}
      → {x : ∀ i → X ⇒ O i} {y : ∀ i → O i ⇒ O′ i}
      → times y ∘ factorizer x ≈ factorizer (λ i → y i ∘ x i)
    times-factorizer {O} {O′} = Bld.times-factorizer (Π′ O) (Π′ O′)


    Π-resp-≅ : ∀ {O O′ : I → Obj}
      → (∀ i → O i ≅ O′ i)
      → Π O ≅ Π O′
    Π-resp-≅ {O} {O′} O≅O′ = Bld.Product-resp-≅ O≅O′ (Π′ O) (Π′ O′)


HasProducts→HasTerminal : ∀ {lo la l≈} {C : Category lo la l≈}
  → HasProducts zero C
  → HasTerminal C
HasProducts→HasTerminal {C = C} record { Π′ = Π }
    = let P = Π {I = ⊥} λ() in
      record
        { ⊤ = Product.prod P
        ; isTerminal = Build.nullaryProduct-Terminal C P
        }


record HasBinaryProducts {lo la l≈} (C : Category lo la l≈)
  : Set (lo ⊔ la ⊔ l≈)
  where
  private module Bld = Build C
  open Category C
  open Iso.Build C
  open ≈-Reasoning

  infixr  _×_ _×′_ ⟨_×_⟩ ⟨_,_⟩

  field
    _×′_ : ∀ A B → BinaryProduct C A B


  _×_ : Obj → Obj → Obj
  A × B = (A ×′ B) ᴼ


  projl : ∀ {A B} → A × B ⇒ A
  projl {A} {B} = Product.proj (A ×′ B) true


  projr : ∀ {A B} → A × B ⇒ B
  projr {A} {B} = Product.proj (A ×′ B) false


  ⟨_,_⟩ : ∀ {A B Z} → Z ⇒ A → Z ⇒ B → Z ⇒ A × B
  ⟨_,_⟩ {A} {B} f g
      = Bld.factorizer (A ×′ B) (Bool-elim f g)


  ⟨_×_⟩ : ∀ {A B A′ B′} → A ⇒ A′ → B ⇒ B′ → A × B ⇒ A′ × B′
  ⟨_×_⟩ {A} {B} {A′} {B′} f g
      = Bld.times (A ×′ B) (A′ ×′ B′) (Bool-elim f g)


  first : ∀ {A A′ B} → A ⇒ A′ → A × B ⇒ A′ × B
  first f = ⟨ f × id ⟩


  second : ∀ {A B B′} → B ⇒ B′ → A × B ⇒ A × B′
  second f = ⟨ id × f ⟩


  swap : ∀ {A B} → A × B ⇒ B × A
  swap = ⟨ projr , projl ⟩


  ⟨,⟩-resp : ∀ {A B Z} {f f′ : Z ⇒ A} {g g′ : Z ⇒ B}
    → f ≈ f′
    → g ≈ g′
    → ⟨ f , g ⟩ ≈ ⟨ f′ , g′ ⟩
  ⟨,⟩-resp {A} {B} f≈f′ g≈g′
      = Bld.factorizer-resp (A ×′ B) (Bool-elim f≈f′ g≈g′)


  ⟨,⟩-projl : ∀ {A B Z} {f : Z ⇒ A} {g : Z ⇒ B} → projl ∘ ⟨ f , g ⟩ ≈ f
  ⟨,⟩-projl {A} {B} = Bld.factorizer-proj (A ×′ B)


  ⟨,⟩-projr : ∀ {A B Z} {f : Z ⇒ A} {g : Z ⇒ B} → projr ∘ ⟨ f , g ⟩ ≈ g
  ⟨,⟩-projr {A} {B} = Bld.factorizer-proj (A ×′ B)


  ⟨,⟩-unique : ∀ {A B Z} {f : Z ⇒ A} {g : Z ⇒ B} {u}
    → f ≈ projl ∘ u
    → g ≈ projr ∘ u
    → ⟨ f , g ⟩ ≈ u
  ⟨,⟩-unique {A} {B} eql eqr
    = Bld.factorizer-unique (A ×′ B) _ (Bool-elim eql eqr)


  ⟨,⟩-∘ : ∀ {A B Y Z} {f : Y ⇒ Z} {g : Z ⇒ A} {h : Z ⇒ B}
    → ⟨ g , h ⟩ ∘ f ≈ ⟨ g ∘ f , h ∘ f ⟩
  ⟨,⟩-∘ {A} {B} {Y} {Z} {f} {g} {h}
      = begin
          ⟨ g , h ⟩ ∘ f
        ≈⟨ Bld.factorizer-∘ (A ×′ B) ⟩
          Bld.factorizer (A ×′ B)
            (λ i → Bool-elim {A = λ i → Z ⇒ Bool-elim A B i} g h i ∘ f)
        ≈⟨ Bld.factorizer-resp (A ×′ B) (Bool-elim ≈.refl ≈.refl) ⟩
          ⟨ g ∘ f , h ∘ f ⟩
        ∎


  ⟨,⟩-id : ∀ {A B} → ⟨ projl , projr ⟩ ≈ id {A × B}
  ⟨,⟩-id {A} {B} = ⟨,⟩-unique (≈.sym id-r) (≈.sym id-r)


  ⟨×⟩-resp : ∀ {A A′ B B′} {f f′ : A ⇒ A′} {g g′ : B ⇒ B′}
    → f ≈ f′
    → g ≈ g′
    → ⟨ f × g ⟩ ≈ ⟨ f′ × g′ ⟩
  ⟨×⟩-resp {A} {A′} {B} {B′} f≈f′ g≈g′
      = Bld.times-resp (A ×′ B) (A′ ×′ B′) (Bool-elim f≈f′ g≈g′)


  ⟨×⟩-projl : ∀ {A A′ B B′} {f : A ⇒ A′} {g : B ⇒ B′}
    → projl ∘ ⟨ f × g ⟩ ≈ f ∘ projl
  ⟨×⟩-projl {A} {A′} {B} {B′} = Bld.times-proj (A ×′ B) (A′ ×′ B′)


  ⟨×⟩-projr : ∀ {A A′ B B′} {f : A ⇒ A′} {g : B ⇒ B′}
    → projr ∘ ⟨ f × g ⟩ ≈ g ∘ projr
  ⟨×⟩-projr {A} {A′} {B} {B′} = Bld.times-proj (A ×′ B) (A′ ×′ B′)


  ⟨×⟩-id : ∀ {A B} → ⟨ id {A} × id {B} ⟩ ≈ id
  ⟨×⟩-id {A} {B} = Bld.factorizer-unique (A ×′ B) id
    (Bool-elim (≈.trans id-l (≈.sym id-r)) (≈.trans id-l (≈.sym id-r)))


  ⟨×⟩-∘ : ∀ {A A′ A″ B B′ B″}
    → {f : A′ ⇒ A″} {f′ : A ⇒ A′} {g : B′ ⇒ B″} {g′ : B ⇒ B′}
    → ⟨ f × g ⟩ ∘ ⟨ f′ × g′ ⟩ ≈ ⟨ f ∘ f′ × g ∘ g′ ⟩
  ⟨×⟩-∘ {A} {A′} {A″} {B} {B′} {B″} {f} {f′} {g} {g′} = ≈.trans
    (Bld.times-∘ (A ×′ B) (A′ ×′ B′) (A″ ×′ B″))
    (Bld.times-resp (A ×′ B) (A″ ×′ B″) (Bool-elim ≈.refl ≈.refl))


  ⟨×⟩-⟨,⟩ : ∀ {A B C B′ C′} {f : A ⇒ B} {g : A ⇒ C} {f′ : B ⇒ B′} {g′ : C ⇒ C′}
    → ⟨ f′ × g′ ⟩ ∘ ⟨ f , g ⟩ ≈ ⟨ f′ ∘ f , g′ ∘ g ⟩
  ⟨×⟩-⟨,⟩ {A} {B} {C} {B′} {C′} = ≈.trans
    (Bld.times-factorizer (B ×′ C) (B′ ×′ C′))
    (Bld.factorizer-resp (B′ ×′ C′) (Bool-elim ≈.refl ≈.refl))


  ×-resp-≅ : ∀ {A A′ B B′}
    → A ≅ A′
    → B ≅ B′
    → (A × B) ≅ (A′ × B′)
  ×-resp-≅ {A} {A′} {B} {B′} A≅A′ B≅B′
    = Bld.Product-resp-≅ (Bool-elim A≅A′ B≅B′) (A ×′ B) (A′ ×′ B′)


-- The following is conceptually trivial, but we have to dig quite deep to
-- avoid level-related nonsense.
HasProducts→HasBinaryProducts : ∀ {lp lo la l≈} {C : Category lo la l≈}
  → HasProducts lp C
  → HasBinaryProducts C
HasProducts→HasBinaryProducts {lp} {C = C} record { Π′ = Π }
    = record { _×′_ = _×_ }
  where
    open Category C
    open Unique.Build C
    open Product using (proj)
    open ∃!′ using (arr ; prop ; unique)

    _×_ : ∀ A B → Build.BinaryProduct C A B
    A × B = record
        { prod = prod′
        ; proj = proj′
        ; isProduct = isProduct′
        }
      where
        O : Lift lp Bool → _
        O (lift true) = A
        O (lift false) = B

        prod′ = Product.prod (Π O)

        proj′ = Bool-elim (proj (Π O) (lift true)) (proj (Π O) (lift false))

        isProduct′ : IsProduct C (Bool-elim A B) prod′ proj′
        isProduct′ {X} x = record
            { arr = arr′ ⃗
            ; prop = Bool-elim (prop arr′ (lift true)) (prop arr′ (lift false))
            ; unique = λ eq → unique arr′
                (λ { (lift true) → eq true ; (lift false) → eq false})
            }
          where
            arr′ = Product.isProduct (Π O)
              λ { (lift true) → x true ; (lift false) → x false}



record HasFiniteProducts {lo la l≈} (Cat : Category lo la l≈)
  : Set (lo ⊔ la ⊔ l≈)
  where

  field
    {{hasTerminal}} : HasTerminal Cat
    {{hasBinaryProducts}} : HasBinaryProducts Cat

  open HasTerminal hasTerminal public
  open HasBinaryProducts hasBinaryProducts public


module _ {lo la l≈ lo′ la′ l≈′}
  {C : Category lo la l≈}
  {D : Category lo′ la′ l≈′}
  where

  open Category C
  open Functor


  PreservesBinaryProducts : (F : Functor C D) → Set _
  PreservesBinaryProducts F
    = ∀ {A B A×B} {projl : A×B ⇒ A} {projr : A×B ⇒ B}
    → IsBinaryProduct C A×B projl projr
    → IsBinaryProduct D (fobj F A×B) (fmap F projl) (fmap F projr)


  PreservesProducts : ∀ {i} (I : Set i) (F : Functor C D) → Set _
  PreservesProducts I F
    = ∀ {O : I → Obj} {P} {proj : ∀ i → P ⇒ O i}
    → IsProduct C O P proj
    → IsProduct D (λ i → fobj F (O i)) (fobj F P) (λ i → fmap F (proj i))