diff options
| -rw-r--r-- | Category/Cartesian/Instance/CMonoids.agda | 56 |
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 |