{-# OPTIONS --without-K --safe #-}
 
open import Categories.Category using (Category)
 
-- Defines the following properties of a Category:
-- Cartesian -- a Cartesian category is a category with all products
 
--  (for the induced Monoidal structure, see Cartesian.Monoidal)
 
module Categories.Category.Cartesian {o ℓ e} (𝒞 : Category o ℓ e) where
 
open import Level using (levelOfTerm)
open import Data.Nat using (ℕ; zero; suc)
 
open Category 𝒞
open HomReasoning
 
open import Categories.Category.BinaryProducts 𝒞 using (BinaryProducts; module BinaryProducts)
open import Categories.Object.Terminal 𝒞 using (Terminal)
 
private
  variable
    A B C D W X Y Z : Obj
    f f′ g g′ h i : A ⇒ B
 
-- Cartesian monoidal category
record Cartesian : Set (levelOfTerm 𝒞) where
  field
    terminal : Terminal
    products : BinaryProducts
  open BinaryProducts products using (_×_)
 
  power : Obj → ℕ → Obj
  power A  = Terminal.⊤ terminal
  power A  = A
  power A (suc (suc n)) = A × power A (suc n)