Add adjunction between free monoid and forget

2 files changed, 37 insertions, 28 deletions

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 }
     }