2項積

open import category-theory.category
module category-theory.binary-product
  {o h} (𝒞 : Category o h) where

open import foundations.universe
open import foundations.identity-type
open Category 𝒞

private variable
  Y Z : Ob
  f g : Hom Y Z

record isProduct A B X (π₁ : Hom X A) (π₂ : Hom X B) : Type (o ⊔ h) where
  field
    ⟨_,_⟩ : Hom Y A → Hom Y B → Hom Y X
    β₁ : π₁ ∘ ⟨ f , g ⟩ ＝ f
    β₂ : π₂ ∘ ⟨ f , g ⟩ ＝ g
    η : ⟨ π₁ ∘ f , π₂ ∘ f ⟩ ＝ f

record Product A B : Type (o ⊔ h) where
  field
    X : Ob
    π₁ : Hom X A
    π₂ : Hom X B
    is-product : isProduct A B X π₁ π₂

  open isProduct is-product public