feat: define the category of LTSs

Cslib.lean

@@ -62,6 +62,7 @@ public import Cslib.Foundations.Semantics.FLTS.LTSToFLTS
 public import Cslib.Foundations.Semantics.FLTS.Prod
 public import Cslib.Foundations.Semantics.LTS.Basic
 public import Cslib.Foundations.Semantics.LTS.Bisimulation
+public import Cslib.Foundations.Semantics.LTS.LTSCat.Basic
 public import Cslib.Foundations.Semantics.LTS.Simulation
 public import Cslib.Foundations.Semantics.LTS.TraceEq
 public import Cslib.Foundations.Syntax.Congruence

Cslib/Foundations/Semantics/LTS/LTSCat/Basic.lean

@@ -0,0 +1,99 @@
+/-
+Copyright (c) 2026 Ayberk Tosun (Zeroth Research). All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Ayberk Tosun
+-/
+
+module
+
+public import Mathlib.CategoryTheory.Category.Basic
+public import Cslib.Foundations.Semantics.LTS.Basic
+public import Mathlib.Control.Basic
+
+@[expose] public section
+
+namespace Cslib
+
+variable {State Label : Type*}
+
+/-! # Category of Labelled Transition Systems
+
+This file contains the definition of the category of labelled transition systems
+as defined in Winskel and Nielsen's handbook chapter [WinskelNielsen1995].
+
+## References
+
+* [N. Winskel and M. Nielsen, *Models for concurrency*][WinskelNielsen1995]
+-/
+
+/--
+We first define what is denoted Tran* in [WinskelNielsen1995]: the extension of
+a transition relation with idle transitions.
+-/
+def LTS.lift (trans : State → Label → State → Prop) : State → (Option Label) → State → Prop :=
+  fun s l s' => l.elim (s = s') (trans s · s')
+
+/-! ## LTSs and LTS morphisms form a category -/
+
+/--
+The definition of labelled transition system (with the type of states and the
+type of labels as part of the structure).
+-/
+@[nolint checkUnivs]
+structure LTSCat : Type (max u v + 1) where
+  /-- Type of states of an LTS -/
+  State : Type u
+  /-- Type of labels of an LTS -/
+  Label : Type v
+  /-- Transition relation of an LTS -/
+  lts : LTS State Label
+
+/--
+A morphism between two labelled transition systems consists of (1) a function on
+states, (2) a partial function on labels, and a proof that (1) preserves each
+transition along (2).
+-/
+structure LTS.Morphism (lts₁ lts₂ : LTSCat) : Type where
+  /-- Mapping of states of `lts₁` to states of `lts₂` -/
+  stateMap : lts₁.State → lts₂.State
+  /-- Mapping of labels of `lts₁` to labels of `lts₂` -/
+  labelMap : lts₁.Label → Option lts₂.Label
+  /-- Stipulation that `stateMap` preserve transitions -/
+  labelMap_tr (s s' : lts₁.State) (l : lts₁.Label) :
+    lts₁.lts.Tr s l s' → lift lts₂.lts.Tr (stateMap s) (labelMap l) (stateMap s')
+
+/-- The identity LTS morphism. -/
+def LTS.Morphism.id (lts : LTSCat) : LTS.Morphism lts lts where
+  stateMap := _root_.id
+  labelMap := pure
+  labelMap_tr _ _ _ := _root_.id
+
+/-- Composition of LTS morphisms.
+
+We use Kleisli composition to define this.
+-/
+def LTS.Morphism.comp {lts₁ lts₂ lts₃} (f : LTS.Morphism lts₁ lts₂) (g : LTS.Morphism lts₂ lts₃) :
+    LTS.Morphism lts₁ lts₃ where
+  stateMap := g.stateMap ∘ f.stateMap
+  labelMap := f.labelMap >=> g.labelMap
+  labelMap_tr s s' l h := by
+    obtain ⟨f, μ, p⟩ := f
+    obtain ⟨g, ν, q⟩ := g
+    change ((μ l).bind ν).elim (g (f s) = g (f s')) _
+    cases hμ : μ l with grind [lift]
+
+/-- Finally, we prove that these form a category. -/
+instance : CategoryTheory.Category LTSCat where
+  Hom := LTS.Morphism
+  id := LTS.Morphism.id
+  comp := LTS.Morphism.comp
+  comp_id _ := by
+    simp only [LTS.Morphism.comp, LTS.Morphism.id]
+    congr 1
+    rw [fish_pure]
+  assoc _ _ _ := by
+    simp only [LTS.Morphism.comp]
+    congr 1
+    rw [fish_assoc]
+
+end Cslib

references.bib

@@ -264,3 +264,16 @@ @article{         ShepherdsonSturgis1963
   publisher    = {Association for Computing Machinery},
   address      = {New York, NY, USA}
 }
+
+@incollection{WinskelNielsen1995,
+  author       = {Winskel, Glynn and Nielsen, Mogens},
+  isbn         = {9780198537809},
+  title        = {Models for concurrency},
+  booktitle    = {Handbook of Logic in Computer Science},
+  publisher    = {Oxford University Press},
+  year         = {1995},
+  month        = {05},
+  doi          = {10.1093/oso/9780198537809.003.0001},
+  url          = {https://doi.org/10.1093/oso/9780198537809.003.0001},
+  eprint       = {https://academic.oup.com/book/0/chapter/421962123/chapter-pdf/52352653/isbn-9780198537809-book-part-1.pdf},
+}