diff options
Diffstat (limited to 'Category/Cartesian/Instance/SymMonCat.agda')
| -rw-r--r-- | Category/Cartesian/Instance/SymMonCat.agda | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/Category/Cartesian/Instance/SymMonCat.agda b/Category/Cartesian/Instance/SymMonCat.agda new file mode 100644 index 0000000..7d91d52 --- /dev/null +++ b/Category/Cartesian/Instance/SymMonCat.agda @@ -0,0 +1,16 @@ +{-# OPTIONS --without-K --safe #-} + +open import Level using (Level; suc; _⊔_) + +module Category.Cartesian.Instance.SymMonCat {o ℓ e : Level} where + +open import Category.Instance.SymMonCat {o} {ℓ} {e} using (SymMonCat) +open import Category.Instance.Properties.SymMonCat {o} {ℓ} {e} using (SymMonCat-Cartesian) +open import Categories.Category.Cartesian.Bundle using (CartesianCategory) + +SymMonCat-CC : CartesianCategory (suc (o ⊔ ℓ ⊔ e)) (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e) +SymMonCat-CC = record + { U = SymMonCat + ; cartesian = SymMonCat-Cartesian + } + |