diff options
Diffstat (limited to 'Data/System.agda')
| -rw-r--r-- | Data/System.agda | 179 |
1 files changed, 119 insertions, 60 deletions
diff --git a/Data/System.agda b/Data/System.agda index cecdfcd..5d5e484 100644 --- a/Data/System.agda +++ b/Data/System.agda @@ -1,85 +1,144 @@ {-# OPTIONS --without-K --safe #-} open import Level using (Level; 0ℓ; suc) + module Data.System {ℓ : Level} where -import Function.Construct.Identity as Id import Relation.Binary.Properties.Preorder as PreorderProperties +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning -open import Data.Circuit.Value using (Value) -open import Data.Nat.Base using (ℕ) +open import Categories.Category using (Category) +open import Categories.Category.Instance.SingletonSet using () renaming (SingletonSetoid to ⊤ₛ) +open import Data.Circuit.Value using (Monoid) +open import Data.Nat using (ℕ) open import Data.Setoid using (_⇒ₛ_; ∣_∣) -open import Data.System.Values Value using (Values; _≋_; module ≋) +open import Data.System.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 import Relation.Binary using (Reflexive; Transitive; Preorder; _⇒_; Setoid) -open import Function.Base using (_∘_) -open import Function.Bundles using (Func; _⟨$⟩_) -open import Function.Construct.Setoid using (_∙_) open Func -record System (n : ℕ) : Set₁ where - - field - S : Setoid 0ℓ 0ℓ - fₛ : ∣ Values n ⇒ₛ S ⇒ₛ S ∣ - fₒ : ∣ S ⇒ₛ Values n ∣ - - fₛ′ : ∣ Values n ∣ → ∣ S ∣ → ∣ S ∣ - fₛ′ = to ∘ to fₛ - - fₒ′ : ∣ S ∣ → ∣ Values n ∣ - fₒ′ = to fₒ - - open Setoid S public +module _ (n : ℕ) where -module _ {n : ℕ} where + record System : Set₁ where - record ≤-System (a b : System n) : Set ℓ where - module A = System a - module B = System b field - ⇒S : ∣ A.S ⇒ₛ B.S ∣ - ≗-fₛ - : (i : ∣ Values n ∣) (s : ∣ A.S ∣) - → ⇒S ⟨$⟩ (A.fₛ′ i s) B.≈ B.fₛ′ i (⇒S ⟨$⟩ s) - ≗-fₒ - : (s : ∣ A.S ∣) - → A.fₒ′ s ≋ B.fₒ′ (⇒S ⟨$⟩ s) + S : Setoid 0ℓ 0ℓ + fₛ : ∣ Values n ⇒ₛ S ⇒ₛ S ∣ + fₒ : ∣ S ⇒ₛ Values n ∣ - open ≤-System + fₛ′ : ∣ Values n ∣ → ∣ S ∣ → ∣ S ∣ + fₛ′ i = to (to fₛ i) - ≤-refl : Reflexive ≤-System - ⇒S ≤-refl = Id.function _ - ≗-fₛ (≤-refl {x}) _ _ = System.refl x - ≗-fₒ (≤-refl {x}) _ = ≋.refl + fₒ′ : ∣ S ∣ → ∣ Values n ∣ + fₒ′ = to fₒ - ≡⇒≤ : _≡_ ⇒ ≤-System - ≡⇒≤ ≡.refl = ≤-refl + module S = Setoid S open System - ≤-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 a b) s = ≋.trans (≗-fₒ a s) (≗-fₒ b (⇒S a ⟨$⟩ s)) - - System-Preorder : Preorder (suc 0ℓ) (suc 0ℓ) ℓ - System-Preorder = record - { Carrier = System n - ; _≈_ = _≡_ - ; _≲_ = ≤-System - ; isPreorder = record - { isEquivalence = ≡.isEquivalence - ; reflexive = ≡⇒≤ - ; trans = ≤-trans - } - } + discrete : System + discrete .S = ⊤ₛ + discrete .fₛ = Const (Values n) (⊤ₛ ⇒ₛ ⊤ₛ) (Id ⊤ₛ) + discrete .fₒ = Const ⊤ₛ (Values n) <ε> -module _ (n : ℕ) where +module _ {n : ℕ} where - open PreorderProperties (System-Preorder {n}) using (InducedEquivalence) + record _≤_ (a b : System n) : Set ℓ where - Systemₛ : Setoid (suc 0ℓ) ℓ - Systemₛ = InducedEquivalence + 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 + +private + + 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} + } |