Add adjunction between free monoid and forget

9 files changed, 415 insertions, 99 deletions

diff --git a/Adjoint/Instance/List.agda b/Adjoint/Instance/List.agda
new file mode 100644
index 0000000..f517f16
--- /dev/null
+++ b/Adjoint/Instance/List.agda
@@ -0,0 +1,87 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Level using (Level; _⊔_; suc; 0ℓ)
+
+module Adjoint.Instance.List {c ℓ : Level} where
+
+import Data.List as L
+import Data.List.Relation.Binary.Pointwise as PW
+
+open import Categories.Category.Monoidal.Bundle using (MonoidalCategory; SymmetricMonoidalCategory)
+open import Category.Instance.Setoids.SymmetricMonoidal using (Setoids-×)
+
+module S = SymmetricMonoidalCategory (Setoids-× {c ⊔ ℓ} {c ⊔ ℓ})
+
+open import Categories.Adjoint using (_⊣_)
+open import Categories.Category.Construction.Monoids using (Monoids)
+open import Categories.Functor using (Functor; id; _∘F_)
+open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper)
+open import Categories.Object.Monoid S.monoidal using (Monoid; 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.Setoid using (∣_∣)
+open import Function using (_⟶ₛ_; _⟨$⟩_)
+open import Functor.Forgetful.Instance.Monoid {suc (c ⊔ ℓ)} {c ⊔ ℓ} {c ⊔ ℓ} using (Forget)
+open import Functor.Free.Instance.Monoid {c ⊔ ℓ} {c ⊔ ℓ} using (Free; Listₘ)
+open import Relation.Binary using (Setoid)
+
+open Monoid
+open Monoid⇒
+
+S-mc : MonoidalCategory (suc (c ⊔ ℓ)) (c ⊔ ℓ) (c ⊔ ℓ)
+S-mc = record { monoidal = S.monoidal }
+
+opaque
+
+  unfolding [-]ₛ
+  unfolding fold
+
+  map-[-]ₛ
+      : {X Y : Setoid (c ⊔ ℓ) (c ⊔ ℓ)}
+      → (f : X ⟶ₛ Y)
+      → (open Setoid (Listₛ Y))
+      → {x : ∣ X ∣}
+      → [-]ₛ ⟨$⟩ (f ⟨$⟩ x)
+      ≈ mapₛ f ⟨$⟩ ([-]ₛ ⟨$⟩ x)
+  map-[-]ₛ {X} {Y} f {x} = Setoid.refl (Listₛ Y)
+
+  zig
+      : (Aₛ  : Setoid (c ⊔ ℓ) (c ⊔ ℓ))
+        {xs : ∣ Listₛ Aₛ ∣}
+      → (open Setoid (Listₛ Aₛ))
+      → foldₛ (toMonoid (Listₘ Aₛ)) ⟨$⟩ (mapₛ [-]ₛ ⟨$⟩ xs) ≈ xs
+  zig Aₛ {xs = L.[]} = Setoid.refl (Listₛ Aₛ)
+  zig Aₛ {xs = x L.∷ xs} = Setoid.refl Aₛ PW.∷ zig Aₛ {xs = xs}
+
+  zag
+      : (M : Monoid)
+        {x : ∣ Carrier M ∣}
+      → (open Setoid (Carrier M))
+      → fold (toMonoid M) ([-]ₛ ⟨$⟩ x) ≈ x
+  zag M {x} = Setoid.sym (Carrier M) (identityʳ M {x , _})
+
+unit : NaturalTransformation id (Forget S-mc ∘F Free)
+unit = ntHelper record
+    { η = λ X → [-]ₛ {c ⊔ ℓ} {c ⊔ ℓ} {X}
+    ; commute = map-[-]ₛ
+   }
+
+foldₘ : (X : Monoid) → Monoid⇒ (Listₘ (Carrier X)) X
+foldₘ X .arr = foldₛ (toMonoid X)
+foldₘ X .preserves-μ {xs , ys} = ++ₛ-homo (toMonoid X) xs ys
+foldₘ X .preserves-η {_} = []ₛ-homo (toMonoid X)
+
+counit : NaturalTransformation (Free ∘F Forget S-mc) id
+counit = ntHelper record
+    { η = foldₘ
+    ; commute = λ {X} {Y} f → uncurry (fold-mapₛ (toMonoid X) (toMonoid Y)) (toMonoid⇒ X Y f)
+    }
+
+List⊣ : Free ⊣ Forget S-mc
+List⊣ = record
+    { unit = unit
+    ; counit = counit
+    ; zig = λ {X} → zig X
+    ; zag = λ {M} → zag M
+    }
diff --git a/Data/Monoid.agda b/Data/Monoid.agda
new file mode 100644
index 0000000..ae2ded9
--- /dev/null
+++ b/Data/Monoid.agda
@@ -0,0 +1,66 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Level using (Level)
+module Data.Monoid {c ℓ : Level} where
+
+open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory)
+open import Category.Instance.Setoids.SymmetricMonoidal {c} {ℓ} using (Setoids-×)
+open import Categories.Object.Monoid using (Monoid; Monoid⇒)
+
+module Setoids-× = SymmetricMonoidalCategory Setoids-×
+
+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′; _,_)
+open Func
+
+-- A monoid object in the (monoidal) category of setoids is just a monoid
+
+toMonoid : Monoid Setoids-×.monoidal → Alg.Monoid c ℓ
+toMonoid M = record
+    { Carrier = Carrier
+    ; _≈_ = _≈_
+    ; _∙_ = curry′ (to μ)
+    ; ε = to η _
+    ; isMonoid = record
+        { isSemigroup = record
+            { isMagma = record
+                { isEquivalence = isEquivalence
+                ; ∙-cong = curry′ (cong μ)
+                }
+            ; assoc = λ x y z → assoc {(x , y) , z}
+            }
+        ; identity = (λ x → sym (identityˡ {_ , x}) ) , λ x → sym (identityʳ {x , _})
+        }
+    }
+  where
+    open Monoid M renaming (Carrier to A)
+    open Setoid A
+
+-- A morphism of monoids in the (monoidal) category of setoids is a monoid homomorphism
+
+module  _ (M N : Monoid Setoids-×.monoidal) where
+
+  module M = Alg.Monoid (toMonoid M)
+  module N = Alg.Monoid (toMonoid N)
+
+  open import Data.Product using (Σ; _,_)
+  open import Function using (_⟶ₛ_; _⟨$⟩_)
+  open import Algebra.Morphism using (IsMonoidHomomorphism)
+  open Monoid⇒
+  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}
+          }
+      ; ε-homo = preserves-η f
+      }
diff --git a/Data/Opaque/List.agda b/Data/Opaque/List.agda
index a8e536f..83a2fe3 100644
--- a/Data/Opaque/List.agda
+++ b/Data/Opaque/List.agda
@@ -4,13 +4,19 @@ module Data.Opaque.List where
 
 import Data.List as L
 import Function.Construct.Constant as Const
