diff options
Diffstat (limited to 'Data/System.agda')
| -rw-r--r-- | Data/System.agda | 142 |
1 files changed, 5 insertions, 137 deletions
diff --git a/Data/System.agda b/Data/System.agda index a2adec3..968332d 100644 --- a/Data/System.agda +++ b/Data/System.agda @@ -1,142 +1,10 @@ {-# OPTIONS --without-K --safe #-} -open import Level using (Level; 0ℓ; suc) +open import Level using (Level) module Data.System {ℓ : Level} where -import Relation.Binary.Properties.Preorder as PreorderProperties -import Relation.Binary.Reasoning.Setoid as ≈-Reasoning - -open import Categories.Category using (Category) -open import Data.Circuit.Value using (Monoid) -open import Data.Nat using (ℕ) -open import Data.Setoid using (_⇒ₛ_; ∣_∣) -open import Data.Setoid.Unit using (⊤ₛ) -open import Data.Values Monoid using (Values; _≋_; module ≋; <ε>) -open import Function using (Func; _⟨$⟩_; flip) -open import Function.Construct.Constant using () renaming (function to Const) -open import Function.Construct.Identity using () renaming (function to Id) -open import Function.Construct.Setoid using (_∙_) -open import Level using (Level; 0ℓ; suc) -open import Relation.Binary as Rel using (Reflexive; Transitive; Preorder; Setoid; Rel) -open import Relation.Binary.PropositionalEquality as ≡ using (_≡_) - -open Func - -module _ (n : ℕ) where - - record System : Set₁ where - - field - S : Setoid 0ℓ 0ℓ - fₛ : ∣ Values n ⇒ₛ S ⇒ₛ S ∣ - fₒ : ∣ S ⇒ₛ Values n ∣ - - fₛ′ : ∣ Values n ∣ → ∣ S ∣ → ∣ S ∣ - fₛ′ i = to (to fₛ i) - - fₒ′ : ∣ S ∣ → ∣ Values n ∣ - fₒ′ = to fₒ - - module S = Setoid S - - open System - - discrete : System - discrete .S = ⊤ₛ - discrete .fₛ = Const (Values n) (⊤ₛ ⇒ₛ ⊤ₛ) (Id ⊤ₛ) - discrete .fₒ = Const ⊤ₛ (Values n) <ε> - -module _ {n : ℕ} where - - record _≤_ (a b : System n) : Set ℓ where - - private - module A = System a - module B = System b - - open B using (S) - - field - ⇒S : ∣ A.S ⇒ₛ B.S ∣ - ≗-fₛ : (i : ∣ Values n ∣) (s : ∣ A.S ∣) → ⇒S ⟨$⟩ (A.fₛ′ i s) S.≈ B.fₛ′ i (⇒S ⟨$⟩ s) - ≗-fₒ : (s : ∣ A.S ∣) → A.fₒ′ s ≋ B.fₒ′ (⇒S ⟨$⟩ s) - - infix 4 _≤_ - -open System - -module _ {n : ℕ} where - - open _≤_ - - ≤-refl : Reflexive (_≤_ {n}) - ⇒S ≤-refl = Id _ - ≗-fₛ (≤-refl {x}) _ _ = S.refl x - ≗-fₒ ≤-refl _ = ≋.refl - - ≡⇒≤ : _≡_ Rel.⇒ _≤_ - ≡⇒≤ ≡.refl = ≤-refl - - ≤-trans : Transitive _≤_ - ⇒S (≤-trans a b) = ⇒S b ∙ ⇒S a - ≗-fₛ (≤-trans {x} {y} {z} a b) i s = let open ≈-Reasoning (S z) in begin - ⇒S b ⟨$⟩ (⇒S a ⟨$⟩ (fₛ′ x i s)) ≈⟨ cong (⇒S b) (≗-fₛ a i s) ⟩ - ⇒S b ⟨$⟩ (fₛ′ y i (⇒S a ⟨$⟩ s)) ≈⟨ ≗-fₛ b i (⇒S a ⟨$⟩ s) ⟩ - fₛ′ z i (⇒S b ⟨$⟩ (⇒S a ⟨$⟩ s)) ∎ - ≗-fₒ (≤-trans {x} {y} {z} a b) s = let open ≈-Reasoning (Values n) in begin - fₒ′ x s ≈⟨ ≗-fₒ a s ⟩ - fₒ′ y (⇒S a ⟨$⟩ s) ≈⟨ ≗-fₒ b (⇒S a ⟨$⟩ s) ⟩ - fₒ′ z (⇒S b ⟨$⟩ (⇒S a ⟨$⟩ s)) ∎ - - variable - A B C : System n - - _≈_ : Rel (A ≤ B) 0ℓ - _≈_ {A} {B} ≤₁ ≤₂ = ⇒S ≤₁ A⇒B.≈ ⇒S ≤₂ - where - module A⇒B = Setoid (S A ⇒ₛ S B) - - open Rel.IsEquivalence - - ≈-isEquiv : Rel.IsEquivalence (_≈_ {A} {B}) - ≈-isEquiv {B = B} .refl = S.refl B - ≈-isEquiv {B = B} .sym a = S.sym B a - ≈-isEquiv {B = B} .trans a b = S.trans B a b - - ≤-resp-≈ : {f h : B ≤ C} {g i : A ≤ B} → f ≈ h → g ≈ i → ≤-trans g f ≈ ≤-trans i h - ≤-resp-≈ {_} {C} {_} {f} {h} {g} {i} f≈h g≈i {x} = begin - ⇒S f ⟨$⟩ (⇒S g ⟨$⟩ x) ≈⟨ f≈h ⟩ - ⇒S h ⟨$⟩ (⇒S g ⟨$⟩ x) ≈⟨ cong (⇒S h) g≈i ⟩ - ⇒S h ⟨$⟩ (⇒S i ⟨$⟩ x) ∎ - where - open ≈-Reasoning (System.S C) - -System-≤ : ℕ → Preorder (suc 0ℓ) (suc 0ℓ) ℓ -System-≤ n = record - { _≲_ = _≤_ {n} - ; isPreorder = record - { isEquivalence = ≡.isEquivalence - ; reflexive = ≡⇒≤ - ; trans = ≤-trans - } - } - -Systemₛ : ℕ → Setoid (suc 0ℓ) ℓ -Systemₛ n = PreorderProperties.InducedEquivalence (System-≤ n) - -Systems : ℕ → Category (suc 0ℓ) ℓ 0ℓ -Systems n = record - { Obj = System n - ; _⇒_ = _≤_ - ; _≈_ = _≈_ - ; id = ≤-refl - ; _∘_ = flip ≤-trans - ; assoc = λ {D = D} → S.refl D - ; sym-assoc = λ {D = D} → S.refl D - ; identityˡ = λ {B = B} → S.refl B - ; identityʳ = λ {B = B} → S.refl B - ; identity² = λ {A = A} → S.refl A - ; equiv = ≈-isEquiv - ; ∘-resp-≈ = λ {f = f} {h} {g} {i} → ≤-resp-≈ {f = f} {h} {g} {i} - } +open import Data.System.Core {ℓ} public +open import Data.System.Category {ℓ} public +open import Data.System.Looped {ℓ} public +open import Data.System.Monoidal {ℓ} public using (Systems-MC; Systems-SMC) |