From f84a8d1bf9525aa9a005c1a31045b7685c6ac059 Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Thu, 1 Jan 2026 14:31:42 -0600
Subject: Update push, pull, and sys functors

---
 Data/CMonoid.agda | 25 ++++++++-----------------
 1 file changed, 8 insertions(+), 17 deletions(-)

(limited to 'Data/CMonoid.agda')

diff --git a/Data/CMonoid.agda b/Data/CMonoid.agda
index 8aaf869..dd0277c 100644
--- a/Data/CMonoid.agda
+++ b/Data/CMonoid.agda
@@ -3,19 +3,16 @@
 open import Level using (Level)
 module Data.CMonoid {c ℓ : Level} where
 
-open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory)
+import Algebra.Bundles as Alg
+
+open import Algebra.Morphism using (IsMonoidHomomorphism)
+open import Categories.Object.Monoid using (Monoid)
 open import Category.Instance.Setoids.SymmetricMonoidal {c} {ℓ} using (Setoids-×; ×-symmetric′)
+open import Data.Monoid {c} {ℓ} using (toMonoid; fromMonoid; toMonoid⇒; module FromMonoid)
+open import Data.Product using (_,_; Σ)
+open import Function using (Func; _⟨$⟩_; _⟶ₛ_)
 open import Object.Monoid.Commutative using (CommutativeMonoid; CommutativeMonoid⇒)
-open import Categories.Object.Monoid using (Monoid)
-
-open import Data.Monoid {c} {ℓ} using (toMonoid; fromMonoid; toMonoid⇒)
 
-import Algebra.Bundles as Alg
-
-open import Data.Setoid using (∣_∣)
-open import Relation.Binary using (Setoid)
-open import Function using (Func; _⟨$⟩_)
-open import Data.Product using (curry′; uncurry′; _,_)
 open Func
 
 -- A commutative monoid object in the (symmetric monoidal) category of setoids
@@ -37,9 +34,6 @@ toCMonoid M = record
       comm : (x y : M.Carrier) → x M.∙ y M.≈ y M.∙ x
       comm x y = commutative {x , y}
 
-open import Function.Construct.Constant using () renaming (function to Const)
-open import Data.Setoid.Unit using (⊤ₛ)
-
 fromCMonoid : Alg.CommutativeMonoid c ℓ → CommutativeMonoid Setoids-×.symmetric
 fromCMonoid M = record
     { M
@@ -53,7 +47,7 @@ fromCMonoid M = record
     module M = Monoid (fromMonoid monoid)
     open Setoids-× using (_≈_; _∘_; module braiding)
     opaque
-      unfolding toMonoid
+      unfolding FromMonoid.μ
       commutative : M.μ ≈ M.μ ∘ braiding.⇒.η _
       commutative {x , y} = comm x y
 
@@ -64,9 +58,6 @@ module  _ (M N : CommutativeMonoid Setoids-×.symmetric) where
   module M = Alg.CommutativeMonoid (toCMonoid M)
   module N = Alg.CommutativeMonoid (toCMonoid N)
 
-  open import Data.Product using (Σ; _,_)
-  open import Function using (_⟶ₛ_)
-  open import Algebra.Morphism using (IsMonoidHomomorphism)
   open CommutativeMonoid
   open CommutativeMonoid⇒
 
-- 
cgit v1.2.3