diff options
Diffstat (limited to 'Functor/Instance/Nat')
| -rw-r--r-- | Functor/Instance/Nat/Pull.agda | 72 | ||||
| -rw-r--r-- | Functor/Instance/Nat/Push.agda | 65 | ||||
| -rw-r--r-- | Functor/Instance/Nat/System.agda | 150 |
3 files changed, 167 insertions, 120 deletions
diff --git a/Functor/Instance/Nat/Pull.agda b/Functor/Instance/Nat/Pull.agda index 5b74399..b1764d9 100644 --- a/Functor/Instance/Nat/Pull.agda +++ b/Functor/Instance/Nat/Pull.agda @@ -14,50 +14,68 @@ open import Function.Construct.Setoid using (setoid; _∙_) open import Level using (0ℓ) open import Relation.Binary using (Rel; Setoid) open import Relation.Binary.PropositionalEquality as ≡ using (_≗_) -open import Data.Circuit.Value using (Value) -open import Data.System.Values Value using (Values) +open import Data.Circuit.Value using (Monoid) +open import Data.System.Values Monoid using (Values) +open import Data.Unit using (⊤; tt) open Functor open Func -_≈_ : {X Y : Setoid 0ℓ 0ℓ} → Rel (X ⟶ₛ Y) 0ℓ -_≈_ {X} {Y} = Setoid._≈_ (setoid X Y) -infixr 4 _≈_ +-- Pull takes a natural number n to the setoid Values n private + variable A B C : ℕ + _≈_ : {X Y : Setoid 0ℓ 0ℓ} → Rel (X ⟶ₛ Y) 0ℓ + _≈_ {X} {Y} = Setoid._≈_ (setoid X Y) + + infixr 4 _≈_ + + opaque + + unfolding Values + + -- action of Pull on morphisms (contravariant) + Pull₁ : (Fin A → Fin B) → Values B ⟶ₛ Values A + to (Pull₁ f) i = i ∘ f + cong (Pull₁ f) x≗y = x≗y ∘ f --- action on objects is Values n (Vector Value n) + -- Pull respects identity + Pull-identity : Pull₁ id ≈ Id (Values A) + Pull-identity {A} = Setoid.refl (Values A) --- action of Pull on morphisms (contravariant) -Pull₁ : (Fin A → Fin B) → Values B ⟶ₛ Values A -to (Pull₁ f) i = i ∘ f -cong (Pull₁ f) x≗y = x≗y ∘ f + opaque --- Pull respects identity -Pull-identity : Pull₁ id ≈ Id (Values A) -Pull-identity {A} = Setoid.refl (Values A) + unfolding Pull₁ --- Pull flips composition -Pull-homomorphism - : {A B C : ℕ} - (f : Fin A → Fin B) - (g : Fin B → Fin C) - → Pull₁ (g ∘ f) ≈ Pull₁ f ∙ Pull₁ g -Pull-homomorphism {A} _ _ = Setoid.refl (Values A) + -- Pull flips composition + Pull-homomorphism + : (f : Fin A → Fin B) + (g : Fin B → Fin C) + → Pull₁ (g ∘ f) ≈ Pull₁ f ∙ Pull₁ g + Pull-homomorphism {A} _ _ = Setoid.refl (Values A) --- Pull respects equality -Pull-resp-≈ - : {f g : Fin A → Fin B} - → f ≗ g - → Pull₁ f ≈ Pull₁ g -Pull-resp-≈ f≗g {v} = ≡.cong v ∘ f≗g + -- Pull respects equality + Pull-resp-≈ + : {f g : Fin A → Fin B} + → f ≗ g + → Pull₁ f ≈ Pull₁ g + Pull-resp-≈ f≗g {v} = ≡.cong v ∘ f≗g + +opaque + + unfolding Pull₁ + + Pull-defs : ⊤ + Pull-defs = tt -- the Pull functor Pull : Functor Natop (Setoids 0ℓ 0ℓ) F₀ Pull = Values F₁ Pull = Pull₁ identity Pull = Pull-identity -homomorphism Pull {f = f} {g} {v} = Pull-homomorphism g f {v} +homomorphism Pull {f = f} {g} = Pull-homomorphism g f F-resp-≈ Pull = Pull-resp-≈ + +module Pull = Functor Pull diff --git a/Functor/Instance/Nat/Push.agda b/Functor/Instance/Nat/Push.agda index 53d0bef..8126006 100644 --- a/Functor/Instance/Nat/Push.agda +++ b/Functor/Instance/Nat/Push.agda @@ -17,43 +17,56 @@ open import Function.Construct.Setoid using (setoid; _∙_) open import Level using (0ℓ) open import Relation.Binary using (Rel; Setoid) open import Relation.Binary.PropositionalEquality as ≡ using (_≗_) -open import Data.Circuit.Value using (Value) -open import Data.System.Values Value using (Values) +open import Data.Circuit.Value using (Monoid) +open import Data.System.Values Monoid using (Values) +open import Data.Unit using (⊤; tt) open Func open Functor +-- Push sends a natural number n to Values n + private + variable A B C : ℕ -_≈_ : {X Y : Setoid 0ℓ 0ℓ} → Rel (X ⟶ₛ Y) 0ℓ -_≈_ {X} {Y} = Setoid._≈_ (setoid X Y) -infixr 4 _≈_ + _≈_ : {X Y : Setoid 0ℓ 0ℓ} → Rel (X ⟶ₛ Y) 0ℓ + _≈_ {X} {Y} = Setoid._≈_ (setoid X Y) + infixr 4 _≈_ + + opaque + + unfolding Values --- action of Push on objects is Values n (Vector Value n) + -- action of Push on morphisms (covariant) + Push₁ : (Fin A → Fin B) → Values A ⟶ₛ Values B + to (Push₁ f) v = merge v ∘ preimage f ∘ ⁅_⁆ + cong (Push₁ f) x≗y = merge-cong₁ x≗y ∘ preimage f ∘ ⁅_⁆ --- action of Push on morphisms (covariant) -Push₁ : (Fin A → Fin B) → Values A ⟶ₛ Values B -to (Push₁ f) v = merge v ∘ preimage f ∘ ⁅_⁆ -cong (Push₁ f) x≗y = merge-cong₁ x≗y ∘ preimage f ∘ ⁅_⁆ + -- Push respects identity + Push-identity : Push₁ id ≈ Id (Values A) + Push-identity {_} {v} = merge-⁅⁆ v --- Push respects identity -Push-identity : Push₁ id ≈ Id (Values A) -Push-identity {_} {v} = merge-⁅⁆ v + -- Push respects composition + Push-homomorphism + : {f : Fin A → Fin B} + {g : Fin B → Fin C} + → Push₁ (g ∘ f) ≈ Push₁ g ∙ Push₁ f + Push-homomorphism {f = f} {g} {v} = merge-preimage f v ∘ preimage g ∘ ⁅_⁆ --- Push respects composition -Push-homomorphism - : {f : Fin A → Fin B} - {g : Fin B → Fin C} - → Push₁ (g ∘ f) ≈ Push₁ g ∙ Push₁ f -Push-homomorphism {f = f} {g} {v} = merge-preimage f v ∘ preimage g ∘ ⁅_⁆ + -- Push respects equality + Push-resp-≈ + : {f g : Fin A → Fin B} + → f ≗ g + → Push₁ f ≈ Push₁ g + Push-resp-≈ f≗g {v} = merge-cong₂ v ∘ preimage-cong₁ f≗g ∘ ⁅_⁆ --- Push respects equality -Push-resp-≈ - : {f g : Fin A → Fin B} - → f ≗ g - → Push₁ f ≈ Push₁ g -Push-resp-≈ f≗g {v} = merge-cong₂ v ∘ preimage-cong₁ f≗g ∘ ⁅_⁆ +opaque + + unfolding Push₁ + + Push-defs : ⊤ + Push-defs = tt -- the Push functor Push : Functor Nat (Setoids 0ℓ 0ℓ) @@ -62,3 +75,5 @@ F₁ Push = Push₁ identity Push = Push-identity homomorphism Push = Push-homomorphism F-resp-≈ Push = Push-resp-≈ + +module Push = Functor Push diff --git a/Functor/Instance/Nat/System.agda b/Functor/Instance/Nat/System.agda index 00451ad..05e1e7b 100644 --- a/Functor/Instance/Nat/System.agda +++ b/Functor/Instance/Nat/System.agda @@ -2,91 +2,103 @@ module Functor.Instance.Nat.System where + open import Level using (suc; 0ℓ) + open import Categories.Category.Instance.Nat using (Nat) open import Categories.Category.Instance.Setoids using (Setoids) open import Categories.Functor.Core using (Functor) -open import Data.Circuit.Value using (Value) +open import Data.Circuit.Value using (Monoid) open import Data.Fin.Base using (Fin) open import Data.Nat.Base using (ℕ) open import Data.Product.Base using (_,_; _×_) -open import Data.System {suc 0ℓ} using (System; ≤-System; Systemₛ) -open import Data.System.Values Value using (module ≋) -open import Function.Bundles using (Func; _⟶ₛ_) +open import Data.System {suc 0ℓ} using (System; _≤_; Systemₛ) +open import Data.System.Values Monoid using (module ≋) +open import Data.Unit using (⊤; tt) open import Function.Base using (id; _∘_) +open import Function.Bundles using (Func; _⟶ₛ_; _⟨$⟩_) +open import Function.Construct.Identity using () renaming (function to Id) open import Function.Construct.Setoid using (_∙_) -open import Functor.Instance.Nat.Pull using (Pull₁; Pull-resp-≈) -open import Functor.Instance.Nat.Push using (Push₁; Push-identity; Push-homomorphism; Push-resp-≈) +open import Functor.Instance.Nat.Pull using (Pull) +open import Functor.Instance.Nat.Push using (Push) open import Relation.Binary.PropositionalEquality as ≡ using (_≗_) --- import Relation.Binary.Reasoning.Setoid as ≈-Reasoning -import Function.Construct.Identity as Id - open Func -open ≤-System open Functor +open _≤_ private + variable A B C : ℕ -map : (Fin A → Fin B) → System A → System B -map f X = record - { S = S - ; fₛ = fₛ ∙ Pull₁ f - ; fₒ = Push₁ f ∙ fₒ - } - where - open System X - -≤-cong : (f : Fin A → Fin B) {X Y : System A} → ≤-System Y X → ≤-System (map f Y) (map f X) -⇒S (≤-cong f x≤y) = ⇒S x≤y -≗-fₛ (≤-cong f x≤y) = ≗-fₛ x≤y ∘ to (Pull₁ f) -≗-fₒ (≤-cong f x≤y) = cong (Push₁ f) ∘ ≗-fₒ x≤y - -System₁ : (Fin A → Fin B) → Systemₛ A ⟶ₛ Systemₛ B -to (System₁ f) = map f -cong (System₁ f) (x≤y , y≤x) = ≤-cong f x≤y , ≤-cong f y≤x - -id-x≤x : {X : System A} → ≤-System (map id X) X -⇒S (id-x≤x) = Id.function _ -≗-fₛ (id-x≤x {_} {x}) i s = System.refl x -≗-fₒ (id-x≤x {A} {x}) s = Push-identity - -x≤id-x : {x : System A} → ≤-System x (map id x) -⇒S x≤id-x = Id.function _ -≗-fₛ (x≤id-x {A} {x}) i s = System.refl x -≗-fₒ (x≤id-x {A} {x}) s = ≋.sym Push-identity - - -System-homomorphism - : {f : Fin A → Fin B} - {g : Fin B → Fin C} - {X : System A} - → ≤-System (map (g ∘ f) X) (map g (map f X)) × ≤-System (map g (map f X)) (map (g ∘ f) X) -System-homomorphism {f = f} {g} {X} = left , right - where - open System X - left : ≤-System (map (g ∘ f) X) (map g (map f X)) - left .⇒S = Id.function S - left .≗-fₛ i s = refl - left .≗-fₒ s = Push-homomorphism - right : ≤-System (map g (map f X)) (map (g ∘ f) X) - right .⇒S = Id.function S - right .≗-fₛ i s = refl - right .≗-fₒ s = ≋.sym Push-homomorphism - -System-resp-≈ - : {f g : Fin A → Fin B} - → f ≗ g - → {X : System A} - → (≤-System (map f X) (map g X)) × (≤-System (map g X) (map f X)) -System-resp-≈ {A} {B} {f = f} {g} f≗g {X} = both f≗g , both (≡.sym ∘ f≗g) - where - open System X - both : {f g : Fin A → Fin B} → f ≗ g → ≤-System (map f X) (map g X) - both f≗g .⇒S = Id.function S - both f≗g .≗-fₛ i s = cong fₛ (Pull-resp-≈ f≗g {i}) - both {f} {g} f≗g .≗-fₒ s = Push-resp-≈ f≗g + opaque + + map : (Fin A → Fin B) → System A → System B + map f X = let open System X in record + { S = S + ; fₛ = fₛ ∙ Pull.₁ f + ; fₒ = Push.₁ f ∙ fₒ + } + + ≤-cong : (f : Fin A → Fin B) {X Y : System A} → Y ≤ X → map f Y ≤ map f X + ⇒S (≤-cong f x≤y) = ⇒S x≤y + ≗-fₛ (≤-cong f x≤y) = ≗-fₛ x≤y ∘ to (Pull.₁ f) + ≗-fₒ (≤-cong f x≤y) = cong (Push.₁ f) ∘ ≗-fₒ x≤y + + System₁ : (Fin A → Fin B) → Systemₛ A ⟶ₛ Systemₛ B + to (System₁ f) = map f + cong (System₁ f) (x≤y , y≤x) = ≤-cong f x≤y , ≤-cong f y≤x + + opaque + + unfolding System₁ + + id-x≤x : {X : System A} → System₁ id ⟨$⟩ X ≤ X + ⇒S (id-x≤x) = Id _ + ≗-fₛ (id-x≤x {_} {x}) i s = cong (System.fₛ x) Pull.identity + ≗-fₒ (id-x≤x {A} {x}) s = Push.identity + + x≤id-x : {x : System A} → x ≤ System₁ id ⟨$⟩ x + ⇒S x≤id-x = Id _ + ≗-fₛ (x≤id-x {A} {x}) i s = cong (System.fₛ x) (≋.sym Pull.identity) + ≗-fₒ (x≤id-x {A} {x}) s = ≋.sym Push.identity + + System-homomorphism + : {f : Fin A → Fin B} + {g : Fin B → Fin C} + {X : System A} + → System₁ (g ∘ f) ⟨$⟩ X ≤ System₁ g ⟨$⟩ (System₁ f ⟨$⟩ X) + × System₁ g ⟨$⟩ (System₁ f ⟨$⟩ X) ≤ System₁ (g ∘ f) ⟨$⟩ X + System-homomorphism {f = f} {g} {X} = left , right + where + open System X + left : map (g ∘ f) X ≤ map g (map f X) + left .⇒S = Id S + left .≗-fₛ i s = cong fₛ Pull.homomorphism + left .≗-fₒ s = Push.homomorphism + right : map g (map f X) ≤ map (g ∘ f) X + right .⇒S = Id S + right .≗-fₛ i s = cong fₛ (≋.sym Pull.homomorphism) + right .≗-fₒ s = ≋.sym Push.homomorphism + + System-resp-≈ + : {f g : Fin A → Fin B} + → f ≗ g + → {X : System A} + → System₁ f ⟨$⟩ X ≤ System₁ g ⟨$⟩ X + × System₁ g ⟨$⟩ X ≤ System₁ f ⟨$⟩ X + System-resp-≈ {A} {B} {f = f} {g} f≗g {X} = both f≗g , both (≡.sym ∘ f≗g) + where + open System X + both : {f g : Fin A → Fin B} → f ≗ g → map f X ≤ map g X + both f≗g .⇒S = Id S + both f≗g .≗-fₛ i s = cong fₛ (Pull.F-resp-≈ f≗g {i}) + both {f} {g} f≗g .≗-fₒ s = Push.F-resp-≈ f≗g + +opaque + unfolding System₁ + Sys-defs : ⊤ + Sys-defs = tt Sys : Functor Nat (Setoids (suc 0ℓ) (suc 0ℓ)) Sys .F₀ = Systemₛ @@ -94,3 +106,5 @@ Sys .F₁ = System₁ Sys .identity = id-x≤x , x≤id-x Sys .homomorphism {x = X} = System-homomorphism {X = X} Sys .F-resp-≈ = System-resp-≈ + +module Sys = Functor Sys |