1 files changed, 229 insertions, 0 deletions
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
+        }
+    }