blob: 50d950ba8c89c2c49c93f6fb838732b6495a9148 (
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
|
{-# 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 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}
}
|
