blob: f69d75b093b35935a5bd7f55b33e81793ade2d86 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
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
}
|
