diff options
| -rw-r--r-- | Data/System.agda | 16 | ||||
| -rw-r--r-- | Functor/Instance/Nat/Pull.agda | 7 | ||||
| -rw-r--r-- | Functor/Instance/Nat/Push.agda | 9 | ||||
| -rw-r--r-- | Functor/Instance/Nat/System.agda | 94 |
4 files changed, 107 insertions, 19 deletions
diff --git a/Data/System.agda b/Data/System.agda index fa7d8e7..e2ac073 100644 --- a/Data/System.agda +++ b/Data/System.agda @@ -41,13 +41,13 @@ module _ {ℓ : Level} where field S : Setoid ℓ ℓ fₛ : ∣ Values n ⇒ₛ S ⇒ₛ S ∣ - fₒ : ∣ Values n ⇒ₛ S ⇒ₛ Values n ∣ + fₒ : ∣ S ⇒ₛ Values n ∣ fₛ′ : ∣ Values n ∣ → ∣ S ∣ → ∣ S ∣ fₛ′ = to ∘ to fₛ - fₒ′ : ∣ Values n ∣ → ∣ S ∣ → ∣ Values n ∣ - fₒ′ = to ∘ to fₒ + fₒ′ : ∣ S ∣ → ∣ Values n ∣ + fₒ′ = to fₒ open Setoid S public @@ -62,15 +62,15 @@ module _ {ℓ : Level} where : (i : ∣ Values n ∣) (s : ∣ A.S ∣) → ⇒S ⟨$⟩ (A.fₛ′ i s) B.≈ B.fₛ′ i (⇒S ⟨$⟩ s) ≗-fₒ - : (i : ∣ Values n ∣) (s : ∣ A.S ∣) - → A.fₒ′ i s ≋ B.fₒ′ i (⇒S ⟨$⟩ s) + : (s : ∣ A.S ∣) + → A.fₒ′ s ≋ B.fₒ′ (⇒S ⟨$⟩ s) open ≤-System ≤-refl : Reflexive ≤-System ⇒S ≤-refl = Id.function _ - ≗-fₛ (≤-refl {x}) p e = System.refl x - ≗-fₒ (≤-refl {x}) _ _ = ≋.refl + ≗-fₛ (≤-refl {x}) _ _ = System.refl x + ≗-fₒ (≤-refl {x}) _ = ≋.refl ≡⇒≤ : _≡_ ⇒ ≤-System ≡⇒≤ ≡.refl = ≤-refl @@ -79,7 +79,7 @@ module _ {ℓ : Level} where ≤-trans : Transitive ≤-System ⇒S (≤-trans a b) = ⇒S b ∙ ⇒S a ≗-fₛ (≤-trans {x} {y} {z} a b) i s = System.trans z (cong (⇒S b) (≗-fₛ a i s)) (≗-fₛ b i (⇒S a ⟨$⟩ s)) - ≗-fₒ (≤-trans {x} {y} {z} a b) i s = ≋.trans (≗-fₒ a i s) (≗-fₒ b i (⇒S a ⟨$⟩ s)) + ≗-fₒ (≤-trans a b) s = ≋.trans (≗-fₒ a s) (≗-fₒ b (⇒S a ⟨$⟩ s)) System-Preorder : Preorder (suc ℓ) (suc ℓ) ℓ System-Preorder = record diff --git a/Functor/Instance/Nat/Pull.agda b/Functor/Instance/Nat/Pull.agda index 3f13303..cf15809 100644 --- a/Functor/Instance/Nat/Pull.agda +++ b/Functor/Instance/Nat/Pull.agda @@ -7,12 +7,10 @@ open import Categories.Category.Instance.Nat using (Nat) open import Categories.Category.Instance.Setoids using (Setoids) open import Categories.Functor using (Functor) open import Data.Circuit.Merge using (merge; merge-cong₁; merge-cong₂; merge-⁅⁆; merge-preimage) -open import Data.Circuit.Value using (Value) open import Data.Fin.Base using (Fin) open import Data.Fin.Preimage using (preimage; preimage-cong₁) open import Data.Nat.Base using (ℕ) open import Data.Subset.Functional using (⁅_⁆) -open import Data.Vec.Functional.Relation.Binary.Equality.Setoid using (≋-setoid) open import Function.Base using (id; flip; _∘_) open import Function.Bundles using (Func; _⟶ₛ_) open import Function.Construct.Identity using () renaming (function to Id) @@ -20,6 +18,7 @@ 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.System using (Values) open Functor open Func @@ -33,9 +32,7 @@ infixr 4 _≈_ private variable A B C : ℕ --- action on objects (Vector Value n) -Values : ℕ → Setoid 0ℓ 0ℓ -Values = ≋-setoid (≡.setoid Value) +-- action on objects is Values n (Vector Value n) -- action of Pull on morphisms (contravariant) Pull₁ : (Fin A → Fin B) → Values B ⟶ₛ Values A diff --git a/Functor/Instance/Nat/Push.agda b/Functor/Instance/Nat/Push.agda index c7443ab..8b40bd7 100644 --- a/Functor/Instance/Nat/Push.agda +++ b/Functor/Instance/Nat/Push.agda @@ -5,20 +5,19 @@ module Functor.Instance.Nat.Push where open import Categories.Functor using (Functor) open import Categories.Category.Instance.Nat using (Nat) open import Categories.Category.Instance.Setoids using (Setoids) -open import Data.Circuit.Value using (Value) open import Data.Circuit.Merge using (merge; merge-cong₁; merge-cong₂; merge-⁅⁆; merge-preimage) open import Data.Fin.Base using (Fin) open import Data.Fin.Preimage using (preimage; preimage-cong₁) open import Data.Nat.Base using (ℕ) open import Data.Subset.Functional using (⁅_⁆) -open import Data.Vec.Functional.Relation.Binary.Equality.Setoid using (≋-setoid) -open import Function.Base using (id; flip; _∘_) +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 (setoid; _∙_) open import Level using (0ℓ) open import Relation.Binary using (Rel; Setoid) open import Relation.Binary.PropositionalEquality as ≡ using (_≗_) +open import Data.System using (Values) open Func open Functor @@ -30,9 +29,7 @@ _≈_ : {X Y : Setoid 0ℓ 0ℓ} → Rel (X ⟶ₛ Y) 0ℓ _≈_ {X} {Y} = Setoid._≈_ (setoid X Y) infixr 4 _≈_ --- action on objects (Vector Value n) -Values : ℕ → Setoid 0ℓ 0ℓ -Values = ≋-setoid (≡.setoid Value) +-- 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 diff --git a/Functor/Instance/Nat/System.agda b/Functor/Instance/Nat/System.agda new file mode 100644 index 0000000..2b96355 --- /dev/null +++ b/Functor/Instance/Nat/System.agda @@ -0,0 +1,94 @@ +{-# OPTIONS --without-K --safe #-} + +module Functor.Instance.Nat.System {ℓ} where + +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.Fin.Base using (Fin) +open import Data.Nat.Base using (ℕ) +open import Data.Product.Base using (_,_; _×_) +open import Data.System using (System; ≤-System; Systemₛ; module ≋) +open import Function.Bundles using (Func; _⟶ₛ_) +open import Function.Base using (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 Level using (suc) +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 + +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 + +Sys : Functor Nat (Setoids (suc ℓ) ℓ) +Sys .F₀ = Systemₛ +Sys .F₁ = System₁ +Sys .identity = id-x≤x , x≤id-x +Sys .homomorphism {x = X} = System-homomorphism {X = X} +Sys .F-resp-≈ = System-resp-≈ |