blob: 7e0b79127bb8a2995d3f0203f124945c4387ca11 (
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
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
|
{-# OPTIONS --without-K --safe #-}
open import Level using (Level; suc; _⊔_)
module Data.System.Category {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.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)
open Func
open System
open _≤_
private module ≈ {I : Setoid c ℓ} {O : CommutativeMonoid c ℓ} where
private
variable
A B C : System I O
_≈_ : Rel (A ≤ B) ℓ
_≈_ {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[_,_] : Setoid c ℓ → CommutativeMonoid c ℓ → Category (c ⊔ suc ℓ) (c ⊔ ℓ) ℓ
Systems[ I , O ] = record
{ Obj = System I O
; _⇒_ = _≤_
; _≈_ = _≈_
; 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}
}
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 }
}
|
