1 files changed, 63 insertions, 0 deletions
diff --git a/Data/System/Category.agda b/Data/System/Category.agda
new file mode 100644
index 0000000..171a003
--- /dev/null
+++ b/Data/System/Category.agda
@@ -0,0 +1,63 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Level using (Level; 0ℓ; suc)
+
+module Data.System.Category {ℓ : Level} where
+
+import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
+
+open import Categories.Category using (Category)
+open import Data.Nat using (ℕ)
+open import Data.System.Core {ℓ} using (System; _≤_; ≤-trans; ≤-refl)
+open import Data.Setoid using (_⇒ₛ_)
+open import Function using (Func; _⟨$⟩_; flip)
+open import Relation.Binary as Rel using (Setoid; Rel)
+
+open Func
+open System
+open _≤_
+
+private module ≈ {n m : ℕ} where
+
+  private
+    variable
+      A B C : System n m
+
+  _≈_ : Rel (A ≤ B) 0ℓ
+  _≈_ {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[_,_] : ℕ → ℕ → Category (suc 0ℓ) ℓ 0ℓ
+Systems[ n , m ] = record
+    { Obj = System n m
+    ; _⇒_ = _≤_
+    ; _≈_ = _≈_
+    ; 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}
+    }