diff options
Diffstat (limited to 'Functor/Instance/Nat/System.agda')
| -rw-r--r-- | Functor/Instance/Nat/System.agda | 150 |
1 files changed, 82 insertions, 68 deletions
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 |