+import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
 
-open import Level using (Level; _⊔_)
+open import Algebra.Bundles using (Monoid)
+open import Algebra.Morphism using (IsMonoidHomomorphism)
+open import Data.List.Effectful.Foldable using (foldable; ++-homo)
 open import Data.List.Relation.Binary.Pointwise as PW using (++⁺; map⁺)
-open import Data.Product using (uncurry′)
+open import Data.Product using (_,_; curry′; uncurry′)
 open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
+open import Data.Setoid using (∣_∣)
 open import Data.Unit.Polymorphic using (⊤)
-open import Function using (_⟶ₛ_; Func)
+open import Effect.Foldable using (RawFoldable)
+open import Function using (_⟶ₛ_; Func; _⟨$⟩_; id)
+open import Level using (Level; _⊔_)
 open import Relation.Binary using (Setoid)
 
 open Func
@@ -52,10 +58,108 @@ opaque
   ∷ₛ .to = uncurry′ _∷_
   ∷ₛ .cong = uncurry′ PW._∷_
 
+  [-]ₛ : Aₛ ⟶ₛ Listₛ Aₛ
+  [-]ₛ .to = L.[_]
+  [-]ₛ .cong y = y PW.∷ PW.[]
+
   mapₛ : (Aₛ ⟶ₛ Bₛ) → Listₛ Aₛ ⟶ₛ Listₛ Bₛ
   mapₛ f .to = map (to f)
   mapₛ f .cong xs≈ys = map⁺ (to f) (to f) (PW.map (cong f) xs≈ys)
 
