4 files changed, 157 insertions, 0 deletions
diff --git a/NaturalTransformation/Instance/EmptyList.agda b/NaturalTransformation/Instance/EmptyList.agda
new file mode 100644
index 0000000..9f94955
--- /dev/null
+++ b/NaturalTransformation/Instance/EmptyList.agda
@@ -0,0 +1,35 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Level using (Level; _⊔_)
+
+module NaturalTransformation.Instance.EmptyList {c ℓ : Level} where
+
+open import Categories.Functor using (Functor)
+open import Categories.Functor.Construction.Constant using (const)
+open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper)
+open import Data.Opaque.List using (Listₛ; []ₛ; mapₛ)
+open import Data.Setoid using (_⇒ₛ_)
+open import Data.Setoid.Unit 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)
+
+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 ⊤ₛ) List
+⊤⇒[] = ntHelper record
+    { η = λ X → []ₛ
+    ; commute = map-[]ₛ
+    }
diff --git a/NaturalTransformation/Instance/EmptyMultiset.agda b/NaturalTransformation/Instance/EmptyMultiset.agda
new file mode 100644
index 0000000..bfec451
--- /dev/null
+++ b/NaturalTransformation/Instance/EmptyMultiset.agda
@@ -0,0 +1,34 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Level using (Level; _⊔_)
+
+module NaturalTransformation.Instance.EmptyMultiset {c ℓ : Level} where
+
+import Function.Construct.Constant as Const
+
+open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper)
+open import Categories.Functor using (Functor)
+open import Data.Setoid.Unit {c} {c ⊔ ℓ} using (⊤ₛ)
+open import Categories.Functor.Construction.Constant using (const)
+open import Data.Opaque.Multiset using (Multisetₛ; []ₛ; mapₛ)
+open import Functor.Instance.Multiset {c} {ℓ} using (Multiset)
+open import Function.Construct.Constant using () renaming (function to Const)
+open import Relation.Binary using (Setoid)
+open import Data.Setoid using (_⇒ₛ_)
+open import Function using (Func; _⟶ₛ_)
+open import Function.Construct.Setoid using (_∙_)
+
+opaque
+  unfolding mapₛ
+  map-[]ₛ
+      : {A B : Setoid c ℓ}
+      → (f : A ⟶ₛ B)
+      → (open Setoid (⊤ₛ ⇒ₛ Multisetₛ B))
+      → []ₛ ≈ mapₛ f ∙ []ₛ
+  map-[]ₛ {B = B} f = Setoid.refl (Multisetₛ B)
+
+⊤⇒[] : NaturalTransformation (const ⊤ₛ) Multiset
+⊤⇒[] = ntHelper record
+    { η = λ X → []ₛ {Aₛ = X}
+    ; commute = map-[]ₛ
+    }
diff --git a/NaturalTransformation/Instance/ListAppend.agda b/NaturalTransformation/Instance/ListAppend.agda
new file mode 100644
index 0000000..3f198e1
--- /dev/null
+++ b/NaturalTransformation/Instance/ListAppend.agda
@@ -0,0 +1,43 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Level using (Level; _⊔_)
+
+module NaturalTransformation.Instance.ListAppend {c ℓ : Level} where
+
+open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper)
+open import Categories.Category.Product using (_※_)
+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.Opaque.List as L using (mapₛ; ++ₛ)
+open import Data.List.Properties using (map-++)
+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 Relation.Binary using (Setoid)
+
+open Cartesian (Setoids-Cartesian {c} {c ⊔ ℓ}) using (products)
+open BinaryProducts products using (-×-)
+open Func
+
+opaque
+
+  unfolding ++ₛ
+
+  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 → ++ₛ {c} {ℓ} {X}
+    ; commute = λ { {A} {B} f {xs , ys} → map-++ₛ f xs ys }
+    }
diff --git a/NaturalTransformation/Instance/MultisetAppend.agda b/NaturalTransformation/Instance/MultisetAppend.agda
new file mode 100644
index 0000000..f786124
--- /dev/null
+++ b/NaturalTransformation/Instance/MultisetAppend.agda
@@ -0,0 +1,45 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Level using (Level; _⊔_)
+
+module NaturalTransformation.Instance.MultisetAppend {c ℓ : Level} where
+
+import Data.Opaque.List as L
+
+open import Categories.Category.BinaryProducts using (module BinaryProducts)
+open import Categories.Category.Cartesian using (Cartesian)
+open import Categories.Category.Monoidal.Instance.Setoids using (Setoids-Cartesian)
+open import Categories.Category.Product using (_※_)
+open import Categories.Functor using (Functor; _∘F_)
+open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper)
+open import Data.List.Properties using (map-++)
+open import Data.List.Relation.Binary.Permutation.Setoid.Properties using (++⁺)
+open import Data.Opaque.Multiset using (Multisetₛ; mapₛ; ++ₛ)
+open import Data.Product using (_,_)
+open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
+open import Function using (Func; _⟶ₛ_; _⟨$⟩_)
+open import Functor.Instance.Multiset {c} {ℓ} using (Multiset)
+open import Relation.Binary using (Setoid)
+
+open Cartesian (Setoids-Cartesian {c} {c ⊔ ℓ}) using (products)
+open BinaryProducts products using (-×-)
+open Func
+
+opaque
+  unfolding ++ₛ mapₛ
+
+  map-++ₛ
+    : {A B : Setoid c ℓ}
+      (f : Func A B)
+      (xs ys : Setoid.Carrier (Multiset.₀ A))
+    → (open Setoid (Multiset.₀ B))
+    → ++ₛ ⟨$⟩ (mapₛ f ⟨$⟩ xs , mapₛ f ⟨$⟩ ys) ≈ mapₛ f ⟨$⟩ (++ₛ ⟨$⟩ (xs , ys))
+  map-++ₛ {A} {B} f xs ys = sym (reflexive (map-++ (to f) xs ys))
+    where
+      open Setoid (Multiset.₀ B)
+
+++ : NaturalTransformation (-×- ∘F (Multiset ※ Multiset)) Multiset
+++ = ntHelper record
+    { η = λ X → ++ₛ
+    ; commute = λ { {A} {B} f {xs , ys} → map-++ₛ f xs ys }
+    }