1 files changed, 74 insertions, 0 deletions

diff --git a/Category/Construction/CMonoids/Properties.agda b/Category/Construction/CMonoids/Properties.agda
new file mode 100644
index 0000000..fab8b0b
--- /dev/null
+++ b/Category/Construction/CMonoids/Properties.agda
@@ -0,0 +1,74 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Categories.Category.Core using (Category)
+open import Categories.Category.Monoidal.Core using (Monoidal)
+open import Categories.Category.Monoidal.Symmetric using (Symmetric)
+open import Level using (Level; _⊔_)
+
+module Category.Construction.CMonoids.Properties
+    {o ℓ e : Level}
+    {𝒞 : Category o ℓ e}
+    {monoidal : Monoidal 𝒞}
+    (symmetric : Symmetric monoidal)
+  where
+
+import Categories.Category.Monoidal.Reasoning monoidal as ⊗-Reasoning
+import Categories.Morphism.Reasoning 𝒞 as ⇒-Reasoning
+import Category.Construction.Monoids.Properties {o} {ℓ} {e} {𝒞} monoidal as Monoids
+
+open import Categories.Category using (_[_,_])
+open import Categories.Category.Monoidal.Symmetric.Properties symmetric using (module Shorthands)
+open import Categories.Morphism using (_≅_)
+open import Categories.Morphism.Notation using (_[_≅_])
+open import Categories.Object.Monoid monoidal using (Monoid)
+open import Category.Construction.CMonoids symmetric using (CMonoids)
+open import Data.Product using (Σ-syntax; _,_)
+open import Object.Monoid.Commutative symmetric using (CommutativeMonoid)
+
+module 𝒞 = Category 𝒞
+
+open CommutativeMonoid using (monoid) renaming (Carrier to ∣_∣)
+
+transport-by-iso
+    : {X : 𝒞.Obj}
+    → (M : CommutativeMonoid)
+    → 𝒞 [ ∣ M ∣ ≅ X ]
+    → Σ[ Xₘ ∈ CommutativeMonoid ] CMonoids [ M ≅ Xₘ ]
+transport-by-iso {X} M ∣M∣≅X
+  using (Xₘ′ , M≅Xₘ′) ← Monoids.transport-by-iso {X} (monoid M) ∣M∣≅X = Xₘ , M≅Xₘ
+  where
+    module M≅Xₘ′ = _≅_ M≅Xₘ′
+    open _≅_ ∣M∣≅X
+    module Xₘ′ = Monoid Xₘ′
+    open CommutativeMonoid M
+    open 𝒞 using (_≈_; _∘_)
+    open Shorthands
+    open ⊗-Reasoning
+    open ⇒-Reasoning
+    open Symmetric symmetric using (_⊗₁_; module braiding)
+    comm : from ∘ μ ∘ to ⊗₁ to ≈ (from ∘ μ ∘ to ⊗₁ to) ∘ σ⇒
+    comm = begin
+        from ∘ μ ∘ to ⊗₁ to         ≈⟨ push-center (commutative) ⟩
+        from ∘ μ ∘ σ⇒ ∘ to ⊗₁ to    ≈⟨ pushʳ (pushʳ (braiding.⇒.commute (to , to))) ⟩
+        (from ∘ μ ∘ to ⊗₁ to) ∘ σ⇒  ∎
+    Xₘ : CommutativeMonoid
+    Xₘ = record
+        { Carrier = X
+        ; isCommutativeMonoid = record
+            { isMonoid = Xₘ′.isMonoid
+            ; commutative = comm
+            }
+        }
+    M⇒Xₘ : CMonoids [ M , Xₘ ]
+    M⇒Xₘ = record { monoid⇒ = M≅Xₘ′.from }
+    Xₘ⇒M : CMonoids [ Xₘ , M ]
+    Xₘ⇒M = record { monoid⇒ = M≅Xₘ′.to }
+    M≅Xₘ : CMonoids [ M ≅ Xₘ ]
+    M≅Xₘ = record
+        { from = M⇒Xₘ
+        ; to = Xₘ⇒M
+        ; iso = record
+            { isoˡ = isoˡ
+            ; isoʳ = isoʳ
+            }
+        }