+  cartesianProduct : ∣ Listₛ Aₛ ∣ → ∣ Listₛ Bₛ ∣ → ∣ Listₛ (Aₛ ×ₛ Bₛ) ∣
+  cartesianProduct = L.cartesianProduct
+
+  cartesian-product-cong
+    : {xs xs′ : ∣ Listₛ Aₛ ∣}
+      {ys ys′ : ∣ Listₛ Bₛ ∣}
+    → (let open Setoid (Listₛ Aₛ) in xs ≈ xs′)
+    → (let open Setoid (Listₛ Bₛ) in ys ≈ ys′)
+    → (let open Setoid (Listₛ (Aₛ ×ₛ Bₛ)) in cartesianProduct xs ys ≈ cartesianProduct xs′ ys′)
+  cartesian-product-cong PW.[] ys≋ys′ = PW.[]
+  cartesian-product-cong {Aₛ = Aₛ} {Bₛ = Bₛ} {xs = x₀ L.∷ xs} {xs′ = x₀′ L.∷ xs′} (x₀≈x₀′ PW.∷ xs≋xs′) ys≋ys′ =
+      ++⁺
+          (map⁺ (x₀ ,_) (x₀′ ,_) (PW.map (x₀≈x₀′ ,_) ys≋ys′))
+          (cartesian-product-cong {Aₛ = Aₛ} {Bₛ = Bₛ} xs≋xs′ ys≋ys′)
+
+  pairsₛ : Listₛ Aₛ ×ₛ Listₛ Bₛ ⟶ₛ Listₛ (Aₛ ×ₛ Bₛ)
+  pairsₛ .to = uncurry′ L.cartesianProduct
+  pairsₛ {Aₛ = Aₛ} {Bₛ = Bₛ} .cong = uncurry′ (cartesian-product-cong {Aₛ = Aₛ} {Bₛ = Bₛ})
+
   ++ₛ : Listₛ Aₛ ×ₛ Listₛ Aₛ ⟶ₛ Listₛ Aₛ
   ++ₛ .to = uncurry′ _++_
   ++ₛ .cong = uncurry′ ++⁺
