diff options
| -rw-r--r-- | Data/System.agda | 142 | ||||
| -rw-r--r-- | Data/System/Category.agda | 63 | ||||
| -rw-r--r-- | Data/System/Core.agda | 84 | ||||
| -rw-r--r-- | Data/System/Looped.agda | 83 | ||||
| -rw-r--r-- | Data/System/Looped/Monoidal.agda | 120 | ||||
| -rw-r--r-- | Data/System/Monoidal.agda | 37 | ||||
| -rw-r--r-- | Functor/Instance/Nat/System.agda | 86 | ||||
| -rw-r--r-- | NaturalTransformation/Instance/GateSemantics.agda | 10 |
8 files changed, 421 insertions, 204 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) diff --git a/Data/System/Category.agda b/Data/System/Category.agda new file mode 100644 index 0000000..171a003 --- /dev/null +++ b/Data/System/Category.agda @@ -0,0 +1,63 @@ +{-# OPTIONS --without-K --safe #-} + +open import Level using (Level; 0ℓ; suc) + +module Data.System.Category {ℓ : Level} where + +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning + +open import Categories.Category using (Category) +open import Data.Nat using (ℕ) +open import Data.System.Core {ℓ} using (System; _≤_; ≤-trans; ≤-refl) +open import Data.Setoid using (_⇒ₛ_) +open import Function using (Func; _⟨$⟩_; flip) +open import Relation.Binary as Rel using (Setoid; Rel) + +open Func +open System +open _≤_ + +private module ≈ {n m : ℕ} where + + private + variable + A B C : System n m + + _≈_ : 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) + +open ≈ using (_≈_) public +open ≈ using (≈-isEquiv; ≤-resp-≈) + +Systems[_,_] : ℕ → ℕ → Category (suc 0ℓ) ℓ 0ℓ +Systems[ n , m ] = record + { Obj = System n m + ; _⇒_ = _≤_ + ; _≈_ = _≈_ + ; 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} + } diff --git a/Data/System/Core.agda b/Data/System/Core.agda new file mode 100644 index 0000000..6da264c --- /dev/null +++ b/Data/System/Core.agda @@ -0,0 +1,84 @@ +{-# OPTIONS --without-K --safe #-} + +open import Level using (Level; 0ℓ; suc) + +module Data.System.Core {ℓ : Level} where + +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning + +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; _⟨$⟩_) +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 Relation.Binary using (Setoid; Reflexive; Transitive) + +open Func + +-- A dynamical system with a set of states, +-- a state update function, +-- and a readout function +record System (n m : ℕ) : Set₁ where + + field + S : Setoid 0ℓ 0ℓ + fₛ : ∣ Values n ⇒ₛ S ⇒ₛ S ∣ + fₒ : ∣ S ⇒ₛ Values m ∣ + + fₛ′ : ∣ Values n ∣ → ∣ S ∣ → ∣ S ∣ + fₛ′ i = to (to fₛ i) + + fₒ′ : ∣ S ∣ → ∣ Values m ∣ + fₒ′ = to fₒ + + module S = Setoid S + +open System + +-- the discrete system from n nodes to m nodes +discrete : (n m : ℕ) → System n m +discrete _ _ .S = ⊤ₛ +discrete n _ .fₛ = Const (Values n) (⊤ₛ ⇒ₛ ⊤ₛ) (Id ⊤ₛ) +discrete _ m .fₒ = Const ⊤ₛ (Values m) <ε> + +module _ {n m : ℕ} where + + -- Simulation of systems: a mapping of internal + -- states which respects i/o behavior + record _≤_ (A B : System n m) : Set ℓ where + + private + 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.S.≈ B.fₛ′ i (⇒S ⟨$⟩ s) + ≗-fₒ : (s : ∣ A.S ∣) → A.fₒ′ s ≋ B.fₒ′ (⇒S ⟨$⟩ s) + + infix 4 _≤_ + + open _≤_ + open System + + -- ≤ is reflexive: every system simulates itself + ≤-refl : Reflexive _≤_ + ⇒S ≤-refl = Id _ + ≗-fₛ (≤-refl {x}) _ _ = S.refl x + ≗-fₒ ≤-refl _ = ≋.refl + + -- ≤ is transitive: if B simulates A, and C simulates B, then C simulates A + ≤-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 m) 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)) ∎ diff --git a/Data/System/Looped.agda b/Data/System/Looped.agda new file mode 100644 index 0000000..f69d75b --- /dev/null +++ b/Data/System/Looped.agda @@ -0,0 +1,83 @@ +{-# OPTIONS --without-K --safe #-} + +open import Level using (Level; 0ℓ; suc) + +module Data.System.Looped {ℓ : Level} where + +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning + +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 Function using (Func; _⟨$⟩_) renaming (id to idf) + +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 + + 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 + +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 + } + +module _ (n : ℕ) where + + open Category Systems[ n , n ] + open Functor (Loop n) + + Systems[_] : Category (suc 0ℓ) ℓ 0ℓ + Systems[_] = categoryHelper record + { Obj = Obj + ; _⇒_ = _⇒_ + ; _≈_ = λ f g → F₁ f ≈ F₁ g + ; id = id + ; _∘_ = _∘_ + ; assoc = λ {f = f} {g h} → assoc {f = f} {g} {h} + ; identityˡ = λ {A B f} → identityˡ {A} {B} {f} + ; identityʳ = λ {A B f} → identityʳ {A} {B} {f} + ; equiv = equiv + ; ∘-resp-≈ = λ {f = f} {g h i} f≈g h≈i → ∘-resp-≈ {f = f} {g} {h} {i} f≈g h≈i + } diff --git a/Data/System/Looped/Monoidal.agda b/Data/System/Looped/Monoidal.agda new file mode 100644 index 0000000..af3d77c --- /dev/null +++ b/Data/System/Looped/Monoidal.agda @@ -0,0 +1,120 @@ +{-# OPTIONS --without-K --safe #-} + +open import Level using (Level; 0ℓ; suc) + +module Data.System.Looped.Monoidal {ℓ : Level} where + +import Categories.Morphism as Morphism +import Data.System.Monoidal {ℓ} as Unlooped + +open import Categories.Category.Monoidal using (Monoidal) +open import Categories.Category.Monoidal.Symmetric using (Symmetric) +open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_) +open import Categories.Category.Monoidal.Bundle using (MonoidalCategory; SymmetricMonoidalCategory) +open import Categories.Functor.Bifunctor using (Bifunctor; flip-bifunctor) +open import Data.Nat using (ℕ) +open import Data.System.Core {ℓ} using (System) +open import Data.System.Looped {ℓ} using (Systems[_]) + +module _ (n : ℕ) where + + private + + module Systems-MC = MonoidalCategory (Unlooped.Systems-MC n n) + + ⊗ : Bifunctor Systems[ n ] Systems[ n ] Systems[ n ] + ⊗ = record + { F₀ = Systems-MC.⊗.₀ + ; F₁ = Systems-MC.⊗.₁ + ; identity = λ {X} → Systems-MC.⊗.identity {X} + ; homomorphism = λ {f = f} {g} → Systems-MC.⊗.homomorphism {f = f} {g} + ; F-resp-≈ = λ {f = f} {g} → Systems-MC.⊗.F-resp-≈ {f = f} {g} + } + + module _ {X : System n n} where + + open Morphism Systems[ n ] using (_≅_; module Iso) + open Systems-MC using (_⊗₀_) + + unitorˡ : Systems-MC.unit ⊗₀ X ≅ X + unitorˡ = record + { from = Systems-MC.unitorˡ.from + ; to = Systems-MC.unitorˡ.to + ; iso = record + { isoˡ = Systems-MC.unitorˡ.isoˡ {X} + ; isoʳ = Systems-MC.unitorˡ.isoʳ {X} + } + } + + unitorʳ : X ⊗₀ Systems-MC.unit ≅ X + unitorʳ = record + { from = Systems-MC.unitorʳ.from + ; to = Systems-MC.unitorʳ.to + ; iso = record + { isoˡ = Systems-MC.unitorʳ.isoˡ {X} + ; isoʳ = Systems-MC.unitorʳ.isoʳ {X} + } + } + + module _ {X Y Z : System n n} where + + module X = System X + module Y = System Y + module Z = System Z + + open Morphism Systems[ n ] using (_≅_; module Iso) + open Systems-MC using (_⊗₀_) + + associator : (X ⊗₀ Y) ⊗₀ Z ≅ X ⊗₀ (Y ⊗₀ Z) + associator = record + { from = Systems-MC.associator.from + ; to = Systems-MC.associator.to + ; iso = record + { isoˡ = Systems-MC.associator.isoˡ {X} {Y} {Z} + ; isoʳ = Systems-MC.associator.isoʳ {X} {Y} {Z} + } + } + + Systems-Monoidal : Monoidal Systems[ n ] + Systems-Monoidal = record + { ⊗ = ⊗ + ; unit = Systems-MC.unit + ; unitorˡ = unitorˡ + ; unitorʳ = unitorʳ + ; associator = associator + ; unitorˡ-commute-from = λ {f = f} → Systems-MC.unitorˡ-commute-from {f = f} + ; unitorˡ-commute-to = λ {f = f} → Systems-MC.unitorˡ-commute-to {f = f} + ; unitorʳ-commute-from = λ {f = f} → Systems-MC.unitorʳ-commute-from {f = f} + ; unitorʳ-commute-to = λ {f = f} → Systems-MC.unitorʳ-commute-to {f = f} + ; assoc-commute-from = λ {f = f} {g = g} {h = h} → Systems-MC.assoc-commute-from {f = f} {g = g} {h = h} + ; assoc-commute-to = λ {f = f} {g = g} {h = h} → Systems-MC.assoc-commute-to {f = f} {g = g} {h = h} + ; triangle = λ {X Y} → Systems-MC.triangle {X} {Y} + ; pentagon = λ {X Y Z W} → Systems-MC.pentagon {X} {Y} {Z} {W} + } + + private + + module Systems-SMC = SymmetricMonoidalCategory (Unlooped.Systems-SMC n n) + + braiding : ⊗ ≃ flip-bifunctor ⊗ + braiding = record + { F⇒G = record { Systems-SMC.braiding.⇒ } + ; F⇐G = record { Systems-SMC.braiding.⇐ } + ; iso = λ X → record { Systems-SMC.braiding.iso X } + } + + Systems-Symmetric : Symmetric Systems-Monoidal + Systems-Symmetric = record + { braided = record + { braiding = braiding + ; hexagon₁ = λ {X Y Z} → Systems-SMC.hexagon₁ {X} {Y} {Z} + ; hexagon₂ = λ {X Y Z} → Systems-SMC.hexagon₂ {X} {Y} {Z} + } + ; commutative = λ {X Y} → Systems-SMC.commutative {X} {Y} + } + + Systems-MC : MonoidalCategory (suc 0ℓ) ℓ 0ℓ + Systems-MC = record { monoidal = Systems-Monoidal } + + Systems-SMC : SymmetricMonoidalCategory (suc 0ℓ) ℓ 0ℓ + Systems-SMC = record { symmetric = Systems-Symmetric } diff --git a/Data/System/Monoidal.agda b/Data/System/Monoidal.agda index 31b6c20..731bbe5 100644 --- a/Data/System/Monoidal.agda +++ b/Data/System/Monoidal.agda @@ -3,16 +3,17 @@ open import Data.Nat using (ℕ) open import Level using (Level; suc; 0ℓ) -module Data.System.Monoidal {ℓ : Level} (n : ℕ) where +module Data.System.Monoidal {ℓ : Level} (n m : ℕ) where -open import Data.System {ℓ} using (System; Systems; _≤_; ≤-refl; ≤-trans; _≈_; discrete) +open import Data.System.Core {ℓ} using (System; _≤_; ≤-refl; ≤-trans; discrete) +open import Data.System.Category {ℓ} using (Systems[_,_]) open import Categories.Category.Monoidal using (Monoidal) open import Categories.Category.Monoidal.Symmetric using (Symmetric) open import Categories.Category.Monoidal.Bundle using (MonoidalCategory; SymmetricMonoidalCategory) open import Categories.Functor using (Functor) open import Categories.Functor.Bifunctor using (Bifunctor; flip-bifunctor) -open import Categories.Morphism (Systems n) using (_≅_; Iso) +open import Categories.Morphism (Systems[ n , m ]) using (_≅_; Iso) open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_; niHelper) open import Data.Circuit.Value using (Monoid) open import Data.Product using (_,_; _×_; uncurry′) @@ -35,11 +36,11 @@ module _ where δₛ .to v = v , v δₛ .cong v≋w = v≋w , v≋w - ⊕ₛ : Values n ×ₛ Values n ⟶ₛ Values n + ⊕ₛ : Values m ×ₛ Values m ⟶ₛ Values m ⊕ₛ .to (v , w) = v ⊕ w ⊕ₛ .cong (v₁≋v₂ , w₁≋w₂) = ⊕-cong v₁≋v₂ w₁≋w₂ -_⊗₀_ : System n → System n → System n +_⊗₀_ : System n m → System n m → System n m _⊗₀_ X Y = let open System in record { S = S X ×ₛ S Y ; fₛ = fₛ X ×-⇒ fₛ Y ∙ δₛ @@ -47,7 +48,7 @@ _⊗₀_ X Y = let open System in record } _⊗₁_ - : {A A′ B B′ : System n} + : {A A′ B B′ : System n m} (f : A ≤ A′) (g : B ≤ B′) → A ⊗₀ B ≤ A′ ⊗₀ B′ @@ -60,33 +61,33 @@ module _ where open Functor open System - ⊗ : Bifunctor (Systems n) (Systems n) (Systems n) + ⊗ : Bifunctor Systems[ n , m ] Systems[ n , m ] Systems[ n , m ] ⊗ .F₀ = uncurry′ _⊗₀_ ⊗ .F₁ = uncurry′ _⊗₁_ ⊗ .identity {X , Y} = refl (S X) , refl (S Y) ⊗ .homomorphism {_} {_} {X″ , Y″} = refl (S X″) , refl (S Y″) ⊗ .F-resp-≈ (f≈f′ , g≈g′) = f≈f′ , g≈g′ -module Unitors {X : System n} where +module Unitors {X : System n m} where open System X - ⊗-discreteˡ-≤ : discrete n ⊗₀ X ≤ X + ⊗-discreteˡ-≤ : discrete n m ⊗₀ X ≤ X ⊗-discreteˡ-≤ .⇒S = proj₂ₛ ⊗-discreteˡ-≤ .≗-fₛ i s = S.refl ⊗-discreteˡ-≤ .≗-fₒ (_ , s) = ⊕-identityˡ (fₒ′ s) - ⊗-discreteˡ-≥ : X ≤ discrete n ⊗₀ X + ⊗-discreteˡ-≥ : X ≤ discrete n m ⊗₀ X ⊗-discreteˡ-≥ .⇒S = record { to = λ s → _ , s ; cong = λ s≈s′ → _ , s≈s′ } ⊗-discreteˡ-≥ .≗-fₛ i s = _ , S.refl ⊗-discreteˡ-≥ .≗-fₒ s = ≋.sym (⊕-identityˡ (fₒ′ s)) - ⊗-discreteʳ-≤ : X ⊗₀ discrete n ≤ X + ⊗-discreteʳ-≤ : X ⊗₀ discrete n m ≤ X ⊗-discreteʳ-≤ .⇒S = proj₁ₛ ⊗-discreteʳ-≤ .≗-fₛ i s = S.refl ⊗-discreteʳ-≤ .≗-fₒ (s , _) = ⊕-identityʳ (fₒ′ s) - ⊗-discreteʳ-≥ : X ≤ X ⊗₀ discrete n + ⊗-discreteʳ-≥ : X ≤ X ⊗₀ discrete n m ⊗-discreteʳ-≥ .⇒S = record { to = λ s → s , _ ; cong = λ s≈s′ → s≈s′ , _ } ⊗-discreteʳ-≥ .≗-fₛ i s = S.refl , _ ⊗-discreteʳ-≥ .≗-fₒ s = ≋.sym (⊕-identityʳ (fₒ′ s)) @@ -94,13 +95,13 @@ module Unitors {X : System n} where open _≅_ open Iso - unitorˡ : discrete n ⊗₀ X ≅ X + unitorˡ : discrete n m ⊗₀ X ≅ X unitorˡ .from = ⊗-discreteˡ-≤ unitorˡ .to = ⊗-discreteˡ-≥ unitorˡ .iso .isoˡ = _ , S.refl unitorˡ .iso .isoʳ = S.refl - unitorʳ : X ⊗₀ discrete n ≅ X + unitorʳ : X ⊗₀ discrete n m ≅ X unitorʳ .from = ⊗-discreteʳ-≤ unitorʳ .to = ⊗-discreteʳ-≥ unitorʳ .iso .isoˡ = S.refl , _ @@ -108,7 +109,7 @@ module Unitors {X : System n} where open Unitors using (unitorˡ; unitorʳ) public -module Associator {X Y Z : System n} where +module Associator {X Y Z : System n m} where module X = System X module Y = System Y @@ -135,10 +136,10 @@ module Associator {X Y Z : System n} where open Associator using (associator) public -Systems-Monoidal : Monoidal (Systems n) +Systems-Monoidal : Monoidal Systems[ n , m ] Systems-Monoidal = let open System in record { ⊗ = ⊗ - ; unit = discrete n + ; unit = discrete n m ; unitorˡ = unitorˡ ; unitorʳ = unitorʳ ; associator = associator @@ -154,7 +155,7 @@ Systems-Monoidal = let open System in record open System -⊗-swap-≤ : {X Y : System n} → Y ⊗₀ X ≤ X ⊗₀ Y +⊗-swap-≤ : {X Y : System n m} → Y ⊗₀ X ≤ X ⊗₀ Y ⊗-swap-≤ .⇒S = swapₛ ⊗-swap-≤ {X} {Y} .≗-fₛ i (s₁ , s₂) = refl (S X) , refl (S Y) ⊗-swap-≤ {X} {Y} .≗-fₒ (s₁ , s₂) = ⊕-comm (fₒ′ Y s₁) (fₒ′ X s₂) diff --git a/Functor/Instance/Nat/System.agda b/Functor/Instance/Nat/System.agda index a3c65ca..35768f8 100644 --- a/Functor/Instance/Nat/System.agda +++ b/Functor/Instance/Nat/System.agda @@ -35,8 +35,7 @@ open import Data.Product using (_,_; _×_) open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_) open import Data.Setoid using (∣_∣) open import Data.Setoid.Unit using (⊤ₛ) -open import Data.System {suc 0ℓ} using (System; _≤_; Systemₛ; Systems; ≤-refl; ≤-trans; _≈_; discrete) -open import Data.System.Monoidal {suc 0ℓ} using (Systems-MC; Systems-SMC) +open import Data.System {suc 0ℓ} using (System; _≤_; _≈_; Systems[_,_]; ≤-refl; ≤-trans; discrete; Systems-MC; Systems-SMC) open import Data.Values Monoid using (module ≋; module Object; Values; ≋-isEquiv) open import Function using (Func; _⟶ₛ_; _⟨$⟩_; _∘_; id) open import Function.Construct.Identity using () renaming (function to Id) @@ -63,7 +62,7 @@ private opaque unfolding Valuesₘ ≋-isEquiv - map : (Fin A → Fin B) → System A → System B + map : (Fin A → Fin B) → System A A → System B B map {A} {B} f X = let open System X in record { S = S ; fₛ = fₛ ∙ arr (Pull.₁ f) @@ -73,7 +72,7 @@ opaque opaque unfolding map open System - map-≤ : (f : Fin A → Fin B) {X Y : System A} → X ≤ Y → map f X ≤ map f Y + map-≤ : (f : Fin A → Fin B) {X Y : System A A} → X ≤ Y → map f X ≤ map f Y ⇒S (map-≤ f x≤y) = ⇒S x≤y ≗-fₛ (map-≤ f x≤y) = ≗-fₛ x≤y ∘ to (arr (Pull.₁ f)) ≗-fₒ (map-≤ f x≤y) = cong (arr (Push.₁ f)) ∘ ≗-fₒ x≤y @@ -82,15 +81,15 @@ opaque unfolding map-≤ map-≤-refl : (f : Fin A → Fin B) - → {X : System A} - → map-≤ f (≤-refl {A} {X}) ≈ ≤-refl + → {X : System A A} + → map-≤ f (≤-refl {A} {A} {X}) ≈ ≤-refl map-≤-refl f {X} = Setoid.refl (S (map f X)) opaque unfolding map-≤ map-≤-trans : (f : Fin A → Fin B) - → {X Y Z : System A} + → {X Y Z : System A A} → {h : X ≤ Y} → {g : Y ≤ Z} → map-≤ f (≤-trans h g) ≈ ≤-trans (map-≤ f h) (map-≤ f g) @@ -100,13 +99,13 @@ opaque unfolding map-≤ map-≈ : (f : Fin A → Fin B) - → {X Y : System A} + → {X Y : System A A} → {g h : X ≤ Y} → h ≈ g → map-≤ f h ≈ map-≤ f g map-≈ f h≈g = h≈g -Sys₁ : (Fin A → Fin B) → Functor (Systems A) (Systems B) +Sys₁ : (Fin A → Fin B) → Functor Systems[ A , A ] Systems[ B , B ] Sys₁ {A} {B} f = record { F₀ = map f ; F₁ = λ C≤D → map-≤ f C≤D @@ -117,14 +116,14 @@ Sys₁ {A} {B} f = record opaque unfolding map - map-id-≤ : (X : System A) → map id X ≤ X + map-id-≤ : (X : System A A) → map id X ≤ X map-id-≤ X .⇒S = Id (S X) map-id-≤ X .≗-fₛ i s = cong (fₛ X) Pull.identity map-id-≤ X .≗-fₒ s = Push.identity opaque unfolding map - map-id-≥ : (X : System A) → X ≤ map id X + map-id-≥ : (X : System A A) → X ≤ map id X map-id-≥ X .⇒S = Id (S X) map-id-≥ X .≗-fₛ i s = cong (fₛ X) (≋.sym Pull.identity) map-id-≥ X .≗-fₒ s = ≋.sym Push.identity @@ -132,7 +131,7 @@ opaque opaque unfolding map-≤ map-id-≤ map-id-comm - : {X Y : System A} + : {X Y : System A A} (f : X ≤ Y) → ≤-trans (map-≤ id f) (map-id-≤ Y) ≈ ≤-trans (map-id-≤ X) f map-id-comm {Y} f = Setoid.refl (S Y) @@ -142,12 +141,12 @@ opaque unfolding map-id-≤ map-id-≥ map-id-isoˡ - : (X : System A) + : (X : System A A) → ≤-trans (map-id-≤ X) (map-id-≥ X) ≈ ≤-refl map-id-isoˡ X = Setoid.refl (S X) map-id-isoʳ - : (X : System A) + : (X : System A A) → ≤-trans (map-id-≥ X) (map-id-≤ X) ≈ ≤-refl map-id-isoʳ X = Setoid.refl (S X) @@ -167,7 +166,7 @@ opaque map-∘-≤ : (f : Fin A → Fin B) (g : Fin B → Fin C) - (X : System A) + (X : System A A) → map (g ∘ f) X ≤ map g (map f X) map-∘-≤ f g X .⇒S = Id (S X) map-∘-≤ f g X .≗-fₛ i s = cong (fₛ X) Pull.homomorphism @@ -178,7 +177,7 @@ opaque map-∘-≥ : (f : Fin A → Fin B) (g : Fin B → Fin C) - (X : System A) + (X : System A A) → map g (map f X) ≤ map (g ∘ f) X map-∘-≥ f g X .⇒S = Id (S X) map-∘-≥ f g X .≗-fₛ i s = cong (fₛ X) (≋.sym Pull.homomorphism) @@ -203,12 +202,12 @@ Sys-homo {A} f g = niHelper record map-∘-comm : (f : Fin A → Fin B) (g : Fin B → Fin C) - → {X Y : System A} + → {X Y : System A A} (X≤Y : X ≤ Y) → ≤-trans (map-≤ (g ∘ f) X≤Y) (map-∘-≤ f g Y) ≈ ≤-trans (map-∘-≤ f g X) (map-≤ g (map-≤ f X≤Y)) map-∘-comm f g {Y} X≤Y = Setoid.refl (S Y) - module _ (X : System A) where + module _ (X : System A A) where opaque unfolding map-∘-≤ map-∘-≥ isoˡ : ≤-trans (map-∘-≤ f g X) (map-∘-≥ f g X) ≈ ≤-refl @@ -216,8 +215,7 @@ Sys-homo {A} f g = niHelper record isoʳ : ≤-trans (map-∘-≥ f g X) (map-∘-≤ f g X) ≈ ≤-refl isoʳ = Setoid.refl (S X) - -module _ {f g : Fin A → Fin B} (f≗g : f ≗ g) (X : System A) where +module _ {f g : Fin A → Fin B} (f≗g : f ≗ g) (X : System A A) where opaque @@ -238,7 +236,7 @@ opaque map-cong-comm : {f g : Fin A → Fin B} (f≗g : f ≗ g) - {X Y : System A} + {X Y : System A A} (h : X ≤ Y) → ≤-trans (map-≤ f h) (map-cong-≤ f≗g Y) ≈ ≤-trans (map-cong-≤ f≗g X) (map-≤ g h) @@ -251,14 +249,14 @@ opaque map-cong-isoˡ : {f g : Fin A → Fin B} (f≗g : f ≗ g) - (X : System A) + (X : System A A) → ≤-trans (map-cong-≤ f≗g X) (map-cong-≥ f≗g X) ≈ ≤-refl map-cong-isoˡ f≗g X = Setoid.refl (S X) map-cong-isoʳ : {f g : Fin A → Fin B} (f≗g : f ≗ g) - (X : System A) + (X : System A A) → ≤-trans (map-cong-≥ f≗g X) (map-cong-≤ f≗g X) ≈ ≤-refl map-cong-isoʳ f≗g X = Setoid.refl (S X) @@ -276,7 +274,7 @@ Sys-resp-≈ f≗g = niHelper record module NatCat where Sys : Functor Nat (Cats (suc 0ℓ) (suc 0ℓ) 0ℓ) - Sys .F₀ = Systems + Sys .F₀ n = Systems[ n , n ] Sys .F₁ = Sys₁ Sys .identity = Sys-identity Sys .homomorphism = Sys-homo _ _ @@ -288,15 +286,15 @@ module NatMC where module _ (f : Fin A → Fin B) where - module A = System-⊗ A - module B = System-⊗ B + module A = System-⊗ A A + module B = System-⊗ B B open CommutativeMonoid⇒ (Push.₁ f) - open Morphism (Systems B) using (_≅_) + open Morphism Systems[ B , B ] using (_≅_) opaque unfolding map - ε-≅ : discrete B ≅ map f (discrete A) + ε-≅ : discrete B B ≅ map f (discrete A A) ε-≅ = record -- other fields can be inferred { from = record @@ -337,7 +335,7 @@ module NatMC where module A-MC = MonoidalCategory A.Systems-MC module B-MC = MonoidalCategory B.Systems-MC - F : Functor (Systems A) (Systems B) + F : Functor Systems[ A , A ] Systems[ B , B ] F = Sys₁ f module F = Functor F @@ -349,7 +347,7 @@ module NatMC where unfolding ⊗-homo-≃ associativity - : {X Y Z : System A} + : {X Y Z : System A A} → F.₁ A.Associator.assoc-≤ ∘′ ⊗-homo-≃.⇒.η (X A.⊗₀ Y , Z) ∘′ ⊗-homo-≃.⇒.η (X , Y) B.⊗₁ B-MC.id @@ -359,7 +357,7 @@ module NatMC where associativity {X} {Y} {Z} = Setoid.refl (S X ×ₛ (S Y ×ₛ S Z)) unitaryˡ - : {X : System A} + : {X : System A A} → F.₁ A.Unitors.⊗-discreteˡ-≤ ∘′ ⊗-homo-≃.⇒.η (A-MC.unit , X) ∘′ ε-≅.from B.⊗₁ B-MC.id @@ -367,14 +365,14 @@ module NatMC where unitaryˡ {X} = Setoid.refl (S X) unitaryʳ - : {X : System A} + : {X : System A A} → F.₁ A.Unitors.⊗-discreteʳ-≤ - ∘′ ⊗-homo-≃.⇒.η (X , discrete A) + ∘′ ⊗-homo-≃.⇒.η (X , discrete A A) ∘′ B-MC.id B.⊗₁ ε-≅.from B-MC.≈ B-MC.unitorʳ.from unitaryʳ {X} = Setoid.refl (S X) - Sys-MC₁ : StrongMonoidalFunctor (Systems-MC A) (Systems-MC B) + Sys-MC₁ : StrongMonoidalFunctor (Systems-MC A A) (Systems-MC B B) Sys-MC₁ = record { F = Sys₁ f ; isStrongMonoidal = record @@ -388,7 +386,7 @@ module NatMC where opaque unfolding map-id-≤ ⊗-homo-≃ - Sys-MC-identity : MonoidalNaturalIsomorphism (Sys-MC₁ id) (idF-StrongMonoidal (Systems-MC A)) + Sys-MC-identity : MonoidalNaturalIsomorphism (Sys-MC₁ id) (idF-StrongMonoidal (Systems-MC A A)) Sys-MC-identity = record { U = NatCat.Sys.identity ; F⇒G-isMonoidal = record @@ -426,7 +424,7 @@ module NatMC where } Sys : Functor Nat (StrongMonoidals (suc 0ℓ) (suc 0ℓ) 0ℓ) - Sys .F₀ = Systems-MC + Sys .F₀ n = Systems-MC n n Sys .F₁ = Sys-MC₁ Sys .identity = Sys-MC-identity Sys .homomorphism = Sys-MC-homomorphism @@ -440,29 +438,29 @@ module NatSMC where private - module A = System-⊗ A - module B = System-⊗ B + module A = System-⊗ A A + module B = System-⊗ B B module A-SMC = SymmetricMonoidalCategory A.Systems-SMC module B-SMC = SymmetricMonoidalCategory B.Systems-SMC - F : Functor (Systems A) (Systems B) + F : Functor Systems[ A , A ] Systems[ B , B ] F = Sys₁ f module F = Functor F - F-MF : StrongMonoidalFunctor (Systems-MC A) (Systems-MC B) + F-MF : StrongMonoidalFunctor (Systems-MC A A) (Systems-MC B B) F-MF = NatMC.Sys.₁ f module F-MF = StrongMonoidalFunctor F-MF opaque unfolding NatMC.⊗-homo-≃ σ-compat - : {X Y : System A} + : {X Y : System A A} → F.₁ (A-SMC.braiding.⇒.η (X , Y)) B-SMC.∘ F-MF.⊗-homo.⇒.η (X , Y) B-SMC.≈ F-MF.⊗-homo.⇒.η (Y , X) B-SMC.∘ B-SMC.braiding.⇒.η (F.₀ X , F.₀ Y) σ-compat {X} {Y} = Setoid.refl (S Y ×ₛ S X) - Sys-SMC₁ : SymmetricMonoidalFunctor (Systems-SMC A) (Systems-SMC B) + Sys-SMC₁ : SymmetricMonoidalFunctor (Systems-SMC A A) (Systems-SMC B B) Sys-SMC₁ = record { F-MF ; isBraidedMonoidal = record @@ -471,7 +469,7 @@ module NatSMC where } } - Sys-SMC-identity : SymmetricMonoidalNaturalIsomorphism (Sys-SMC₁ id) (idF-StrongSymmetricMonoidal (Systems-SMC A)) + Sys-SMC-identity : SymmetricMonoidalNaturalIsomorphism (Sys-SMC₁ id) (idF-StrongSymmetricMonoidal (Systems-SMC A A)) Sys-SMC-identity = record { MonoidalNaturalIsomorphism NatMC.Sys.identity } Sys-SMC-homomorphism @@ -487,7 +485,7 @@ module NatSMC where Sys-SMC-resp-≈ f≗g = record { MonoidalNaturalIsomorphism (NatMC.Sys.F-resp-≈ f≗g) } Sys : Functor Nat (SymMonCat {suc 0ℓ} {suc 0ℓ} {0ℓ}) - Sys .F₀ = Systems-SMC + Sys .F₀ n = Systems-SMC n n Sys .F₁ = Sys-SMC₁ Sys .identity = Sys-SMC-identity Sys .homomorphism = Sys-SMC-homomorphism diff --git a/NaturalTransformation/Instance/GateSemantics.agda b/NaturalTransformation/Instance/GateSemantics.agda index c85526c..9cdbc1b 100644 --- a/NaturalTransformation/Instance/GateSemantics.agda +++ b/NaturalTransformation/Instance/GateSemantics.agda @@ -44,12 +44,12 @@ opaque unfolding Values - 1-cell : Value → System 1 + 1-cell : Value → System 1 1 1-cell x .S = ⊤ₛ 1-cell x .fₛ = Const (Values 1) (⊤ₛ ⇒ₛ ⊤ₛ) (Id ⊤ₛ) 1-cell x .fₒ = Const ⊤ₛ (Values 1) λ { 0F → x } - 2-cell : (Value → Value) → System 2 + 2-cell : (Value → Value) → System 2 2 2-cell f .S = Valueₛ 2-cell f .fₛ .to x = Const Valueₛ Valueₛ (f (x (# 0))) 2-cell f .fₛ .cong x = ≡.cong f (x (# 0)) @@ -58,7 +58,7 @@ opaque 2-cell f .fₒ .cong _ 0F = ≡.refl 2-cell f .fₒ .cong x 1F = x - 3-cell : (Value → Value → Value) → System 3 + 3-cell : (Value → Value → Value) → System 3 3 3-cell f .S = Valueₛ 3-cell f .fₛ .to i = Const Valueₛ Valueₛ (f (i (# 0)) (i (# 1))) 3-cell f .fₛ .cong ≡i = ≡.cong₂ f (≡i (# 0)) (≡i (# 1)) @@ -125,7 +125,7 @@ module _ where open Belnap open Gate - system-of-gate : {n : ℕ} → Gate n → System n + system-of-gate : {n : ℕ} → Gate n → System n n system-of-gate ZERO = 1-cell true system-of-gate ONE = 1-cell false system-of-gate ID = 2-cell id @@ -147,7 +147,7 @@ private open EGate hiding (Edge) -system-of-edge : {n : ℕ} → ∣ Edge.₀ n ∣ → System n +system-of-edge : {n : ℕ} → ∣ Edge.₀ n ∣ → System n n system-of-edge (mkEdge gate ports) = U.₁ (Sys.₁ ports) ⟨$⟩ system-of-gate gate system-of-edgeₛ : (n : ℕ) → Edge.₀ n ⟶ₛ U.₀ (Sys.₀ n) |