{-# OPTIONS --without-K --safe #-}
open import Categories.Category

--(Binary) product of objects and morphisms

module Categories.Object.Product {o ℓ e} (C : Category o ℓ e) where

open import Categories.Object.Product.Core C public
open import Categories.Object.Product.Morphisms C public