+
+  foldr : (Aₛ ×ₛ Bₛ ⟶ₛ Bₛ) → ∣ Bₛ ∣ → ∣ Listₛ Aₛ ∣ → ∣ Bₛ ∣
+  foldr f = L.foldr (curry′ (to f))
+
+  foldr-cong
+      : (f : Aₛ ×ₛ Bₛ ⟶ₛ Bₛ)
+      → (e : ∣ Bₛ ∣)
+      → (let module [A]ₛ = Setoid (Listₛ Aₛ))
+      → {xs ys : ∣ Listₛ Aₛ ∣}
+      → (xs [A]ₛ.≈ ys)
+      → (open Setoid Bₛ)
+      → foldr f e xs ≈ foldr f e ys
+  foldr-cong {Bₛ = Bₛ} f e PW.[] = Setoid.refl Bₛ
+  foldr-cong f e (x≈y PW.∷ xs≋ys) = cong f (x≈y , foldr-cong f e xs≋ys)
+
+  foldrₛ : (Aₛ ×ₛ Bₛ ⟶ₛ Bₛ) → ∣ Bₛ ∣ → Listₛ Aₛ ⟶ₛ Bₛ
+  foldrₛ f e .to = foldr f e
+  foldrₛ {Bₛ = Bₛ} f e .cong = foldr-cong f e
+
+module _ (M : Monoid c ℓ) where
+
+  open Monoid M renaming (setoid to Mₛ)
+
+  opaque
+    unfolding List
+    fold : ∣ Listₛ Mₛ ∣ → ∣ Mₛ ∣
+    fold = RawFoldable.fold foldable rawMonoid
+
+    fold-cong
+        : {xs ys : ∣ Listₛ Mₛ ∣}
+        → (let module [M]ₛ = Setoid (Listₛ Mₛ))
+        → (xs [M]ₛ.≈ ys)
+        → fold xs ≈ fold ys
+    fold-cong = PW.rec (λ {xs} {ys} _ → fold xs ≈ fold ys) ∙-cong refl
+
+  foldₛ : Listₛ Mₛ ⟶ₛ Mₛ
+  foldₛ .to = fold
+  foldₛ .cong = fold-cong
+
+  opaque
+    unfolding fold
+    ++ₛ-homo
+        : (xs ys : ∣ Listₛ Mₛ ∣)
+        → foldₛ ⟨$⟩ (++ₛ ⟨$⟩ (xs , ys)) ≈ (foldₛ ⟨$⟩ xs) ∙ (foldₛ ⟨$⟩ ys)
+    ++ₛ-homo xs ys = ++-homo M id xs
+
+    []ₛ-homo : foldₛ ⟨$⟩ ([]ₛ ⟨$⟩ _) ≈ ε
+    []ₛ-homo = refl
+
+module _ (M N : Monoid c ℓ) where
+
+  module M = Monoid M
+  module N = Monoid N
+
+  open IsMonoidHomomorphism
+
+  opaque
+    unfolding fold
+
+    fold-mapₛ
+        : (f : M.setoid ⟶ₛ N.setoid)
+        → IsMonoidHomomorphism M.rawMonoid N.rawMonoid (to f)
+        → {xs : ∣ Listₛ M.setoid ∣}
+        → foldₛ N ⟨$⟩ (mapₛ f ⟨$⟩ xs) N.≈ f ⟨$⟩ (foldₛ M ⟨$⟩ xs)
+    fold-mapₛ f isMH {L.[]} = N.sym (ε-homo isMH)
+    fold-mapₛ f isMH {x L.∷ xs} = begin
+        f′ x ∙ fold N (map f′ xs) ≈⟨ N.∙-cong N.refl (fold-mapₛ f isMH {xs}) ⟩
+        f′ x ∙ f′ (fold M xs)     ≈⟨ homo isMH x (fold M xs) ⟨
+        f′ (x ∘ fold M xs)        ∎
+      where
+        open N using (_∙_)
+        open M using () renaming (_∙_ to _∘_)
+        open ≈-Reasoning N.setoid
+        f′ : M.Carrier → N.Carrier
+        f′ = to f
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
diff --git a/NaturalTransformation/Instance/EmptyList.agda b/NaturalTransformation/Instance/EmptyList.agda
index 9a558a2..0e069d2 100644
--- a/NaturalTransformation/Instance/EmptyList.agda
+++ b/NaturalTransformation/Instance/EmptyList.agda
@@ -1,23 +1,35 @@
 {-# OPTIONS --without-K --safe #-}
 
-open import Level using (Level)
+open import Level using (Level; _⊔_)
 
 module NaturalTransformation.Instance.EmptyList {c ℓ : Level} where
 
-import Function.Construct.Constant as Const
-
-open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper)
+open import Categories.Category.Instance.SingletonSet using () renaming (SingletonSetoid to ⊤ₛ)
 open import Categories.Functor using (Functor)
-open import Categories.Category.Instance.SingletonSet using (SingletonSetoid)
 open import Categories.Functor.Construction.Constant using (const)
-open import Data.List using ([])
+open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper)
+open import Data.Opaque.List using (Listₛ; []ₛ; mapₛ)
+open import Data.Setoid using (_⇒ₛ_)
+open import Function using (_⟶ₛ_)
+open import Function.Construct.Constant using () renaming (function to Const)
+open import Function.Construct.Setoid using (_∙_)
 open import Functor.Instance.List {c} {ℓ} using (List)
 open import Relation.Binary using (Setoid)
 
