blob: 1fd86d6ac398f3ea548f17f26ab5ec05152f21c6 (
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
84
85
86
87
88
|
{-# OPTIONS --without-K --safe #-}
open import Level using (Level; suc; _⊔_)
module Data.System.Looped {c ℓ : Level} where
import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
open import Algebra using (CommutativeMonoid)
open import Categories.Category using (Category)
open import Categories.Category.Helper using (categoryHelper)
open import Categories.Functor using (Functor)
open import Data.System.Category using (Systems[_,_])
open import Data.System.Core using (System; _≤_)
open import Function using (Func; _⟨$⟩_) renaming (id to idf)
open import Relation.Binary using (Setoid)
open Func
open System
private
module _ {V : CommutativeMonoid c ℓ} where
open CommutativeMonoid V
loop : System setoid V → System setoid V
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)
}
; fₒ = X.fₒ
}
where
module X = System X
loop-≤ : {A B : System setoid V} → 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
module _ (V : CommutativeMonoid c ℓ) where
open CommutativeMonoid V using (setoid)
Loop : Functor Systems[ setoid , V ] Systems[ setoid , V ]
Loop = record
{ F₀ = loop
; F₁ = loop-≤
; identity = λ {A} → Setoid.refl (S A)
; homomorphism = λ {Z = Z} → Setoid.refl (S Z)
; F-resp-≈ = idf
}
open Category Systems[ setoid , V ]
open Functor Loop
Systems[_] : Category (c ⊔ suc ℓ) (c ⊔ ℓ) ℓ
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
}
|
