diff options
| -rw-r--r-- | Adjoint/Instance/List.agda | 87 | ||||
| -rw-r--r-- | Data/Monoid.agda | 66 | ||||
| -rw-r--r-- | Data/Opaque/List.agda | 110 | ||||
| -rw-r--r-- | Functor/Forgetful/Instance/Monoid.agda | 27 | ||||
| -rw-r--r-- | Functor/Free/Instance/Monoid.agda | 85 | ||||
| -rw-r--r-- | Functor/Instance/FreeMonoid.agda | 64 | ||||
| -rw-r--r-- | Functor/Instance/List.agda | 10 | ||||
| -rw-r--r-- | NaturalTransformation/Instance/EmptyList.agda | 32 | ||||
| -rw-r--r-- | NaturalTransformation/Instance/ListAppend.agda | 33 |
9 files changed, 415 insertions, 99 deletions
diff --git a/Adjoint/Instance/List.agda b/Adjoint/Instance/List.agda new file mode 100644 index 0000000..f517f16 --- /dev/null +++ b/Adjoint/Instance/List.agda @@ -0,0 +1,87 @@ +{-# OPTIONS --without-K --safe #-} + +open import Level using (Level; _⊔_; suc; 0ℓ) + +module Adjoint.Instance.List {c ℓ : Level} where + +import Data.List as L +import Data.List.Relation.Binary.Pointwise as PW + +open import Categories.Category.Monoidal.Bundle using (MonoidalCategory; SymmetricMonoidalCategory) +open import Category.Instance.Setoids.SymmetricMonoidal using (Setoids-×) + +module S = SymmetricMonoidalCategory (Setoids-× {c ⊔ ℓ} {c ⊔ ℓ}) + +open import Categories.Adjoint using (_⊣_) +open import Categories.Category.Construction.Monoids using (Monoids) +open import Categories.Functor using (Functor; id; _∘F_) +open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper) +open import Categories.Object.Monoid S.monoidal using (Monoid; Monoid⇒) +open import Data.Monoid using (toMonoid; toMonoid⇒) +open import Data.Opaque.List using ([-]ₛ; Listₛ; mapₛ; foldₛ; ++ₛ; ++ₛ-homo; []ₛ-homo; fold-mapₛ; fold) +open import Data.Product using (_,_; uncurry) +open import Data.Setoid using (∣_∣) +open import Function using (_⟶ₛ_; _⟨$⟩_) +open import Functor.Forgetful.Instance.Monoid {suc (c ⊔ ℓ)} {c ⊔ ℓ} {c ⊔ ℓ} using (Forget) +open import Functor.Free.Instance.Monoid {c ⊔ ℓ} {c ⊔ ℓ} using (Free; Listₘ) +open import Relation.Binary using (Setoid) + +open Monoid +open Monoid⇒ + +S-mc : MonoidalCategory (suc (c ⊔ ℓ)) (c ⊔ ℓ) (c ⊔ ℓ) +S-mc = record { monoidal = S.monoidal } + +opaque + + unfolding [-]ₛ + unfolding fold + + map-[-]ₛ + : {X Y : Setoid (c ⊔ ℓ) (c ⊔ ℓ)} + → (f : X ⟶ₛ Y) + → (open Setoid (Listₛ Y)) + → {x : ∣ X ∣} + → [-]ₛ ⟨$⟩ (f ⟨$⟩ x) + ≈ mapₛ f ⟨$⟩ ([-]ₛ ⟨$⟩ x) + map-[-]ₛ {X} {Y} f {x} = Setoid.refl (Listₛ Y) + + zig + : (Aₛ : Setoid (c ⊔ ℓ) (c ⊔ ℓ)) + {xs : ∣ Listₛ Aₛ ∣} + → (open Setoid (Listₛ Aₛ)) + → foldₛ (toMonoid (Listₘ Aₛ)) ⟨$⟩ (mapₛ [-]ₛ ⟨$⟩ xs) ≈ xs + zig Aₛ {xs = L.[]} = Setoid.refl (Listₛ Aₛ) + zig Aₛ {xs = x L.∷ xs} = Setoid.refl Aₛ PW.∷ zig Aₛ {xs = xs} + + zag + : (M : Monoid) + {x : ∣ Carrier M ∣} + → (open Setoid (Carrier M)) + → fold (toMonoid M) ([-]ₛ ⟨$⟩ x) ≈ x + zag M {x} = Setoid.sym (Carrier M) (identityʳ M {x , _}) + +unit : NaturalTransformation id (Forget S-mc ∘F Free) +unit = ntHelper record + { η = λ X → [-]ₛ {c ⊔ ℓ} {c ⊔ ℓ} {X} + ; commute = map-[-]ₛ + } + +foldₘ : (X : Monoid) → Monoid⇒ (Listₘ (Carrier X)) X +foldₘ X .arr = foldₛ (toMonoid X) +foldₘ X .preserves-μ {xs , ys} = ++ₛ-homo (toMonoid X) xs ys +foldₘ X .preserves-η {_} = []ₛ-homo (toMonoid X) + +counit : NaturalTransformation (Free ∘F Forget S-mc) id +counit = ntHelper record + { η = foldₘ + ; commute = λ {X} {Y} f → uncurry (fold-mapₛ (toMonoid X) (toMonoid Y)) (toMonoid⇒ X Y f) + } + +List⊣ : Free ⊣ Forget S-mc +List⊣ = record + { unit = unit + ; counit = counit + ; zig = λ {X} → zig X + ; zag = λ {M} → zag M + } diff --git a/Data/Monoid.agda b/Data/Monoid.agda new file mode 100644 index 0000000..ae2ded9 --- /dev/null +++ b/Data/Monoid.agda @@ -0,0 +1,66 @@ +{-# OPTIONS --without-K --safe #-} + +open import Level using (Level) +module Data.Monoid {c ℓ : Level} where + +open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory) +open import Category.Instance.Setoids.SymmetricMonoidal {c} {ℓ} using (Setoids-×) +open import Categories.Object.Monoid using (Monoid; Monoid⇒) + +module Setoids-× = SymmetricMonoidalCategory Setoids-× + +import Algebra.Bundles as Alg + +open import Data.Setoid using (∣_∣) +open import Relation.Binary using (Setoid) +open import Function using (Func) +open import Data.Product using (curry′; _,_) +open Func + +-- A monoid object in the (monoidal) category of setoids is just a monoid + +toMonoid : Monoid Setoids-×.monoidal → Alg.Monoid c ℓ +toMonoid M = record + { Carrier = Carrier + ; _≈_ = _≈_ + ; _∙_ = curry′ (to μ) + ; ε = to η _ + ; isMonoid = record + { isSemigroup = record + { isMagma = record + { isEquivalence = isEquivalence + ; ∙-cong = curry′ (cong μ) + } + ; assoc = λ x y z → assoc {(x , y) , z} + } + ; identity = (λ x → sym (identityˡ {_ , x}) ) , λ x → sym (identityʳ {x , _}) + } + } + where + open Monoid M renaming (Carrier to A) + open Setoid A + +-- A morphism of monoids in the (monoidal) category of setoids is a monoid homomorphism + +module _ (M N : Monoid Setoids-×.monoidal) where + + module M = Alg.Monoid (toMonoid M) + module N = Alg.Monoid (toMonoid N) + + open import Data.Product using (Σ; _,_) + open import Function using (_⟶ₛ_; _⟨$⟩_) + open import Algebra.Morphism using (IsMonoidHomomorphism) + open Monoid⇒ + toMonoid⇒ + : Monoid⇒ Setoids-×.monoidal M N + → Σ (M.setoid ⟶ₛ N.setoid) (λ f + → IsMonoidHomomorphism M.rawMonoid N.rawMonoid (to f)) + toMonoid⇒ f = arr f , record + { isMagmaHomomorphism = record + { isRelHomomorphism = record + { cong = cong (arr f) + } + ; homo = λ x y → preserves-μ f {x , y} + } + ; ε-homo = preserves-η f + } diff --git a/Data/Opaque/List.agda b/Data/Opaque/List.agda index a8e536f..83a2fe3 100644 --- a/Data/Opaque/List.agda +++ b/Data/Opaque/List.agda @@ -4,13 +4,19 @@ module Data.Opaque.List where import Data.List as L import Function.Construct.Constant as Const +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning -open import Level using (Level; _⊔_) +open import Algebra.Bundles using (Monoid) +open import Algebra.Morphism using (IsMonoidHomomorphism) +open import Data.List.Effectful.Foldable using (foldable; ++-homo) open import Data.List.Relation.Binary.Pointwise as PW using (++⁺; map⁺) -open import Data.Product using (uncurry′) +open import Data.Product using (_,_; curry′; uncurry′) open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_) +open import Data.Setoid using (∣_∣) open import Data.Unit.Polymorphic using (⊤) -open import Function using (_⟶ₛ_; Func) +open import Effect.Foldable using (RawFoldable) +open import Function using (_⟶ₛ_; Func; _⟨$⟩_; id) +open import Level using (Level; _⊔_) open import Relation.Binary using (Setoid) open Func @@ -52,10 +58,108 @@ opaque ∷ₛ .to = uncurry′ _∷_ ∷ₛ .cong = uncurry′ PW._∷_ + [-]ₛ : Aₛ ⟶ₛ Listₛ Aₛ + [-]ₛ .to = L.[_] + [-]ₛ .cong y = y PW.∷ PW.[] + mapₛ : (Aₛ ⟶ₛ Bₛ) → Listₛ Aₛ ⟶ₛ Listₛ Bₛ mapₛ f .to = map (to f) mapₛ f .cong xs≈ys = map⁺ (to f) (to f) (PW.map (cong f) xs≈ys) + cartesianProduct : ∣ Listₛ Aₛ ∣ → ∣ Listₛ Bₛ ∣ → ∣ Listₛ (Aₛ ×ₛ Bₛ) ∣ + cartesianProduct = L.cartesianProduct + + cartesian-product-cong + : {xs xs′ : ∣ Listₛ Aₛ ∣} + {ys ys′ : ∣ Listₛ Bₛ ∣} + → (let open Setoid (Listₛ Aₛ) in xs ≈ xs′) + → (let open Setoid (Listₛ Bₛ) in ys ≈ ys′) + → (let open Setoid (Listₛ (Aₛ ×ₛ Bₛ)) in cartesianProduct xs ys ≈ cartesianProduct xs′ ys′) + cartesian-product-cong PW.[] ys≋ys′ = PW.[] + cartesian-product-cong {Aₛ = Aₛ} {Bₛ = Bₛ} {xs = x₀ L.∷ xs} {xs′ = x₀′ L.∷ xs′} (x₀≈x₀′ PW.∷ xs≋xs′) ys≋ys′ = + ++⁺ + (map⁺ (x₀ ,_) (x₀′ ,_) (PW.map (x₀≈x₀′ ,_) ys≋ys′)) + (cartesian-product-cong {Aₛ = Aₛ} {Bₛ = Bₛ} xs≋xs′ ys≋ys′) + + pairsₛ : Listₛ Aₛ ×ₛ Listₛ Bₛ ⟶ₛ Listₛ (Aₛ ×ₛ Bₛ) + pairsₛ .to = uncurry′ L.cartesianProduct + pairsₛ {Aₛ = Aₛ} {Bₛ = Bₛ} .cong = uncurry′ (cartesian-product-cong {Aₛ = Aₛ} {Bₛ = Bₛ}) + ++ₛ : Listₛ Aₛ ×ₛ Listₛ Aₛ ⟶ₛ Listₛ Aₛ ++ₛ .to = uncurry′ _++_ ++ₛ .cong = uncurry′ ++⁺ + + foldr : (Aₛ ×ₛ Bₛ ⟶ₛ Bₛ) → ∣ Bₛ ∣ → ∣ Listₛ Aₛ ∣ → ∣ Bₛ ∣ + foldr f = L.foldr (curry′ (to f)) + + foldr-cong + : (f : Aₛ ×ₛ Bₛ ⟶ₛ Bₛ) + → (e : ∣ Bₛ ∣) + → (let module [A]ₛ = Setoid (Listₛ Aₛ)) + → {xs ys : ∣ Listₛ Aₛ ∣} + → (xs [A]ₛ.≈ ys) + → (open Setoid Bₛ) + → foldr f e xs ≈ foldr f e ys + foldr-cong {Bₛ = Bₛ} f e PW.[] = Setoid.refl Bₛ + foldr-cong f e (x≈y PW.∷ xs≋ys) = cong f (x≈y , foldr-cong f e xs≋ys) + + foldrₛ : (Aₛ ×ₛ Bₛ ⟶ₛ Bₛ) → ∣ Bₛ ∣ → Listₛ Aₛ ⟶ₛ Bₛ + foldrₛ f e .to = foldr f e + foldrₛ {Bₛ = Bₛ} f e .cong = foldr-cong f e + +module _ (M : Monoid c ℓ) where + + open Monoid M renaming (setoid to Mₛ) + + opaque + unfolding List + fold : ∣ Listₛ Mₛ ∣ → ∣ Mₛ ∣ + fold = RawFoldable.fold foldable rawMonoid + + fold-cong + : {xs ys : ∣ Listₛ Mₛ ∣} + → (let module [M]ₛ = Setoid (Listₛ Mₛ)) + → (xs [M]ₛ.≈ ys) + → fold xs ≈ fold ys + fold-cong = PW.rec (λ {xs} {ys} _ → fold xs ≈ fold ys) ∙-cong refl + + foldₛ : Listₛ Mₛ ⟶ₛ Mₛ + foldₛ .to = fold + foldₛ .cong = fold-cong + + opaque + unfolding fold + ++ₛ-homo + : (xs ys : ∣ Listₛ Mₛ ∣) + → foldₛ ⟨$⟩ (++ₛ ⟨$⟩ (xs , ys)) ≈ (foldₛ ⟨$⟩ xs) ∙ (foldₛ ⟨$⟩ ys) + ++ₛ-homo xs ys = ++-homo M id xs + + []ₛ-homo : foldₛ ⟨$⟩ ([]ₛ ⟨$⟩ _) ≈ ε + []ₛ-homo = refl + +module _ (M N : Monoid c ℓ) where + + module M = Monoid M + module N = Monoid N + + open IsMonoidHomomorphism + + opaque + unfolding fold + + fold-mapₛ + : (f : M.setoid ⟶ₛ N.setoid) + → IsMonoidHomomorphism M.rawMonoid N.rawMonoid (to f) + → {xs : ∣ Listₛ M.setoid ∣} + → foldₛ N ⟨$⟩ (mapₛ f ⟨$⟩ xs) N.≈ f ⟨$⟩ (foldₛ M ⟨$⟩ xs) + fold-mapₛ f isMH {L.[]} = N.sym (ε-homo isMH) + fold-mapₛ f isMH {x L.∷ xs} = begin + f′ x ∙ fold N (map f′ xs) ≈⟨ N.∙-cong N.refl (fold-mapₛ f isMH {xs}) ⟩ + f′ x ∙ f′ (fold M xs) ≈⟨ homo isMH x (fold M xs) ⟨ + f′ (x ∘ fold M xs) ∎ + where + open N using (_∙_) + open M using () renaming (_∙_ to _∘_) + open ≈-Reasoning N.setoid + f′ : M.Carrier → N.Carrier + f′ = to f diff --git a/Functor/Forgetful/Instance/Monoid.agda b/Functor/Forgetful/Instance/Monoid.agda new file mode 100644 index 0000000..2c786ef --- /dev/null +++ b/Functor/Forgetful/Instance/Monoid.agda @@ -0,0 +1,27 @@ +{-# OPTIONS --without-K --safe #-} + +open import Categories.Category.Monoidal using (MonoidalCategory) +open import Level using (Level) + +module Functor.Forgetful.Instance.Monoid {o ℓ e : Level} (S : MonoidalCategory o ℓ e) where + +open import Categories.Category.Construction.Monoids using (Monoids) +open import Categories.Functor using (Functor) +open import Categories.Object.Monoid using (Monoid; Monoid⇒) +open import Function using (id) + +module S = MonoidalCategory S + +open Monoid +open Monoid⇒ +open S.Equiv using (refl) +open Functor + +Forget : Functor (Monoids S.monoidal) S.U +Forget .F₀ = Carrier +Forget .F₁ = arr +Forget .identity = refl +Forget .homomorphism = refl +Forget .F-resp-≈ = id + +module Forget = Functor Forget diff --git a/Functor/Free/Instance/Monoid.agda b/Functor/Free/Instance/Monoid.agda new file mode 100644 index 0000000..34fa2dd --- /dev/null +++ b/Functor/Free/Instance/Monoid.agda @@ -0,0 +1,85 @@ +{-# OPTIONS --without-K --safe #-} + +open import Level using (Level; _⊔_) + +module Functor.Free.Instance.Monoid {c ℓ : Level} where + +import Categories.Object.Monoid as MonoidObject + +open import Categories.Category.Construction.Monoids using (Monoids) +open import Categories.Category.Instance.Setoids using (Setoids) +open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory) +open import Categories.Functor using (Functor) +open import Categories.NaturalTransformation using (NaturalTransformation) +open import Category.Instance.Setoids.SymmetricMonoidal {c} {c ⊔ ℓ} using (Setoids-×) +open import Data.List.Properties using (++-assoc; ++-identityˡ; ++-identityʳ) +open import Data.Opaque.List using ([]ₛ; Listₛ; ++ₛ; mapₛ) +open import Data.Product using (_,_) +open import Data.Setoid using (∣_∣) +open import Function using (_⟶ₛ_; _⟨$⟩_) +open import Functor.Instance.List {c} {ℓ} using (List) +open import NaturalTransformation.Instance.EmptyList {c} {ℓ} using (⊤⇒[]) +open import NaturalTransformation.Instance.ListAppend {c} {ℓ} using (++) +open import Relation.Binary using (Setoid) +open import Relation.Binary.PropositionalEquality as ≡ using (_≡_) + +module Setoids-× = SymmetricMonoidalCategory Setoids-× +module ++ = NaturalTransformation ++ +module ⊤⇒[] = NaturalTransformation ⊤⇒[] + +open Functor +open MonoidObject Setoids-×.monoidal using (Monoid; IsMonoid; Monoid⇒) +open IsMonoid + +-- the functor sending a setoid A to the monoid List A + +module _ (X : Setoid c ℓ) where + + open Setoid (List.₀ X) + + opaque + + unfolding []ₛ + + ++ₛ-assoc + : (x y z : ∣ Listₛ X ∣) + → ++ₛ ⟨$⟩ (++ₛ ⟨$⟩ (x , y) , z) + ≈ ++ₛ ⟨$⟩ (x , ++ₛ ⟨$⟩ (y , z)) + ++ₛ-assoc x y z = reflexive (++-assoc x y z) + + ++ₛ-identityˡ + : (x : ∣ Listₛ X ∣) + → x ≈ ++ₛ ⟨$⟩ ([]ₛ ⟨$⟩ _ , x) + ++ₛ-identityˡ x = reflexive (++-identityˡ x) + + ++ₛ-identityʳ + : (x : ∣ Listₛ X ∣) + → x ≈ ++ₛ ⟨$⟩ (x , []ₛ ⟨$⟩ _) + ++ₛ-identityʳ x = sym (reflexive (++-identityʳ x)) + + ListMonoid : IsMonoid (List.₀ X) + ListMonoid .μ = ++.η X + ListMonoid .η = ⊤⇒[].η X + ListMonoid .assoc {(x , y) , z} = ++ₛ-assoc x y z + ListMonoid .identityˡ {bro , x} = ++ₛ-identityˡ x + ListMonoid .identityʳ {x , _} = ++ₛ-identityʳ x + +Listₘ : Setoid c ℓ → Monoid +Listₘ X = record { isMonoid = ListMonoid X } + +mapₘ + : {Aₛ Bₛ : Setoid c ℓ} + (f : Aₛ ⟶ₛ Bₛ) + → Monoid⇒ (Listₘ Aₛ) (Listₘ Bₛ) +mapₘ f = record + { arr = List.₁ f + ; preserves-μ = λ {x,y} → ++.sym-commute f {x,y} + ; preserves-η = ⊤⇒[].sym-commute f + } + +Free : Functor (Setoids c ℓ) (Monoids Setoids-×.monoidal) +Free .F₀ = Listₘ +Free .F₁ = mapₘ +Free .identity {X} = List.identity {X} +Free .homomorphism {X} {Y} {Z} {f} {g} = List.homomorphism {X} {Y} {Z} {f} {g} +Free .F-resp-≈ {A} {B} {f} {g} = List.F-resp-≈ {A} {B} {f} {g} diff --git a/Functor/Instance/FreeMonoid.agda b/Functor/Instance/FreeMonoid.agda deleted file mode 100644 index bb26fd4..0000000 --- a/Functor/Instance/FreeMonoid.agda +++ /dev/null @@ -1,64 +0,0 @@ -{-# OPTIONS --without-K --safe #-} - -open import Level using (Level; _⊔_) - -module Functor.Instance.FreeMonoid {c ℓ : Level} where - -import Categories.Object.Monoid as MonoidObject - -open import Categories.Category.Construction.Monoids using (Monoids) -open import Categories.Category.Instance.Setoids using (Setoids) -open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory) -open import Categories.Functor using (Functor) -open import Categories.NaturalTransformation using (NaturalTransformation) -open import Category.Instance.Setoids.SymmetricMonoidal {c} {c ⊔ ℓ} using (Setoids-×) -open import Data.List.Properties using (++-assoc; ++-identityˡ; ++-identityʳ) -open import Data.Product using (_,_) -open import Function using (_⟶ₛ_) -open import Functor.Instance.List {c} {ℓ} using (List) -open import NaturalTransformation.Instance.EmptyList {c} {ℓ} using (⊤⇒[]) -open import NaturalTransformation.Instance.ListAppend {c} {ℓ} using (++) -open import Relation.Binary using (Setoid) -open import Relation.Binary.PropositionalEquality as ≡ using (_≡_) - -module List = Functor List -module Setoids-× = SymmetricMonoidalCategory Setoids-× -module ++ = NaturalTransformation ++ -module ⊤⇒[] = NaturalTransformation ⊤⇒[] - -open Functor -open MonoidObject Setoids-×.monoidal using (Monoid; IsMonoid; Monoid⇒) -open IsMonoid - -module _ (X : Setoid c ℓ) where - - private - module X = Setoid X - module ListX = Setoid (List.₀ X) - - ListMonoid : IsMonoid (List.₀ X) - ListMonoid .μ = ++.η X - ListMonoid .η = ⊤⇒[].η X - ListMonoid .assoc {(x , y) , z} = ListX.reflexive (++-assoc x y z) - ListMonoid .identityˡ {_ , x} = ListX.reflexive (++-identityˡ x) - ListMonoid .identityʳ {x , _} = ListX.reflexive (≡.sym (++-identityʳ x)) - -FreeMonoid₀ : (X : Setoid c ℓ) → Monoid -FreeMonoid₀ X = record { isMonoid = ListMonoid X } - -FreeMonoid₁ - : {A B : Setoid c ℓ} - (f : A ⟶ₛ B) - → Monoid⇒ (FreeMonoid₀ A) (FreeMonoid₀ B) -FreeMonoid₁ f = record - { arr = List.₁ f - ; preserves-μ = λ {x,y} → ++.sym-commute f {x,y} - ; preserves-η = ⊤⇒[].commute f - } - -FreeMonoid : Functor (Setoids c ℓ) (Monoids Setoids-×.monoidal) -FreeMonoid .F₀ = FreeMonoid₀ -FreeMonoid .F₁ = FreeMonoid₁ -FreeMonoid .identity {X} = List.identity {X} -FreeMonoid .homomorphism {X} {Y} {Z} {f} {g} = List.homomorphism {X} {Y} {Z} {f} {g} -FreeMonoid .F-resp-≈ {A} {B} {f} {g} = List.F-resp-≈ {A} {B} {f} {g} diff --git a/Functor/Instance/List.agda b/Functor/Instance/List.agda index ceb73e1..a280218 100644 --- a/Functor/Instance/List.agda +++ b/Functor/Instance/List.agda @@ -18,7 +18,7 @@ open Functor open Setoid using (reflexive) open Func -open import Data.Opaque.List as List hiding (List) +open import Data.Opaque.List as L hiding (List) private variable @@ -29,7 +29,7 @@ open import Function.Construct.Setoid using (_∙_) opaque - unfolding List.List + unfolding L.List map-id : (xs : ∣ Listₛ A ∣) @@ -58,8 +58,10 @@ opaque -- which applies the same function to every element of a list List : Functor (Setoids c ℓ) (Setoids c (c ⊔ ℓ)) -List .F₀ = List.Listₛ -List .F₁ = List.mapₛ +List .F₀ = Listₛ +List .F₁ = mapₛ List .identity {_} {xs} = map-id xs List .homomorphism {f = f} {g} {xs} = List-homo f g xs List .F-resp-≈ {f = f} {g} f≈g = List-resp-≈ f g f≈g + +module List = Functor List 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 } } |