Add monoidal structure to system functor

1 files changed, 56 insertions, 0 deletions

diff --git a/Data/System/Category.agda b/Data/System/Category.agda
index 50d950b..7e0b791 100644
--- a/Data/System/Category.agda
+++ b/Data/System/Category.agda
@@ -8,7 +8,10 @@ import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
 
 open import Algebra using (CommutativeMonoid)
 open import Categories.Category using (Category)
+open import Categories.Category.Instance.Setoids using (Setoids)
+open import Categories.Morphism using () renaming (_≅_ to _[_≅_])
 open import Data.Setoid using (_⇒ₛ_)
+open import Data.Setoid using (∣_∣)
 open import Data.System.Core using (System; _≤_; ≤-trans; ≤-refl)
 open import Function using (Func; _⟨$⟩_; flip)
 open import Relation.Binary as Rel using (Setoid; Rel)
@@ -61,3 +64,56 @@ Systems[ I , O ] = record
     ; equiv = ≈-isEquiv
     ; ∘-resp-≈ = λ {f = f} {h} {g} {i} → ≤-resp-≈ {f = f} {h} {g} {i}
     }
+
+module _
+    {I : Setoid c ℓ}
+    {O : CommutativeMonoid c ℓ}
+    {A B : System I O}
+    (let private module A = System A)
+    (let private module B = System B)
+    (≅S : Setoids ℓ ℓ [ A.S ≅ B.S ])
+    (let private module O = CommutativeMonoid O)
+    (let private module ≅S = _[_≅_] ≅S)
+    (≗-fₛ : (i : ∣ I ∣) (s : ∣ A.S ∣) → ≅S.from ⟨$⟩ (A.fₛ′ i s) B.S.≈ B.fₛ′ i (≅S.from ⟨$⟩ s))
+    (≗-fₒ : (s : ∣ A.S ∣) → (A.fₒ′ s) O.≈ B.fₒ′ (≅S.from ⟨$⟩ s))
+  where
+
+  private
+
+    ≗-fₛ-≥ : ((i : ∣ I ∣) (s : ∣ B.S ∣) → ≅S.to ⟨$⟩ (B.fₛ′ i s) A.S.≈ A.fₛ′ i (≅S.to ⟨$⟩ s))
+    ≗-fₛ-≥  i s = begin
+        ≅S.to ⟨$⟩ (B.fₛ′ i s)                           ≈⟨ cong ≅S.to (cong (B.fₛ ⟨$⟩ i) ≅S.isoʳ) ⟨
+        ≅S.to ⟨$⟩ (B.fₛ′ i (≅S.from ⟨$⟩ (≅S.to ⟨$⟩ s))) ≈⟨ cong ≅S.to (≗-fₛ i (≅S.to ⟨$⟩ s)) ⟨
+        ≅S.to ⟨$⟩ (≅S.from ⟨$⟩ (A.fₛ′ i (≅S.to ⟨$⟩ s))) ≈⟨ ≅S.isoˡ ⟩
+        A.fₛ′ i (≅S.to ⟨$⟩ s)                           ∎
+      where
+        open ≈-Reasoning A.S
+
+    ≗-fₒ-≥ : (s : ∣ B.S ∣) → B.fₒ′ s O.≈ A.fₒ′ (≅S.to ⟨$⟩ s)
+    ≗-fₒ-≥ s = begin
+        B.fₒ′ s                           ≈⟨ cong B.fₒ ≅S.isoʳ ⟨
+        B.fₒ′ (≅S.from ⟨$⟩ (≅S.to ⟨$⟩ s)) ≈⟨ ≗-fₒ (≅S.to ⟨$⟩ s) ⟨
+        A.fₒ′ (≅S.to ⟨$⟩ s)               ∎
+      where
+        open ≈-Reasoning O.setoid
+
+    A≤B : A ≤ B
+    A≤B = record
+        { ⇒S = ≅S.from
+        ; ≗-fₛ = ≗-fₛ
+        ; ≗-fₒ = ≗-fₒ
+        }
+
+    B≤A : B ≤ A
+    B≤A = record
+        { ⇒S = ≅S.to
+        ; ≗-fₛ = ≗-fₛ-≥
+        ; ≗-fₒ = ≗-fₒ-≥
+        }
+
+  mk-≅ : Systems[ I , O ] [ A ≅ B ]
+  mk-≅ = record
+      { from = A≤B
+      ; to = B≤A
+      ; iso = record { ≅S }
+      }