From 716411e0c02f5900d7ef81d1ca08f8b83dc13351 Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Thu, 30 Oct 2025 14:03:53 -0500
Subject: Add empty list and append natural transformations

---
 NaturalTransformation/Instance/EmptyList.agda  | 23 +++++++++++++
 NaturalTransformation/Instance/ListAppend.agda | 45 ++++++++++++++++++++++++++
 2 files changed, 68 insertions(+)
 create mode 100644 NaturalTransformation/Instance/EmptyList.agda
 create mode 100644 NaturalTransformation/Instance/ListAppend.agda

(limited to 'NaturalTransformation/Instance')

diff --git a/NaturalTransformation/Instance/EmptyList.agda b/NaturalTransformation/Instance/EmptyList.agda
new file mode 100644
index 0000000..2164d6c
--- /dev/null
+++ b/NaturalTransformation/Instance/EmptyList.agda
@@ -0,0 +1,23 @@
+{-# OPTIONS --without-K --safe #-}
+
+module NaturalTransformation.Instance.EmptyList where
+
+import Function.Construct.Constant as Const
+
+open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper)
+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.Relation.Binary.Pointwise using (refl)
+open import Data.List using ([])
+open import Level using (0ℓ)
+open import Functor.Instance.List {0ℓ} {0ℓ} using (List)
+open import Relation.Binary using (Setoid)
+
+module List = Functor List
+
+⊤⇒[] : NaturalTransformation (const SingletonSetoid) List
+⊤⇒[] = ntHelper record
+    { η = λ X → Const.function SingletonSetoid (List.₀ X) []
+    ; commute = λ {_} {B} f → let module B = Setoid B in refl B.refl
+    }
diff --git a/NaturalTransformation/Instance/ListAppend.agda b/NaturalTransformation/Instance/ListAppend.agda
new file mode 100644
index 0000000..a2bf7b7
--- /dev/null
+++ b/NaturalTransformation/Instance/ListAppend.agda
@@ -0,0 +1,45 @@
+{-# OPTIONS --without-K --safe #-}
+
+module NaturalTransformation.Instance.ListAppend 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.List using (_++_)
+open import Data.List.Properties using (map-++)
+open import Data.List.Relation.Binary.Pointwise using (Pointwise; ++⁺; refl; reflexive; symmetric; ≡⇒Pointwise-≡)
+open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
+open import Data.Product using (_,_)
+open import Functor.Instance.List using (List)
+open import Function using (Func; _⟶ₛ_)
+open import Level using (0ℓ)
+open import Relation.Binary using (Setoid)
+
+module List = Functor (List {0ℓ} {0ℓ})
+
+open Cartesian (Setoids-Cartesian {0ℓ} {0ℓ}) using (products)
+open BinaryProducts products using (-×-)
+open Func
+
+++ₛ : {X : Setoid 0ℓ 0ℓ} → List.₀ X ×ₛ List.₀ X ⟶ₛ List.₀ X
+++ₛ .to (xs , ys) = xs ++ ys
+++ₛ .cong (≈xs , ≈ys)  = ++⁺ ≈xs ≈ys
+
+map-++ₛ
+  : {A B : Setoid 0ℓ 0ℓ}
+    (f : Func A B)
+    (xs ys : Data.List.List (Setoid.Carrier A))
+  → (open Setoid B)
+  → Pointwise _≈_ (Data.List.map (to f) xs ++ Data.List.map (to f) ys) (Data.List.map (to f) (xs ++ ys))
+map-++ₛ {_} {B} f xs ys = symmetric B.sym (reflexive B.reflexive (≡⇒Pointwise-≡ (map-++ (to f) xs ys)))
+    where
+      module B = Setoid B
+
+++ : NaturalTransformation (-×- ∘F (List ※ List)) List
+++ = ntHelper record
+    { η = λ X → ++ₛ {X}
+    ; commute = λ { {A} {B} f {xs , ys} → map-++ₛ f xs ys }
+    }
-- 
cgit v1.2.3