Add monoids / monoid objects in setoids equivalencemain

6 files changed, 361 insertions, 18 deletions

diff --git a/Adjoint/Instance/List.agda b/Adjoint/Instance/List.agda
index 1b65985..6837c8d 100644
--- a/Adjoint/Instance/List.agda
+++ b/Adjoint/Instance/List.agda
@@ -12,6 +12,7 @@ open import Category.Instance.Setoids.SymmetricMonoidal {ℓ} {ℓ} using (Setoi
 
 module S = SymmetricMonoidalCategory Setoids-×
 
+open import Algebra.Morphism.Bundles using (MonoidHomomorphism)
 open import Categories.Adjoint using (_⊣_)
 open import Categories.Category.Construction.Monoids using (Monoids)
 open import Categories.Functor using (Functor; id; _∘F_)
@@ -19,7 +20,7 @@ open import Categories.NaturalTransformation using (NaturalTransformation; ntHel
 open import Categories.Object.Monoid S.monoidal using (Monoid; IsMonoid; Monoid⇒)
 open import Data.Monoid using (toMonoid; toMonoid⇒)
 open import Data.Opaque.List using ([-]ₛ; Listₛ; mapₛ; foldₛ; ++ₛ-homo; []ₛ-homo; fold-mapₛ; fold)
-open import Data.Product using (_,_; uncurry)
+open import Data.Product using (_,_)
 open import Data.Setoid using (∣_∣)
 open import Function using (_⟶ₛ_; _⟨$⟩_)
 open import Functor.Forgetful.Instance.Monoid {suc ℓ} {ℓ} {ℓ} using () renaming (Forget to Forget′)
@@ -70,10 +71,12 @@ opaque
       : {X Y : Monoid}
         (f : Monoid⇒ X Y)
         {x : ∣ Listₛ (Carrier X) ∣}
-      → (open Setoid (Carrier Y))
+        (open Setoid (Carrier Y))
       → arr (foldₘ Y) ⟨$⟩ (arr (mapₘ (arr f)) ⟨$⟩ x)
       ≈ arr f ⟨$⟩ (arr (foldₘ X) ⟨$⟩ x)
-  fold-mapₘ {X} {Y} f = uncurry (fold-mapₛ (toMonoid X) (toMonoid Y)) (toMonoid⇒ X Y f)
+  fold-mapₘ {X} {Y} f = fold-mapₛ (toMonoid X) (toMonoid Y) (record { cong = ⟦⟧-cong }) isMonoidHomomorphism
+    where
+      open MonoidHomomorphism (toMonoid⇒ X Y f)
 
 counit : NaturalTransformation (Free ∘F Forget) id
 counit = ntHelper record
diff --git a/Adjoint/Instance/Multiset.agda b/Adjoint/Instance/Multiset.agda
index c51baa9..5bc46ba 100644
--- a/Adjoint/Instance/Multiset.agda
+++ b/Adjoint/Instance/Multiset.agda
@@ -16,6 +16,7 @@ import Functor.Forgetful.Instance.CMonoid S.symmetric as CMonoid
 import Functor.Forgetful.Instance.Monoid S.monoidal as Monoid
 import Object.Monoid.Commutative S.symmetric as CMonoidObject
 
+open import Algebra.Morphism.Bundles using (MonoidHomomorphism)
 open import Categories.Adjoint using (_⊣_)
 open import Categories.Category using (Category)
 open import Categories.Functor using (Functor; id; _∘F_)
@@ -24,7 +25,7 @@ open import Category.Construction.CMonoids using (CMonoids)
 open import Data.CMonoid using (toCMonoid; toCMonoid⇒)
 open import Data.Monoid using (toMonoid; toMonoid⇒)
 open import Data.Opaque.Multiset using ([-]ₛ; Multisetₛ; foldₛ; ++ₛ-homo; []ₛ-homo; fold-mapₛ; fold)
-open import Data.Product using (_,_; uncurry)
+open import Data.Product using (_,_)
 open import Data.Setoid using (∣_∣)
 open import Function using (_⟶ₛ_; _⟨$⟩_)
 open import Functor.Free.Instance.CMonoid {ℓ} {ℓ} using (Multisetₘ; mapₘ; MultisetCMonoid) renaming (Free to Free′)
@@ -78,7 +79,9 @@ opaque
       → (open Setoid (Carrier Y))
       → arr (foldₘ Y) ⟨$⟩ (arr (mapₘ (arr f)) ⟨$⟩ x)
       ≈ arr f ⟨$⟩ (arr (foldₘ X) ⟨$⟩ x)
-  fold-mapₘ {X} {Y} f = uncurry (fold-mapₛ (toCMonoid X) (toCMonoid Y)) (toCMonoid⇒ X Y f)
+  fold-mapₘ {X} {Y} f = fold-mapₛ (toCMonoid X) (toCMonoid Y) (record { cong = ⟦⟧-cong }) isMonoidHomomorphism
+    where
+      open MonoidHomomorphism (toCMonoid⇒ X Y f)
 
 counit : NaturalTransformation (Free ∘F Forget) id
 counit = ntHelper record
diff --git a/Category/Equivalence/Instance/Monoids.agda b/Category/Equivalence/Instance/Monoids.agda
new file mode 100644
index 0000000..5de2e60
--- /dev/null
+++ b/Category/Equivalence/Instance/Monoids.agda
@@ -0,0 +1,229 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Level using (Level; suc; _⊔_)
+
+module Category.Equivalence.Instance.Monoids (c ℓ : Level) where
+
+open import Category.Instance.Monoids c ℓ using (Monoids; MonoidHomomorphism; mk-⇒; _≗_)
+
+import Algebra as Alg
+import Algebra.Morphism.Bundles as Raw
+
+open import Category.Instance.Setoids.SymmetricMonoidal {c} {ℓ} using (Setoids-×; ×-monoidal′)
+
+open import Categories.Category using (module Category; _[_∘_])
+open import Categories.Category.Construction.Monoids Setoids-×.monoidal using () renaming (Monoids to Monoids[Setoids])
+open import Categories.Category.Equivalence using (StrongEquivalence)
+open import Categories.Functor using (Functor; _∘F_) renaming (id to Id)
+open import Categories.NaturalTransformation.NaturalIsomorphism using (niHelper; _≃_)
+open import Categories.Object.Monoid Setoids-×.monoidal using (Monoid; Monoid⇒)
+open import Data.Monoid using (fromMonoid; toMonoid; fromMonoid⇒; toMonoid⇒)
+open import Function using (Func; _⟨$⟩_; _∘_) renaming (id to idf)
+open import Function.Construct.Identity using () renaming (function to IdFunc)
+open import Relation.Binary using (Setoid)
+
+open Category using (id)
+open Func
+open MonoidHomomorphism using (rawMonoidHomomorphism; ⟦_⟧)
+open Monoid⇒
+
+abstract opaque
+
+  unfolding fromMonoid⇒
+
+  identity⇒
+      : (A : Alg.Monoid c ℓ)
+        (open Alg.Monoid A)
+        {x : Carrier}
+      → arr (fromMonoid⇒ A A (rawMonoidHomomorphism (id Monoids {A}))) ⟨$⟩ x ≈ x
+  identity⇒ = Alg.Monoid.refl
+
+  homo⇒
+      : (X Y Z : Alg.Monoid c ℓ)
+        {f : MonoidHomomorphism X Y}
+        {g : MonoidHomomorphism Y Z}
+        {x : Alg.Monoid.Carrier X}
+        (open Alg.Monoid Z)
+      → arr (fromMonoid⇒ X Z (rawMonoidHomomorphism (Monoids [ g ∘ f ]))) ⟨$⟩ x
+      ≈ arr (fromMonoid⇒ Y Z (rawMonoidHomomorphism g)) ⟨$⟩ (arr (fromMonoid⇒ X Y (rawMonoidHomomorphism f)) ⟨$⟩ x)
+  homo⇒ X Y Z = Alg.Monoid.refl Z
+
+  resp⇒
+      : (A B : Alg.Monoid c ℓ)
+        {f g : MonoidHomomorphism A B}
+      → f ≗ g
+      → {x : Alg.Monoid.Carrier A}
+        (open Alg.Monoid B)
+      → arr (fromMonoid⇒ A B (rawMonoidHomomorphism f)) ⟨$⟩ x
+      ≈ arr (fromMonoid⇒ A B (rawMonoidHomomorphism g)) ⟨$⟩ x
+  resp⇒ A B f≗g {x} = f≗g x
+
+From : Functor Monoids Monoids[Setoids]
+From = record
+    { F₀ = fromMonoid
+    ; F₁ = λ {M N} f → fromMonoid⇒ M N (rawMonoidHomomorphism f)
+    ; identity = λ {A} → identity⇒ A
+    ; homomorphism = λ {X Y Z} → homo⇒ X Y Z
+    ; F-resp-≈ = λ {A B} → resp⇒ A B
+    }
+
+opaque
+
+  unfolding toMonoid⇒
+
+  identity⇐
+      : {A : Monoid}
+      → mk-⇒ (toMonoid⇒ A A (id Monoids[Setoids])) ≗ id Monoids {toMonoid A}
+  identity⇐ {A} _ = Alg.Monoid.refl (toMonoid A)
+
+  homo⇐
+      : {X Y Z : Monoid}
+        {f : Monoid⇒ X Y}
+        {g : Monoid⇒ Y Z}
+      → mk-⇒ (toMonoid⇒ X Z (Monoids[Setoids] [ g ∘ f ]))
+      ≗ _[_∘_] Monoids {toMonoid X} {toMonoid Y} {toMonoid Z} (mk-⇒ (toMonoid⇒ Y Z g)) (mk-⇒ (toMonoid⇒ X Y f))
+  homo⇐ {X} {Y} {Z} {f} {g} x = Alg.Monoid.refl (toMonoid Z)
+
+  resp⇐
+      : {A B : Monoid}
+        {f g : Monoid⇒ A B}
+      → (∀ {x} (open Setoid (Monoid.Carrier B)) → arr f ⟨$⟩ x ≈ arr g ⟨$⟩ x)
+      → _≗_ {toMonoid A} {toMonoid B} (mk-⇒ (toMonoid⇒ A B f)) (mk-⇒ (toMonoid⇒ A B g))
+  resp⇐ {A} {B} {f} {g} f≈g x = f≈g {x}
+
+To : Functor Monoids[Setoids] Monoids
+To = record
+    { F₀ = toMonoid
+    ; F₁ = λ {M N} f → mk-⇒ (toMonoid⇒ M N f)
+    ; identity = identity⇐
+    ; homomorphism = homo⇐
+    ; F-resp-≈ = resp⇐
+    }
+
+opaque
+
+  unfolding toMonoid Data.Monoid.FromMonoid.μ
+
+  from∘to⇒ : (M : Monoid) → Monoid⇒ (fromMonoid (toMonoid M)) M
+  from∘to⇒ M = let open Alg.Monoid (toMonoid M) in record
+      { arr = IdFunc setoid
+      ; preserves-μ = refl
+      ; preserves-η = refl
+      }
+
+  from∘to⇐ : (M : Monoid) → Monoid⇒ M (fromMonoid (toMonoid M))
+  from∘to⇐ M = let open Alg.Monoid (toMonoid M) in record
+      { arr = IdFunc setoid
+      ; preserves-μ = refl
+      ; preserves-η = refl
+      }
+
+  from∘to-isoˡ
+      : (M : Monoid)
+        (open Alg.Monoid (toMonoid M))
+      → {x : Alg.Monoid.Carrier (toMonoid M)}
+      → arr (from∘to⇐ M) ⟨$⟩ (arr (from∘to⇒ M) ⟨$⟩ x) ≈ x
+  from∘to-isoˡ M = Setoid.refl (Monoid.Carrier M)
+
+  from∘to-isoʳ
+      : (M : Monoid)
+        (open Setoid (Monoid.Carrier M))
+        {x : Setoid.Carrier (Monoid.Carrier M)}
+      → arr (from∘to⇒ M) ⟨$⟩ (arr (from∘to⇐ M) ⟨$⟩ x) ≈ x
+  from∘to-isoʳ M = Setoid.refl (Monoid.Carrier M)
+
+  opaque
+    unfolding fromMonoid⇒ toMonoid⇒
+    from∘to⇒-commute
+        : {M N : Monoid}
+          (f : Monoid⇒ M N)
+          {x : Alg.Monoid.Carrier (toMonoid M)}
+          (open Setoid (Monoid.Carrier N))
+        → arr (from∘to⇒ N) ⟨$⟩ (arr (fromMonoid⇒ (toMonoid M) (toMonoid N) (toMonoid⇒ M N f)) ⟨$⟩ x)
+        ≈ arr f ⟨$⟩ (arr (from∘to⇒ M) ⟨$⟩ x)
+    from∘to⇒-commute {M} {N} f = Setoid.refl (Monoid.Carrier N)
+
+From∘To : From ∘F To ≃ Id
+From∘To = niHelper record
+    { η = from∘to⇒
+    ; η⁻¹ = from∘to⇐
+    ; commute = from∘to⇒-commute
+    ; iso = λ M → record
+        { isoˡ = from∘to-isoˡ M
+        ; isoʳ = from∘to-isoʳ M
+        }
+    }
+
+opaque
+  unfolding toMonoid Data.Monoid.FromMonoid.μ
+  to∘from⇒ : (M : Alg.Monoid c ℓ) → MonoidHomomorphism (toMonoid (fromMonoid M)) M
+  to∘from⇒ M = let open Alg.Monoid M in mk-⇒ record
+      { ⟦_⟧ = idf
+      ; isMonoidHomomorphism = record
+          { isMagmaHomomorphism = record
+              { isRelHomomorphism = record
+                  { cong = idf
+                  }
+              ; homo = λ _ _ → refl
+              }
+          ; ε-homo = refl
+          }
+      }
+
+  to∘from⇐ : (M : Alg.Monoid c ℓ) → MonoidHomomorphism M (toMonoid (fromMonoid M))
+  to∘from⇐ M = let open Alg.Monoid M in mk-⇒ record
+      { ⟦_⟧ = idf
+      ; isMonoidHomomorphism = record
+          { isMagmaHomomorphism = record
+              { isRelHomomorphism = record
+                  { cong = idf
+                  }
+              ; homo = λ _ _ → refl
+              }
+          ; ε-homo = refl
+          }
+      }
+
+  to∘from-isoˡ
+      : (M : Alg.Monoid c ℓ)
+        (open Alg.Monoid (toMonoid (fromMonoid M)))
+      → Monoids [ to∘from⇐ M ∘ to∘from⇒ M ] ≗ id Monoids {toMonoid (fromMonoid M)}
+  to∘from-isoˡ M _ = Alg.Monoid.refl M
+
+  to∘from-isoʳ
+      : (M : Alg.Monoid c ℓ)
+        (open Alg.Monoid M)
+      → Monoids [ to∘from⇒ M ∘ to∘from⇐ M ] ≗ id Monoids {M}
+  to∘from-isoʳ M _ = Alg.Monoid.refl M
+
+  opaque
+    unfolding toMonoid⇒ fromMonoid⇒
+    to∘from⇒-commute
+        : {M N : Alg.Monoid c ℓ}
+          (f : MonoidHomomorphism M N)
+          (open Alg.Monoid N)
+        → Monoids [ to∘from⇒ N ∘ mk-⇒ (toMonoid⇒ (fromMonoid M) (fromMonoid N) (fromMonoid⇒ M N (rawMonoidHomomorphism f))) ]
+        ≗ Monoids [ f ∘ to∘from⇒ M ]
+    to∘from⇒-commute {_} {N} _ _ = Alg.Monoid.refl N
+
+To∘From : To ∘F From ≃ Id
+To∘From = niHelper record
+    { η = to∘from⇒
+    ; η⁻¹ = to∘from⇐
+    ; commute = to∘from⇒-commute
+    ; iso = λ M → record
+        { isoˡ = to∘from-isoˡ M
+        ; isoʳ = to∘from-isoʳ M
+        }
+    }
+
+-- The category of monoids is equivalent to the category of monoid objects in Setoids
+Monoids≈Monoids[Setoids] : StrongEquivalence Monoids Monoids[Setoids]
+Monoids≈Monoids[Setoids] = record
+    { F = From
+    ; G = To
+    ; weak-inverse = record
+        { F∘G≈id = From∘To
+        ; G∘F≈id = To∘From
+        }
+    }
diff --git a/Category/Instance/Monoids.agda b/Category/Instance/Monoids.agda
new file mode 100644
index 0000000..28f214b
--- /dev/null
+++ b/Category/Instance/Monoids.agda
@@ -0,0 +1,85 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Level using (Level; suc; _⊔_)
+
+module Category.Instance.Monoids (c ℓ : Level) where
+
+import Algebra.Morphism.Bundles as Raw
+import Algebra.Morphism.Construct.Composition as Compose
+import Algebra.Morphism.Construct.Identity as Identity
+
+open import Algebra using (Monoid)
+open import Categories.Category using (Category)
+open import Categories.Category.Helper using (categoryHelper)
+open import Relation.Binary using (IsEquivalence)
+
+open Monoid hiding (_≈_)
+
+record MonoidHomomorphism (M N : Monoid c ℓ) : Set (c ⊔ ℓ) where
+
+  constructor mk-⇒
+
+  field
+    rawMonoidHomomorphism : Raw.MonoidHomomorphism (rawMonoid M) (rawMonoid N)
+
+  open Raw.MonoidHomomorphism rawMonoidHomomorphism public
+
+module _ {M N : Monoid c ℓ} where
+
+  -- Pointwise equality of monoid homomorphisms
+
+  open MonoidHomomorphism
+
+  _≗_ : (f g : MonoidHomomorphism M N) → Set (c ⊔ ℓ)
+  _≗_ f g = (x : Carrier M) → let open Monoid N in ⟦ f ⟧ x ≈ ⟦ g ⟧ x
+
+  infix 4 _≗_
+
+  ≗-isEquivalence : IsEquivalence _≗_
+  ≗-isEquivalence = record
+      { refl = λ x → refl N
+      ; sym = λ f≈g x → sym N (f≈g x)
+      ; trans = λ f≈g g≈h x → trans N (f≈g x) (g≈h x)
+      }
+
+  module ≗ = IsEquivalence ≗-isEquivalence
+
+private
+
+  id : {M : Monoid c ℓ} → MonoidHomomorphism M M
+  id {M} = mk-⇒ record
+      { isMonoidHomomorphism = Identity.isMonoidHomomorphism (rawMonoid M) (refl M)
+      }
+
+  compose
+      : {M N P : Monoid c ℓ}
+      → MonoidHomomorphism N P
+      → MonoidHomomorphism M N
+      → MonoidHomomorphism M P
+  compose {P = P} f g = mk-⇒ record
+      { isMonoidHomomorphism =
+          Compose.isMonoidHomomorphism
+              (trans P)
+              g.isMonoidHomomorphism
+              f.isMonoidHomomorphism
+      }
+    where
+      module f = MonoidHomomorphism f
+      module g = MonoidHomomorphism g
+
+open MonoidHomomorphism
+
+-- the category of monoids and monoid homomorphisms
+Monoids : Category (suc (c ⊔ ℓ)) (c ⊔ ℓ) (c ⊔ ℓ)
+Monoids = categoryHelper record
+    { Obj = Monoid c ℓ
+    ; _⇒_ = MonoidHomomorphism
+    ; _≈_ = _≗_
+    ; id = id
+    ; _∘_ = compose
+    ; assoc = λ {_ _ _ Q} _ → refl Q
+    ; identityˡ = λ {_ B} _ → refl B
+    ; identityʳ = λ {_ B} _ → refl B
+    ; equiv = ≗-isEquivalence
+    ; ∘-resp-≈ = λ {C = C} {f g h i} eq₁ eq₂ x → trans C (⟦⟧-cong f (eq₂ x)) (eq₁ (⟦ i ⟧ x))
+    }
diff --git a/Data/CMonoid.agda b/Data/CMonoid.agda
index dd0277c..4d84921 100644
--- a/Data/CMonoid.agda
+++ b/Data/CMonoid.agda
@@ -5,7 +5,7 @@ module Data.CMonoid {c ℓ : Level} where
 
 import Algebra.Bundles as Alg
 
-open import Algebra.Morphism using (IsMonoidHomomorphism)
+open import Algebra.Morphism.Bundles using (MonoidHomomorphism)
 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)
@@ -63,6 +63,5 @@ module  _ (M N : CommutativeMonoid Setoids-×.symmetric) where
 
   toCMonoid⇒
       : CommutativeMonoid⇒ Setoids-×.symmetric M N
-      → Σ (M.setoid ⟶ₛ N.setoid) (λ f
-      → IsMonoidHomomorphism M.rawMonoid N.rawMonoid (to f))
+      → MonoidHomomorphism M.rawMonoid N.rawMonoid
   toCMonoid⇒ f = toMonoid⇒ (monoid M) (monoid N) (monoid⇒ f)
diff --git a/Data/Monoid.agda b/Data/Monoid.agda
index 02a8062..deeb1cc 100644
--- a/Data/Monoid.agda
+++ b/Data/Monoid.agda
@@ -6,7 +6,7 @@ module Data.Monoid {c ℓ : Level} where
 
 import Algebra.Bundles as Alg
 
-open import Algebra.Morphism using (IsMonoidHomomorphism)
+open import Algebra.Morphism.Bundles using (MonoidHomomorphism)
 open import Categories.Object.Monoid using (Monoid; Monoid⇒)
 open import Category.Instance.Setoids.SymmetricMonoidal {c} {ℓ} using (Setoids-×; ×-monoidal′)
 open import Data.Product using (curry′; uncurry′; _,_; Σ)
@@ -100,8 +100,10 @@ open FromMonoid using (fromMonoid) public
 
 module  _ (M N : Monoid Setoids-×.monoidal) where
 
-  module M = Alg.Monoid (toMonoid M)
-  module N = Alg.Monoid (toMonoid N)
+  private
+
+    module M = Alg.Monoid (toMonoid M)
+    module N = Alg.Monoid (toMonoid N)
 
   open Monoid⇒
 
@@ -111,12 +113,34 @@ module  _ (M N : Monoid Setoids-×.monoidal) where
 
     toMonoid⇒
         : Monoid⇒ Setoids-×.monoidal M N
-        → Σ (M.setoid ⟶ₛ N.setoid) (λ f
-        → IsMonoidHomomorphism M.rawMonoid N.rawMonoid (to f))
-    toMonoid⇒ f = arr f , record
-        { isMagmaHomomorphism = record
-            { isRelHomomorphism = record { cong = cong (arr f) }
-            ; homo = λ x y → preserves-μ f {x , y}
+        → MonoidHomomorphism M.rawMonoid N.rawMonoid
+    toMonoid⇒ f = record
+        { ⟦_⟧ = to (arr f)
+        ; isMonoidHomomorphism = record
+            { isMagmaHomomorphism = record
+                { isRelHomomorphism = record { cong = cong (arr f) }
+                ; homo = λ x y → preserves-μ f {x , y}
+                }
+            ; ε-homo = preserves-η f
             }
-        ; ε-homo = preserves-η f
+        }
+
+module  _ (M N : Alg.Monoid c ℓ) where
+
+  private
+
+    module M = Alg.Monoid M
+    module N = Alg.Monoid N
+
+  open MonoidHomomorphism
+
+  opaque
+    unfolding FromMonoid.μ
+    fromMonoid⇒
+        : MonoidHomomorphism M.rawMonoid N.rawMonoid
+        → Monoid⇒ Setoids-×.monoidal (fromMonoid M) (fromMonoid N)
+    fromMonoid⇒ f = record
+        { arr = record { cong = ⟦⟧-cong f }
+        ; preserves-μ = λ { {x , y} → homo f x y }
+        ; preserves-η = ε-homo f
         }