diff options
Diffstat (limited to 'Data/System/Looped.agda')
| -rw-r--r-- | Data/System/Looped.agda | 105 |
1 files changed, 55 insertions, 50 deletions
diff --git a/Data/System/Looped.agda b/Data/System/Looped.agda index 96f3432..1fd86d6 100644 --- a/Data/System/Looped.agda +++ b/Data/System/Looped.agda @@ -1,74 +1,79 @@ {-# OPTIONS --without-K --safe #-} -open import Level using (Level; 0ℓ; suc) +open import Level using (Level; suc; _⊔_) -module Data.System.Looped {ℓ : Level} where +module Data.System.Looped {c ℓ : Level} where import Relation.Binary.Reasoning.Setoid as ≈-Reasoning +open import Algebra using (CommutativeMonoid) open import Categories.Category using (Category) open import Categories.Category.Helper using (categoryHelper) open import Categories.Functor using (Functor) -open import Data.Nat using (ℕ) -open import Data.System.Category {ℓ} using (Systems[_,_]) -open import Data.System.Core {ℓ} using (System; _≤_) -open import Categories.Functor using (Functor) -open import Data.Circuit.Value using (monoid) -open import Data.Values monoid using (_⊕_; ⊕-cong; module ≋) -open import Relation.Binary using (Setoid) +open import Data.System.Category using (Systems[_,_]) +open import Data.System.Core using (System; _≤_) open import Function using (Func; _⟨$⟩_) renaming (id to idf) +open import Relation.Binary using (Setoid) open Func open System private - loop : {n : ℕ} → System n n → System n n - loop X = record - { S = X.S - ; fₛ = record - { to = λ i → record - { to = λ s → X.fₛ′ (i ⊕ X.fₒ′ s) s - ; cong = λ {s} {s′} ≈s → X.S.trans - (cong X.fₛ (⊕-cong ≋.refl (cong X.fₒ ≈s))) (cong (X.fₛ ⟨$⟩ (i ⊕ X.fₒ′ s′)) ≈s) - } - ; cong = λ ≋v → cong X.fₛ (⊕-cong ≋v ≋.refl) - } - ; fₒ = X.fₒ - } - where - module X = System X + module _ {V : CommutativeMonoid c ℓ} where - loop-≤ : {n : ℕ} {A B : System n n} → A ≤ B → loop A ≤ loop B - loop-≤ {_} {A} {B} A≤B = record - { ⇒S = A≤B.⇒S - ; ≗-fₛ = λ i s → begin - A≤B.⇒S ⟨$⟩ (fₛ′ (loop A) i s) ≈⟨ A≤B.≗-fₛ (i ⊕ A.fₒ′ s) s ⟩ - B.fₛ′ (i ⊕ A.fₒ′ s) (A≤B.⇒S ⟨$⟩ s) ≈⟨ cong B.fₛ (⊕-cong ≋.refl (A≤B.≗-fₒ s)) ⟩ - B.fₛ′ (i ⊕ B.fₒ′ (A≤B.⇒S ⟨$⟩ s)) (A≤B.⇒S ⟨$⟩ s) ∎ - ; ≗-fₒ = A≤B.≗-fₒ - } - where - module A = System A - module B = System B - open ≈-Reasoning B.S - module A≤B = _≤_ A≤B + open CommutativeMonoid V -Loop : (n : ℕ) → Functor Systems[ n , n ] Systems[ n , n ] -Loop n = record - { F₀ = loop - ; F₁ = loop-≤ - ; identity = λ {A} → Setoid.refl (S A) - ; homomorphism = λ {Z = Z} → Setoid.refl (S Z) - ; F-resp-≈ = idf - } + loop : System setoid V → System setoid V + loop X = record + { S = X.S + ; fₛ = record + { to = λ i → record + { to = λ s → X.fₛ′ (i ∙ X.fₒ′ s) s + ; cong = λ {s} {s′} ≈s → + X.S.trans + (cong X.fₛ (∙-cong refl (cong X.fₒ ≈s))) + (cong (X.fₛ ⟨$⟩ (i ∙ X.fₒ′ s′)) ≈s) + } + ; cong = λ ≈v → cong X.fₛ (∙-congʳ ≈v) + } + ; fₒ = X.fₒ + } + where + module X = System X -module _ (n : ℕ) where + loop-≤ : {A B : System setoid V} → A ≤ B → loop A ≤ loop B + loop-≤ {A} {B} A≤B = record + { ⇒S = A≤B.⇒S + ; ≗-fₛ = λ i s → begin + A≤B.⇒S ⟨$⟩ (fₛ′ (loop A) i s) ≈⟨ A≤B.≗-fₛ (i ∙ A.fₒ′ s) s ⟩ + B.fₛ′ (i ∙ A.fₒ′ s) (A≤B.⇒S ⟨$⟩ s) ≈⟨ cong B.fₛ (∙-cong refl (A≤B.≗-fₒ s)) ⟩ + B.fₛ′ (i ∙ B.fₒ′ (A≤B.⇒S ⟨$⟩ s)) (A≤B.⇒S ⟨$⟩ s) ∎ + ; ≗-fₒ = A≤B.≗-fₒ + } + where + module A = System A + module B = System B + open ≈-Reasoning B.S + module A≤B = _≤_ A≤B + +module _ (V : CommutativeMonoid c ℓ) where + + open CommutativeMonoid V using (setoid) + + Loop : Functor Systems[ setoid , V ] Systems[ setoid , V ] + Loop = record + { F₀ = loop + ; F₁ = loop-≤ + ; identity = λ {A} → Setoid.refl (S A) + ; homomorphism = λ {Z = Z} → Setoid.refl (S Z) + ; F-resp-≈ = idf + } - open Category Systems[ n , n ] - open Functor (Loop n) + open Category Systems[ setoid , V ] + open Functor Loop - Systems[_] : Category (suc 0ℓ) ℓ 0ℓ + Systems[_] : Category (c ⊔ suc ℓ) (c ⊔ ℓ) ℓ Systems[_] = categoryHelper record { Obj = Obj ; _⇒_ = _⇒_ |