{-# 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