Setoid-ify System definition

1 files changed, 49 insertions, 23 deletions

diff --git a/Data/System.agda b/Data/System.agda
index c5bc347..fa7d8e7 100644
--- a/Data/System.agda
+++ b/Data/System.agda
@@ -7,27 +7,49 @@ import Relation.Binary.Properties.Preorder as PreorderProperties
 open import Data.Circuit.Value using (Value)
 open import Data.Nat.Base using (ℕ)
 open import Data.Vec.Functional using (Vector)
-open import Data.Fin.Base using (Fin)
-open import Level using (Level; suc; 0ℓ)
-open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_)
+open import Level using (Level; _⊔_; 0ℓ; suc)
+open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
 open import Relation.Binary using (Rel; Reflexive; Transitive; Preorder; _⇒_; Setoid)
 open import Function.Base using (id; _∘_)
+import Function.Construct.Identity as Id
+open import Data.Vec.Functional.Relation.Binary.Equality.Setoid using (≋-setoid)
 
-Input : ℕ → Set
-Input = Vector Value
+open import Function.Bundles using (Func; _⟶ₛ_; _⟨$⟩_)
 
-Output : ℕ → Set
-Output = Vector Value
+open import Function.Construct.Setoid using (setoid; _∙_)
+open Func
+
+_⇒ₛ_ : {a₁ a₂ b₁ b₂ : Level} → Setoid a₁ a₂ → Setoid b₁ b₂ → Setoid (a₁ ⊔ a₂ ⊔ b₁ ⊔ b₂) (a₁ ⊔ b₂)
+_⇒ₛ_ = setoid
+
+infixr 0 _⇒ₛ_
+
+∣_∣ : {c ℓ : Level} → Setoid c ℓ → Set c
+∣_∣ = Setoid.Carrier
+
+Values : ℕ → Setoid 0ℓ 0ℓ
+Values = ≋-setoid (≡.setoid Value)
+
+_≋_ : {n : ℕ} → Rel (Vector Value n) 0ℓ
+_≋_ {n} = Setoid._≈_ (Values n)
+
+module ≋ {n : ℕ} = Setoid (Values n)
 
 module _ {ℓ : Level} where
 
   record System (n : ℕ) : Set (suc ℓ) where
     field
-      S : Set ℓ
-      fₛ : Input n → S → S
-      fₒ : Input n → S → Output n
-      fₛ-cong : {i j : Input n} → i ≗ j → fₛ i ≗ fₛ j
-      fₒ-cong : {i j : Input n} → i ≗ j → (s : S) → fₒ i s ≗ fₒ j s
+      S : Setoid ℓ ℓ
+      fₛ : ∣ Values n ⇒ₛ S ⇒ₛ S ∣
+      fₒ : ∣ Values n ⇒ₛ S ⇒ₛ Values n ∣
+
+    fₛ′ : ∣ Values n ∣ → ∣ S ∣ → ∣ S ∣
+    fₛ′ = to ∘ to fₛ
+
+    fₒ′ : ∣ Values n ∣ → ∣ S ∣ → ∣ Values n ∣
+    fₒ′ = to ∘ to fₒ
+
+    open Setoid S public
 
   module _ {n : ℕ} where
 
@@ -35,25 +57,29 @@ module _ {ℓ : Level} where
       module A = System a
       module B = System b
       field
-        ⇒S : A.S → B.S
-        ≗-fₛ : (i : Input n) (s : A.S) → ⇒S (A.fₛ i s) ≡ B.fₛ i (⇒S s)
-        ≗-fₒ : (i : Input n) (s : A.S) (k : Fin n) → A.fₒ i s k ≡ B.fₒ i (⇒S s) k
+        ⇒S : ∣ A.S ⇒ₛ B.S ∣
+        ≗-fₛ
+            : (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)
 
     open ≤-System
 
     ≤-refl : Reflexive ≤-System
-    ⇒S ≤-refl = id
-    ≗-fₛ ≤-refl _ _ = ≡.refl
-    ≗-fₒ ≤-refl _ _ _ = ≡.refl
+    ⇒S ≤-refl = Id.function _
+    ≗-fₛ (≤-refl {x}) p e = System.refl x
+    ≗-fₒ (≤-refl {x}) _ _ = ≋.refl
 
     ≡⇒≤ : _≡_ ⇒ ≤-System
     ≡⇒≤ ≡.refl = ≤-refl
 
     open System
     ≤-trans : Transitive ≤-System
-    ⇒S (≤-trans a b) = ⇒S b ∘ ⇒S a
-    ≗-fₛ (≤-trans a b) i s = ≡.trans (≡.cong (⇒S b) (≗-fₛ a i s)) (≗-fₛ b i (⇒S a s))
-    ≗-fₒ (≤-trans a b) i s k = ≡.trans (≗-fₒ a i s k) (≗-fₒ b i (⇒S a s) k)
+    ⇒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))
 
     System-Preorder : Preorder (suc ℓ) (suc ℓ) ℓ
     System-Preorder = record
@@ -70,5 +96,5 @@ module _ {ℓ : Level} where
   module _ (n : ℕ) where
 
     open PreorderProperties (System-Preorder {n}) using (InducedEquivalence)
-    System-Setoid : Setoid (suc ℓ) ℓ
-    System-Setoid = InducedEquivalence
+    Systemₛ : Setoid (suc ℓ) ℓ
+    Systemₛ = InducedEquivalence