From 970edad9a35db978d66e648bf5d4379787197eb0 Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Wed, 15 Oct 2025 20:54:35 -0500 Subject: Add monoidal categories for Nat and Nat-op --- Category/Monoidal/Instance/Nat.agda | 37 +++++++++++++++++++++++++++++++++++++ 1 file changed, 37 insertions(+) create mode 100644 Category/Monoidal/Instance/Nat.agda (limited to 'Category/Monoidal') diff --git a/Category/Monoidal/Instance/Nat.agda b/Category/Monoidal/Instance/Nat.agda new file mode 100644 index 0000000..9f1b990 --- /dev/null +++ b/Category/Monoidal/Instance/Nat.agda @@ -0,0 +1,37 @@ +{-# OPTIONS --without-K --safe #-} + +module Category.Monoidal.Instance.Nat where + +open import Level using (0ℓ) +open import Categories.Category.Monoidal.Bundle using (MonoidalCategory) +open import Categories.Category.Instance.Nat using (Nat; Nat-Cartesian; Nat-Cocartesian; Natop) +open import Categories.Category.Cartesian using (Cartesian) +open import Categories.Category.Cocartesian using (Cocartesian; module CocartesianMonoidal) +open import Categories.Category.Cartesian.Monoidal using (module CartesianMonoidal) +open import Categories.Category.Duality using (coCartesian⇒Cocartesian; Cocartesian⇒coCartesian) + +open CartesianMonoidal using () renaming (monoidal to ×-monoidal) +open CocartesianMonoidal using (+-monoidal) +open MonoidalCategory + +Natop-Cartesian : Cartesian Natop +Natop-Cartesian = Cocartesian⇒coCartesian Nat Nat-Cocartesian + +Natop-Cocartesian : Cocartesian Natop +Natop-Cocartesian = coCartesian⇒Cocartesian Natop Nat-Cartesian + +Nat,+,0 : MonoidalCategory 0ℓ 0ℓ 0ℓ +Nat,+,0 .U = Nat +Nat,+,0 .monoidal = +-monoidal Nat Nat-Cocartesian + +Nat,×,1 : MonoidalCategory 0ℓ 0ℓ 0ℓ +Nat,×,1 .U = Nat +Nat,×,1 .monoidal = ×-monoidal Nat-Cartesian + +Natop,+,0 : MonoidalCategory 0ℓ 0ℓ 0ℓ +Natop,+,0 .U = Natop +Natop,+,0 .monoidal = ×-monoidal Natop-Cartesian + +Natop,×,1 : MonoidalCategory 0ℓ 0ℓ 0ℓ +Natop,×,1 .U = Natop +Natop,×,1 .monoidal = +-monoidal Natop Natop-Cocartesian -- cgit v1.2.3