diff options
Diffstat (limited to 'Functor/Instance/List.agda')
| -rw-r--r-- | Functor/Instance/List.agda | 61 |
1 files changed, 34 insertions, 27 deletions
diff --git a/Functor/Instance/List.agda b/Functor/Instance/List.agda index b40670d..ceb73e1 100644 --- a/Functor/Instance/List.agda +++ b/Functor/Instance/List.agda @@ -4,13 +4,12 @@ open import Level using (Level; _⊔_) module Functor.Instance.List {c ℓ : Level} where -import Data.List as List import Data.List.Properties as ListProps import Data.List.Relation.Binary.Pointwise as PW open import Categories.Category.Instance.Setoids using (Setoids) open import Categories.Functor using (Functor) -open import Data.Setoid using (∣_∣) +open import Data.Setoid using (∣_∣; _⇒ₛ_) open import Function.Base using (_∘_; id) open import Function.Bundles using (Func; _⟶ₛ_; _⟨$⟩_) open import Relation.Binary using (Setoid) @@ -19,40 +18,48 @@ open Functor open Setoid using (reflexive) open Func +open import Data.Opaque.List as List hiding (List) + private variable A B C : Setoid c ℓ --- the List functor takes a carrier A to lists of A --- and the equivalence on A to pointwise equivalence on lists of A +open import Function.Construct.Identity using () renaming (function to Id) +open import Function.Construct.Setoid using (_∙_) -Listₛ : Setoid c ℓ → Setoid c (c ⊔ ℓ) -Listₛ = PW.setoid +opaque --- List on morphisms is the familiar map operation --- which applies the same function to every element of a list + unfolding List.List + + map-id + : (xs : ∣ Listₛ A ∣) + → (open Setoid (Listₛ A)) + → mapₛ (Id _) ⟨$⟩ xs ≈ xs + map-id {A} = reflexive (Listₛ A) ∘ ListProps.map-id -mapₛ : A ⟶ₛ B → Listₛ A ⟶ₛ Listₛ B -mapₛ f .to = List.map (to f) -mapₛ f .cong = PW.map⁺ (to f) (to f) ∘ PW.map (cong f) + List-homo + : (f : A ⟶ₛ B) + (g : B ⟶ₛ C) + → (xs : ∣ Listₛ A ∣) + → (open Setoid (Listₛ C)) + → mapₛ (g ∙ f) ⟨$⟩ xs ≈ mapₛ g ⟨$⟩ (mapₛ f ⟨$⟩ xs) + List-homo {C = C} f g = reflexive (Listₛ C) ∘ ListProps.map-∘ -map-id - : (xs : ∣ Listₛ A ∣) - → (open Setoid (Listₛ A)) - → List.map id xs ≈ xs -map-id {A} = reflexive (Listₛ A) ∘ ListProps.map-id + List-resp-≈ + : (f g : A ⟶ₛ B) + → (let open Setoid (A ⇒ₛ B) in f ≈ g) + → (let open Setoid (Listₛ A ⇒ₛ Listₛ B) in mapₛ f ≈ mapₛ g) + List-resp-≈ f g f≈g = PW.map⁺ (to f) (to g) (PW.refl f≈g) -List-homo - : (f : A ⟶ₛ B) - (g : B ⟶ₛ C) - → (xs : ∣ Listₛ A ∣) - → (open Setoid (Listₛ C)) - → List.map (to g ∘ to f) xs ≈ List.map (to g) (List.map (to f) xs) -List-homo {C = C} f g = reflexive (Listₛ C) ∘ ListProps.map-∘ +-- the List functor takes a carrier A to lists of A +-- and the equivalence on A to pointwise equivalence on lists of A + +-- List on morphisms is the familiar map operation +-- which applies the same function to every element of a list List : Functor (Setoids c ℓ) (Setoids c (c ⊔ ℓ)) -List .F₀ = Listₛ -List .F₁ = mapₛ -List .identity {A} {xs} = map-id {A} xs +List .F₀ = List.Listₛ +List .F₁ = List.mapₛ +List .identity {_} {xs} = map-id xs List .homomorphism {f = f} {g} {xs} = List-homo f g xs -List .F-resp-≈ {A} {B} {f} {g} f≈g = PW.map⁺ (to f) (to g) (PW.refl f≈g) +List .F-resp-≈ {f = f} {g} f≈g = List-resp-≈ f g f≈g |