{-# OPTIONS --allow-unsolved-metas #-}
module Cat.Category.Product where

open import Agda.Primitive
open import Cubical
open import Cubical.NType.Properties using (lemPropF)

open import Data.Product as P hiding (_×_ ; proj₁ ; proj₂)

open import Cat.Category hiding (module Propositionality)

module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where

  open Category ℂ

  module _ (A B : Object) where
    record RawProduct : Set (ℓa ⊔ ℓb) where
      no-eta-equality
      field
        object : Object
        proj₁  : ℂ [ object , A ]
        proj₂  : ℂ [ object , B ]

    -- FIXME Not sure this is actually a proposition - so this name is
    -- misleading.
    record IsProduct (raw : RawProduct) : Set (ℓa ⊔ ℓb) where
      open RawProduct raw public
      field
        ump : ∀ {X : Object} (f : ℂ [ X , A ]) (g : ℂ [ X , B ])
          → ∃![ f×g ] (ℂ [ proj₁ ∘ f×g ] ≡ f P.× ℂ [ proj₂ ∘ f×g ] ≡ g)

      -- | Arrow product
      _P[_×_] : ∀ {X} → (π₁ : ℂ [ X , A ]) (π₂ : ℂ [ X , B ])
        → ℂ [ X , object ]
      _P[_×_] π₁ π₂ = P.proj₁ (ump π₁ π₂)

    record Product : Set (ℓa ⊔ ℓb) where
      field
        raw        : RawProduct
        isProduct  : IsProduct raw

      open IsProduct isProduct public

  record HasProducts : Set (ℓa ⊔ ℓb) where
    field
      product : ∀ (A B : Object) → Product A B

    _×_ : Object → Object → Object
    A × B = Product.object (product A B)

    -- | Parallel product of arrows
    --
    -- The product mentioned in awodey in Def 6.1 is not the regular product of
    -- arrows. It's a "parallel" product
    module _ {A A' B B' : Object} where
      open Product
      open Product (product A B) hiding (_P[_×_]) renaming (proj₁ to fst ; proj₂ to snd)
      _|×|_ : ℂ [ A , A' ] → ℂ [ B , B' ] → ℂ [ A × B , A' × B' ]
      f |×| g = product A' B'
        P[ ℂ [ f ∘ fst ]
        ×  ℂ [ g ∘ snd ]
        ]

module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} {A B : Category.Object ℂ} where
  private
    open Category ℂ
    module _ (raw : RawProduct ℂ A B) where
      module _ (x y : IsProduct ℂ A B raw) where
        private
          module x = IsProduct x
          module y = IsProduct y

        module _ {X : Object} (f : ℂ [ X , A ]) (g : ℂ [ X , B ]) where
          prodAux : x.ump f g ≡ y.ump f g
          prodAux = {!!}

        propIsProduct' : x ≡ y
        propIsProduct' i = record { ump = λ f g → prodAux f g i }

      propIsProduct : isProp (IsProduct ℂ A B raw)
      propIsProduct = propIsProduct'

  Product≡ : {x y : Product ℂ A B} → (Product.raw x ≡ Product.raw y) → x ≡ y
  Product≡ {x} {y} p i = record { raw = p i ; isProduct = q i }
    where
    q : (λ i → IsProduct ℂ A B (p i)) [ Product.isProduct x ≡ Product.isProduct y ]
    q = lemPropF propIsProduct p

module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} {A B : Category.Object ℂ} where
  open Category ℂ
  private
    module _ (x y : HasProducts ℂ) where
      private
        module x = HasProducts x
        module y = HasProducts y
      module _ (A B : Object) where
        module pX = Product (x.product A B)
        module pY = Product (y.product A B)
        objEq : pX.object ≡ pY.object
        objEq = {!!}
        proj₁Eq : (λ i → ℂ [ objEq i , A ]) [ pX.proj₁ ≡ pY.proj₁ ]
        proj₁Eq = {!!}
        proj₂Eq : (λ i → ℂ [ objEq i , B ]) [ pX.proj₂ ≡ pY.proj₂ ]
        proj₂Eq = {!!}
        rawEq : pX.raw ≡ pY.raw
        RawProduct.object (rawEq i) = objEq i
        RawProduct.proj₁  (rawEq i) = {!!}
        RawProduct.proj₂  (rawEq i) = {!!}

        isEq : (λ i → IsProduct ℂ A B (rawEq i)) [ pX.isProduct ≡ pY.isProduct ]
        isEq = {!!}

        appEq : x.product A B ≡ y.product A B
        appEq = Product≡ rawEq

      productEq : x.product ≡ y.product
      productEq i = λ A B → appEq A B i

      propHasProducts' : x ≡ y
      propHasProducts' i = record { product = productEq i }

  propHasProducts : isProp (HasProducts ℂ)
  propHasProducts = propHasProducts'