Show category of commutative conoids is cartesian

1 files changed, 56 insertions, 0 deletions

diff --git a/Category/Cartesian/Instance/CMonoids.agda b/Category/Cartesian/Instance/CMonoids.agda
new file mode 100644
index 0000000..7a64d88
--- /dev/null
+++ b/Category/Cartesian/Instance/CMonoids.agda
@@ -0,0 +1,56 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Level using (Level; suc; _⊔_)
+
+module Category.Cartesian.Instance.CMonoids {c ℓ : Level} where
+
+import Algebra.Construct.DirectProduct as ×
+import Algebra.Construct.Terminal as Term
+import Algebra.Morphism.Construct.DirectProduct as ×-⇒
+import Algebra.Morphism.Construct.Terminal as Term-⇒
+
+open import Algebra using (CommutativeMonoid)
+open import Categories.Category.BinaryProducts using (BinaryProducts)
+open import Categories.Category.Cartesian using (Cartesian)
+open import Categories.Category.Cartesian.Bundle using (CartesianCategory)
+open import Categories.Object.Terminal using (Terminal)
+open import Category.Instance.CMonoids c ℓ using (CMonoids; CMonoidHomomorphism; mk-⇒)
+open import Data.Product using (_,_)
+open import Data.Unit.Polymorphic using (tt)
+
+open CMonoidHomomorphism using (isMonoidHomomorphism)
+open CommutativeMonoid using (rawMonoid; refl; sym)
+
+terminal : Terminal CMonoids
+terminal = record
+    { ⊤ = Term.commutativeMonoid
+    ; ⊤-is-terminal = record
+        { ! = λ {M} → mk-⇒ record { isMonoidHomomorphism = Term-⇒.isMonoidHomomorphism (rawMonoid M) }
+        ; !-unique = λ _ _ → tt
+        }
+    }
+
+products : BinaryProducts CMonoids
+products = record
+    { product = λ {M N} → record
+        { A×B = ×.commutativeMonoid M N
+        ; π₁ = mk-⇒ record { isMonoidHomomorphism = ×-⇒.Monoid-Export.proj₁ {refl = refl M} }
+        ; π₂ = mk-⇒ record { isMonoidHomomorphism = ×-⇒.Monoid-Export.proj₂ {refl = refl N} }
+        ; ⟨_,_⟩ = λ {C} f g → mk-⇒ record
+            { isMonoidHomomorphism = ×-⇒.Monoid-Export.< isMonoidHomomorphism f , isMonoidHomomorphism g > }
+        ; project₁ = λ _ → refl M
+        ; project₂ = λ _ → refl N
+        ; unique = λ eq₁ eq₂ x → sym M (eq₁ x) , sym N (eq₂ x)
+        }
+    }
+
+CMonoids-Cartesian : Cartesian CMonoids
+CMonoids-Cartesian = record
+    { terminal = terminal
+    ; products = products
+    }
+
+CMonoids-CC : CartesianCategory (suc (c ⊔ ℓ)) (c ⊔ ℓ) (c ⊔ ℓ)
+CMonoids-CC = record { cartesian = CMonoids-Cartesian }
+
+module CMonoids-CC = CartesianCategory CMonoids-CC