diff options
| -rw-r--r-- | NaturalTransformation/Instance/EmptyList.agda | 23 | ||||
| -rw-r--r-- | NaturalTransformation/Instance/ListAppend.agda | 45 |
2 files changed, 68 insertions, 0 deletions
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 } + } |