Update free and forgetful monoid functors

2 files changed, 59 insertions, 24 deletions

diff --git a/Functor/Forgetful/Instance/Monoid.agda b/Functor/Forgetful/Instance/Monoid.agda
index 2c786ef..2f9e4d8 100644
--- a/Functor/Forgetful/Instance/Monoid.agda
+++ b/Functor/Forgetful/Instance/Monoid.agda
@@ -1,23 +1,25 @@
 {-# OPTIONS --without-K --safe #-}
 
-open import Categories.Category.Monoidal using (MonoidalCategory)
+open import Categories.Category using (Category)
+open import Categories.Category.Monoidal using (Monoidal)
 open import Level using (Level)
 
-module Functor.Forgetful.Instance.Monoid {o ℓ e : Level} (S : MonoidalCategory o ℓ e) where
+module Functor.Forgetful.Instance.Monoid {o ℓ e : Level} {S : Category o ℓ e} (monoidal : Monoidal S) where
 
 open import Categories.Category.Construction.Monoids using (Monoids)
 open import Categories.Functor using (Functor)
 open import Categories.Object.Monoid using (Monoid; Monoid⇒)
 open import Function using (id)
 
-module S = MonoidalCategory S
+private
+  module S = Category S
 
 open Monoid
 open Monoid⇒
 open S.Equiv using (refl)
 open Functor
 
-Forget : Functor (Monoids S.monoidal) S.U
+Forget : Functor (Monoids monoidal) S
 Forget .F₀ = Carrier
 Forget .F₁ = arr
 Forget .identity = refl
diff --git a/Functor/Free/Instance/Monoid.agda b/Functor/Free/Instance/Monoid.agda
index 34fa2dd..e08e42d 100644
--- a/Functor/Free/Instance/Monoid.agda
+++ b/Functor/Free/Instance/Monoid.agda
@@ -1,17 +1,18 @@
 {-# OPTIONS --without-K --safe #-}
 
-open import Level using (Level; _⊔_)
+open import Level using (Level; _⊔_; suc)
 
 module Functor.Free.Instance.Monoid {c ℓ : Level} where
 
 import Categories.Object.Monoid as MonoidObject
 
+open import Categories.Category using (Category)
 open import Categories.Category.Construction.Monoids using (Monoids)
 open import Categories.Category.Instance.Setoids using (Setoids)
 open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory)
 open import Categories.Functor using (Functor)
 open import Categories.NaturalTransformation using (NaturalTransformation)
-open import Category.Instance.Setoids.SymmetricMonoidal {c} {c ⊔ ℓ} using (Setoids-×)
+open import Category.Instance.Setoids.SymmetricMonoidal {c} {c ⊔ ℓ} using (Setoids-×; ×-monoidal′)
 open import Data.List.Properties using (++-assoc; ++-identityˡ; ++-identityʳ)
 open import Data.Opaque.List using ([]ₛ; Listₛ; ++ₛ; mapₛ)
 open import Data.Product using (_,_)
@@ -24,11 +25,13 @@ open import Relation.Binary using (Setoid)
 open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
 
 module Setoids-× = SymmetricMonoidalCategory Setoids-×
+
 module ++ = NaturalTransformation ++
 module ⊤⇒[] = NaturalTransformation ⊤⇒[]
 
 open Functor
 open MonoidObject Setoids-×.monoidal using (Monoid; IsMonoid; Monoid⇒)
+
 open IsMonoid
 
 -- the functor sending a setoid A to the monoid List A
@@ -57,29 +60,59 @@ module _ (X : Setoid c ℓ) where
         → x ≈ ++ₛ ⟨$⟩ (x , []ₛ ⟨$⟩ _)
     ++ₛ-identityʳ x = sym (reflexive (++-identityʳ x))
 
-  ListMonoid : IsMonoid (List.₀ X)
-  ListMonoid .μ = ++.η X
-  ListMonoid .η = ⊤⇒[].η X
-  ListMonoid .assoc {(x , y) , z} = ++ₛ-assoc x y z
-  ListMonoid .identityˡ {bro , x} = ++ₛ-identityˡ x
-  ListMonoid .identityʳ {x , _} = ++ₛ-identityʳ x
+  opaque
+
+    unfolding ×-monoidal′
+
+    ListMonoid : IsMonoid (List.₀ X)
+    ListMonoid = record
+        { μ = ++.η X
+        ; η = ⊤⇒[].η X
+        ; assoc = λ { {(x , y) , z} → ++ₛ-assoc x y z }
+        ; identityˡ = λ { {_ , x} → ++ₛ-identityˡ x }
+        ; identityʳ = λ { {x , _} → ++ₛ-identityʳ x }
+        }
 
 Listₘ : Setoid c ℓ → Monoid
 Listₘ X = record { isMonoid = ListMonoid X }
 
-mapₘ
-    : {Aₛ Bₛ : Setoid c ℓ}
-      (f : Aₛ ⟶ₛ Bₛ)
-    → Monoid⇒ (Listₘ Aₛ) (Listₘ Bₛ)
-mapₘ f = record
-    { arr = List.₁ f
-    ; preserves-μ = λ {x,y} → ++.sym-commute f {x,y}
-    ; preserves-η = ⊤⇒[].sym-commute f
-    }
+opaque
+
+  unfolding ListMonoid
+
+  mapₘ
+      : {Aₛ Bₛ : Setoid c ℓ}
+        (f : Aₛ ⟶ₛ Bₛ)
+      → Monoid⇒ (Listₘ Aₛ) (Listₘ Bₛ)
+  mapₘ f = record
+      { arr = List.₁ f
+      ; preserves-μ = λ {x,y} → ++.sym-commute f {x,y}
+      ; preserves-η = ⊤⇒[].sym-commute f
+      }
+
+module U = Category Setoids-×.U
+open Monoid⇒ using (arr)
+open import Function.Construct.Identity using () renaming (function to Id)
+open import Function.Construct.Composition using () renaming (function to compose)
+opaque
+  unfolding mapₘ
+  Free-identity : {X : Setoid c ℓ} → arr (mapₘ (Id X)) U.≈ U.id
+  Free-identity = List.identity
+
+  Free-homomorphism : {X Y Z : Setoid c ℓ} {f : X ⟶ₛ Y} {g : Y ⟶ₛ Z} → arr (mapₘ (compose f g)) U.≈ arr (mapₘ g) U.∘ arr (mapₘ f)
+  Free-homomorphism = List.homomorphism
+
+  Free-resp-≈
+      : {X Y : Setoid c ℓ}
+        {f g : X ⟶ₛ Y}
+        (let module Y = Setoid Y)
+      → (∀ {x} → f ⟨$⟩ x Y.≈ g ⟨$⟩ x)
+      → arr (mapₘ f) U.≈ arr (mapₘ g)
+  Free-resp-≈ = List.F-resp-≈
 
 Free : Functor (Setoids c ℓ) (Monoids Setoids-×.monoidal)
 Free .F₀ = Listₘ
 Free .F₁ = mapₘ
-Free .identity {X} = List.identity {X}
-Free .homomorphism {X} {Y} {Z} {f} {g} = List.homomorphism {X} {Y} {Z} {f} {g}
-Free .F-resp-≈ {A} {B} {f} {g} = List.F-resp-≈ {A} {B} {f} {g}
+Free .identity = Free-identity
+Free .homomorphism = Free-homomorphism
+Free .F-resp-≈ = Free-resp-≈