1 files changed, 83 insertions, 0 deletions
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
+      }