5 files changed, 267 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 }
+    }
diff --git a/NaturalTransformation/Monoidal/Construction/MonoidValued.agda b/NaturalTransformation/Monoidal/Construction/MonoidValued.agda
new file mode 100644
index 0000000..2ef70d4
--- /dev/null
+++ b/NaturalTransformation/Monoidal/Construction/MonoidValued.agda
@@ -0,0 +1,110 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Categories.Category using (Category)
+open import Categories.Category.Cocartesian using (Cocartesian)
+open import Categories.Category.Cocartesian.Bundle using (CocartesianCategory)
+open import Categories.Category.Construction.Monoids using (Monoids)
+open import Categories.Category.Monoidal.Bundle using (MonoidalCategory)
+open import Categories.Functor using (Functor) renaming (_∘F_ to _∙_)
+open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper; _∘ˡ_)
+open import Level using (Level)
+
+-- A natural transformation between functors F, G
+-- from a cocartesian category 𝒞 to Monoids[S]
+-- can be turned into a monoidal natural transformation
+-- between monoidal functors F′ G′ from 𝒞 to S
+
+module NaturalTransformation.Monoidal.Construction.MonoidValued
+    {o o′ ℓ ℓ′ e e′ : Level}
+    {𝒞 : Category o ℓ e}
+    (𝒞-+ : Cocartesian 𝒞)
+    {S : MonoidalCategory o′ ℓ′ e′}
+    (let module S = MonoidalCategory S)
+    {M N : Functor 𝒞 (Monoids S.monoidal)}
+    (α : NaturalTransformation M N)
+  where
+
+import Categories.Category.Monoidal.Reasoning as ⊗-Reasoning
+import Categories.Morphism.Reasoning as ⇒-Reasoning
+import Categories.Object.Monoid as MonoidObject
+import Functor.Monoidal.Construction.MonoidValued 𝒞-+ {S = S} as FamilyOfMonoids
+
+open import Categories.Category using (module Definitions)
+open import Categories.Functor.Properties using ([_]-resp-square)
+open import Categories.NaturalTransformation.Monoidal using (module Lax)
+open import Data.Product using (_,_)
+open import Functor.Forgetful.Instance.Monoid S.monoidal using (Forget)
+
+private
+
+  module α = NaturalTransformation α
+  module M = Functor M
+  module N = Functor N
+  module 𝒞 = CocartesianCategory (record { cocartesian = 𝒞-+ })
+
+  open 𝒞 using (⊥; i₁; i₂; _+_)
+  open S
+
+  open MonoidObject monoidal using (Monoid; Monoid⇒)
+  open Definitions U using (CommutativeSquare)
+  open FamilyOfMonoids M using (F,⊗,ε)
+  open FamilyOfMonoids N using () renaming (F,⊗,ε to G,⊗,ε)
+  open Monoid using (μ; η)
+  open Monoid⇒
+  open ⇒-Reasoning U using (glue′)
+  open ⊗-Reasoning monoidal
+
+  F : Functor 𝒞 U
+  F = Forget ∙ M
+
+  G : Functor 𝒞 U
+  G = Forget ∙ N
+
+  β : NaturalTransformation F G
+  β = Forget ∘ˡ α
+
+  module F = Functor F
+  module G = Functor G
+  module β = NaturalTransformation β
+
+  module _ {A : 𝒞.Obj} where
+
+    εₘ : unit ⇒ F.₀ A
+    εₘ = η (M.₀ A)
+
+    ⊲ₘ : F.₀ A ⊗₀ F.₀ A ⇒ F.₀ A
+    ⊲ₘ = μ (M.₀ A)
+
+    εₙ : unit ⇒ G.₀ A
+    εₙ = η (N.₀ A)
+
+    ⊲ₙ : G.₀ A ⊗₀ G.₀ A ⇒ G.₀ A
+    ⊲ₙ = μ (N.₀ A)
+
+  ε-compat : β.η ⊥ ∘ εₘ ≈ εₙ
+  ε-compat = preserves-η (α.η ⊥)
+
+  module _ {n m : 𝒞.Obj} where
+
+    square : CommutativeSquare ⊲ₘ (β.η (n + m) ⊗₁ β.η (n + m)) (β.η (n + m)) ⊲ₙ
+    square = preserves-μ (α.η (n + m))
+
+    comm₁ : CommutativeSquare (F.₁ i₁) (β.η n) (β.η (n + m)) (G.₁ i₁)
+    comm₁ = β.commute i₁
+
+    comm₂ : CommutativeSquare (F.₁ i₂) (β.η m) (β.η (n + m)) (G.₁ i₂)
+    comm₂ = β.commute i₂
+
+    ⊗-homo-compat : CommutativeSquare (⊲ₘ ∘ F.₁ i₁ ⊗₁ F.₁ i₂) (β.η n ⊗₁ β.η m) (β.η (n + m)) (⊲ₙ ∘ G.₁ i₁ ⊗₁ G.₁ i₂)
+    ⊗-homo-compat = glue′ square (parallel comm₁ comm₂)
+
+open Lax.MonoidalNaturalTransformation hiding (ε-compat; ⊗-homo-compat)
+
+β,⊗,ε : Lax.MonoidalNaturalTransformation F,⊗,ε G,⊗,ε
+β,⊗,ε .U = β
+β,⊗,ε .isMonoidal = record
+    { ε-compat = ε-compat
+    ; ⊗-homo-compat = ⊗-homo-compat
+    }
+
+module β,⊗,ε = Lax.MonoidalNaturalTransformation β,⊗,ε