-module List = Functor List
+opaque
+
+  unfolding []ₛ
+
+  map-[]ₛ : {A B : Setoid c ℓ}
+      → (f : A ⟶ₛ B)
+      → (open Setoid (⊤ₛ ⇒ₛ Listₛ B))
+      → []ₛ ≈ mapₛ f ∙ []ₛ
+  map-[]ₛ {_} {B} f = refl
+    where
+      open Setoid (List.₀ B)
 
-⊤⇒[] : NaturalTransformation (const SingletonSetoid) List
+⊤⇒[] : NaturalTransformation (const ⊤ₛ) List
 ⊤⇒[] = ntHelper record
-    { η = λ X → Const.function SingletonSetoid (List.₀ X) []
-    ; commute = λ {_} {B} f → Setoid.refl (List.₀ B)
+    { η = λ X → []ₛ
+    ; commute = map-[]ₛ
     }
diff --git a/NaturalTransformation/Instance/ListAppend.agda b/NaturalTransformation/Instance/ListAppend.agda
index 05a31f5..3f198e1 100644
--- a/NaturalTransformation/Instance/ListAppend.agda
+++ b/NaturalTransformation/Instance/ListAppend.agda
@@ -10,37 +10,34 @@ open import Categories.Category.BinaryProducts using (module BinaryProducts)
 open import Categories.Category.Monoidal.Instance.Setoids using (Setoids-Cartesian)
 open import Categories.Category.Cartesian using (Cartesian)
 open import Categories.Functor using (Functor; _∘F_)
-open import Data.List using (_++_; map)
+open import Data.Opaque.List as L using (mapₛ; ++ₛ)
 open import Data.List.Properties using (map-++)
-open import Data.List.Relation.Binary.Pointwise using (++⁺)
 open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
 open import Data.Product using (_,_)
 open import Functor.Instance.List {c} {ℓ} using (List)
-open import Function using (Func; _⟶ₛ_)
+open import Function using (Func; _⟶ₛ_; _⟨$⟩_)
 open import Relation.Binary using (Setoid)
 
-module List = Functor List
-
 open Cartesian (Setoids-Cartesian {c} {c ⊔ ℓ}) using (products)
 open BinaryProducts products using (-×-)
 open Func
 
-++ₛ : {X : Setoid c ℓ} → List.₀ X ×ₛ List.₀ X ⟶ₛ List.₀ X
-++ₛ .to (xs , ys) = xs ++ ys
-++ₛ .cong (≈xs , ≈ys) = ++⁺ ≈xs ≈ys
+opaque
+
+  unfolding ++ₛ
 
-map-++ₛ
-  : {A B : Setoid c ℓ}
-    (f : Func A B)
-    (xs ys : Data.List.List (Setoid.Carrier A))
-  → (open Setoid (List.₀ B))
-  → map (to f) xs ++ map (to f) ys ≈ map (to f) (xs ++ ys)
-map-++ₛ {_} {B} f xs ys = ListB.sym (ListB.reflexive (map-++ (to f) xs ys))
-  where
-    module ListB = Setoid (List.₀ B)
+  map-++ₛ
+    : {A B : Setoid c ℓ}
+      (f : Func A B)
+      (xs ys : Setoid.Carrier (L.Listₛ A))
+      (open Setoid (L.Listₛ B))
+    → ++ₛ ⟨$⟩ (mapₛ f ⟨$⟩ xs , mapₛ f ⟨$⟩ ys) ≈ mapₛ f ⟨$⟩ (++ₛ ⟨$⟩ (xs , ys))
+  map-++ₛ {_} {B} f xs ys = sym (reflexive (map-++ (to f) xs ys))
+    where
+      open Setoid (List.₀ B)
 
 ++ : NaturalTransformation (-×- ∘F (List ※ List)) List
 ++ = ntHelper record
-    { η = λ X → ++ₛ {X}
+    { η = λ X → ++ₛ {c} {ℓ} {X}
     ; commute = λ { {A} {B} f {xs , ys} → map-++ₛ f xs ys }
     }