4 files changed, 118 insertions, 68 deletions
diff --git a/Functor/Forgetful/Instance/Monoid.agda b/Functor/Forgetful/Instance/Monoid.agda
new file mode 100644
index 0000000..2c786ef
--- /dev/null
+++ b/Functor/Forgetful/Instance/Monoid.agda
@@ -0,0 +1,27 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Categories.Category.Monoidal using (MonoidalCategory)
+open import Level using (Level)
+
+module Functor.Forgetful.Instance.Monoid {o ℓ e : Level} (S : MonoidalCategory o ℓ e) 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
+
+open Monoid
+open Monoid⇒
+open S.Equiv using (refl)
+open Functor
+
+Forget : Functor (Monoids S.monoidal) S.U
+Forget .F₀ = Carrier
+Forget .F₁ = arr
+Forget .identity = refl
+Forget .homomorphism = refl
+Forget .F-resp-≈ = id
+
+module Forget = Functor Forget
diff --git a/Functor/Free/Instance/Monoid.agda b/Functor/Free/Instance/Monoid.agda
new file mode 100644
index 0000000..34fa2dd
--- /dev/null
+++ b/Functor/Free/Instance/Monoid.agda
@@ -0,0 +1,85 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Level using (Level; _⊔_)
+
+module Functor.Free.Instance.Monoid {c ℓ : Level} where
+
+import Categories.Object.Monoid as MonoidObject
+
+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 Data.List.Properties using (++-assoc; ++-identityˡ; ++-identityʳ)
+open import Data.Opaque.List using ([]ₛ; Listₛ; ++ₛ; mapₛ)
+open import Data.Product using (_,_)
+open import Data.Setoid using (∣_∣)
+open import Function using (_⟶ₛ_; _⟨$⟩_)
+open import Functor.Instance.List {c} {ℓ} using (List)
+open import NaturalTransformation.Instance.EmptyList {c} {ℓ} using (⊤⇒[])
+open import NaturalTransformation.Instance.ListAppend {c} {ℓ} using (++)
+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
+
+module _ (X : Setoid c ℓ) where
+
+  open Setoid (List.₀ X)
+
+  opaque
+
+    unfolding []ₛ
+
+    ++ₛ-assoc
+        : (x y z : ∣ Listₛ X ∣)
+        → ++ₛ ⟨$⟩ (++ₛ ⟨$⟩ (x , y) , z)
+        ≈ ++ₛ ⟨$⟩ (x , ++ₛ ⟨$⟩ (y , z))
+    ++ₛ-assoc x y z = reflexive (++-assoc x y z)
+
+    ++ₛ-identityˡ
+        : (x : ∣ Listₛ X ∣)
+        → x ≈ ++ₛ ⟨$⟩ ([]ₛ ⟨$⟩ _ , x)
+    ++ₛ-identityˡ x = reflexive (++-identityˡ x)
+
+    ++ₛ-identityʳ
+        : (x : ∣ Listₛ X ∣)
+        → 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
+
+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
+    }
+
+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}
diff --git a/Functor/Instance/FreeMonoid.agda b/Functor/Instance/FreeMonoid.agda
deleted file mode 100644
index bb26fd4..0000000
--- a/Functor/Instance/FreeMonoid.agda
+++ /dev/null
@@ -1,64 +0,0 @@
-{-# OPTIONS --without-K --safe #-}
-
-open import Level using (Level; _⊔_)
-
-module Functor.Instance.FreeMonoid {c ℓ : Level} where
-
-import Categories.Object.Monoid as MonoidObject
-
-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 Data.List.Properties using (++-assoc; ++-identityˡ; ++-identityʳ)
-open import Data.Product using (_,_)
-open import Function using (_⟶ₛ_)
-open import Functor.Instance.List {c} {ℓ} using (List)
-open import NaturalTransformation.Instance.EmptyList {c} {ℓ} using (⊤⇒[])
-open import NaturalTransformation.Instance.ListAppend {c} {ℓ} using (++)
-open import Relation.Binary using (Setoid)
-open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
-
-module List = Functor List
-module Setoids-× = SymmetricMonoidalCategory Setoids-×
-module ++ = NaturalTransformation ++
-module ⊤⇒[] = NaturalTransformation ⊤⇒[]
-
-open Functor
-open MonoidObject Setoids-×.monoidal using (Monoid; IsMonoid; Monoid⇒)
-open IsMonoid
-
-module _ (X : Setoid c ℓ) where
-
-  private
-    module X = Setoid X
-    module ListX = Setoid (List.₀ X)
-
-  ListMonoid : IsMonoid (List.₀ X)
-  ListMonoid .μ = ++.η X
-  ListMonoid .η = ⊤⇒[].η X
-  ListMonoid .assoc {(x , y) , z} = ListX.reflexive (++-assoc x y z)
-  ListMonoid .identityˡ {_ , x} = ListX.reflexive (++-identityˡ x)
-  ListMonoid .identityʳ {x , _} = ListX.reflexive (≡.sym (++-identityʳ x))
-
-FreeMonoid₀ : (X : Setoid c ℓ) → Monoid
-FreeMonoid₀ X = record { isMonoid = ListMonoid X }
-
-FreeMonoid₁
-    : {A B : Setoid c ℓ}
-      (f : A ⟶ₛ B)
-    → Monoid⇒ (FreeMonoid₀ A) (FreeMonoid₀ B)
-FreeMonoid₁ f = record
-    { arr = List.₁ f
-    ; preserves-μ = λ {x,y} → ++.sym-commute f {x,y}
-    ; preserves-η = ⊤⇒[].commute f
-    }
-
-FreeMonoid : Functor (Setoids c ℓ) (Monoids Setoids-×.monoidal)
-FreeMonoid .F₀ = FreeMonoid₀
-FreeMonoid .F₁ = FreeMonoid₁
-FreeMonoid .identity {X} = List.identity {X}
-FreeMonoid .homomorphism {X} {Y} {Z} {f} {g} = List.homomorphism {X} {Y} {Z} {f} {g}
-FreeMonoid .F-resp-≈ {A} {B} {f} {g} = List.F-resp-≈ {A} {B} {f} {g}
diff --git a/Functor/Instance/List.agda b/Functor/Instance/List.agda
index ceb73e1..a280218 100644
--- a/Functor/Instance/List.agda
+++ b/Functor/Instance/List.agda
@@ -18,7 +18,7 @@ open Functor
 open Setoid using (reflexive)
 open Func
 
-open import Data.Opaque.List as List hiding (List)
+open import Data.Opaque.List as L hiding (List)
 
 private
   variable
@@ -29,7 +29,7 @@ open import Function.Construct.Setoid using (_∙_)
 
 opaque
 
-  unfolding List.List
+  unfolding L.List
 
   map-id
       : (xs : ∣ Listₛ A ∣)
@@ -58,8 +58,10 @@ opaque
 -- which applies the same function to every element of a list
 
 List : Functor (Setoids c ℓ) (Setoids c (c ⊔ ℓ))
-List .F₀ = List.Listₛ
-List .F₁ = List.mapₛ
+List .F₀ = Listₛ
+List .F₁ = mapₛ
 List .identity {_} {xs} = map-id xs
 List .homomorphism {f = f} {g} {xs} = List-homo f g xs
 List .F-resp-≈ {f = f} {g} f≈g = List-resp-≈ f g f≈g
+
+module List = Functor List