{-# OPTIONS --without-K --safe #-}

-- Bundled version of a Cartesian Category
module Categories.Category.Cartesian.Bundle where

open import Level

open import Categories.Category.Core using (Category)
open import Categories.Category.Cartesian using (Cartesian)
open import Categories.Category.Cartesian.Monoidal using (module CartesianMonoidal)
open import Categories.Category.Monoidal using (MonoidalCategory)

record CartesianCategory o ℓ e : Set (suc (o ⊔ ℓ ⊔ e)) where
  field
    U         : Category o ℓ e  -- U for underlying
    cartesian : Cartesian U

  open Category U public
  open Cartesian cartesian public

  monoidalCategory : MonoidalCategory o ℓ e
  monoidalCategory = record
    { U        = U
    ; monoidal = CartesianMonoidal.monoidal cartesian
    }