cat/src/Cat/Category/Product.agda

module Cat.Category.Product where

open import Agda.Primitive
open import Cubical
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
        obj : Object
        proj₁ : ℂ [ obj , A ]
        proj₂ : ℂ [ obj , B ]

    record IsProduct (raw : RawProduct) : Set (ℓa ⊔ ℓb) where
      open RawProduct raw public
      field
        isProduct : ∀ {X : Object} (x₁ : ℂ [ X , A ]) (x₂ : ℂ [ X , B ])
          → ∃![ x ] (ℂ [ proj₁ ∘ x ] ≡ x₁ P.× ℂ [ proj₂ ∘ x ] ≡ x₂)

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

    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.obj (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 Propositionality where
  -- TODO `isProp (Product ...)`
  -- TODO `isProp (HasProducts ...)`