structure Edge (es : EventStructure) : Type

An edge in the configuration graph of an event structure: from configuration c₁ to configuration c₂ by adding event e.

• conf₁ : Conf es
• conf₂ : Conf es
• event : es.Event
• conf₁_enables : Configuration.enables es (↑self.conf₁) self.event
• conf₂_equals : ↑self.conf₂ = ↑self.conf₁ ∪ {self.event}

inductive Path (es : EventStructure) : Conf es → Conf es → Type

A path in the configuration graph of an event structure.

• refl {es : EventStructure} {c : Conf es} : Path es c c
• step {es : EventStructure} {c₁ c₂ c₃ : Conf es} (hEdge : Edge es) (hPath : Path es c₂ c₃) : Path es c₁ c₃

def Path.path_id (es : EventStructure) (c : Conf es) : Path es c c

Identity path.

Equations

• Path.path_id es c = Path.refl

def Path.path_comp (es : EventStructure) {c₁ c₂ c₃ : Conf es} (h₁₂ : Path es c₁ c₂) (h₂₃ : Path es c₂ c₃) : Path es c₁ c₃

Composition of paths.

Equations

• Path.path_comp es Path.refl h₂₃_2 = h₂₃_2
• Path.path_comp es (Path.step hEdge hPath) h₂₃ = Path.step hEdge (Path.path_comp es hPath h₂₃)

theorem Path.path_comp_id (es : EventStructure) {c₁ c₂ : Conf es} (h : Path es c₁ c₂) : path_comp es h (path_id es c₂) = h

Left identity law: composing with the identity path on the right.

theorem Path.path_id_comp (es : EventStructure) {c₁ c₂ : Conf es} (h : Path es c₁ c₂) : path_comp es (path_id es c₁) h = h

Right identity law: composing with the identity path on the left.

theorem Path.path_comp_assoc (es : EventStructure) {c₁ c₂ c₃ c₄ : Conf es} (h₁₂ : Path es c₁ c₂) (h₂₃ : Path es c₂ c₃) (h₃₄ : Path es c₃ c₄) : path_comp es (path_comp es h₁₂ h₂₃) h₃₄ = path_comp es h₁₂ (path_comp es h₂₃ h₃₄)

Associativity law: composition of paths is associative.

def Path.trace (es : EventStructure) {c₁ c₂ : Conf es} (hPath : Path es c₁ c₂) : List es.Event

Trace of the path

Equations

• Path.trace es Path.refl = []
• Path.trace es (Path.step hEdge hPath') = hEdge.event :: Path.trace es hPath'

instance Path.pathSetoid (es : EventStructure) (c₁ c₂ : Conf es) : Setoid (Path es c₁ c₂)

Path equivalence is the kernel of the trace function.

Equations

• Path.pathSetoid es c₁ c₂ = Setoid.ker (Path.trace es)

def Path.PathEquiv (es : EventStructure) {c₁ c₂ : Conf es} (p₁ p₂ : Path es c₁ c₂) : Prop

Two paths are equivalent if their traces are trace equivalent

Equations

• Path.PathEquiv es p₁ p₂ = (Path.pathSetoid es c₁ c₂) p₁ p₂

theorem Path.pathEquiv_refl (es : EventStructure) {c₁ c₂ : Conf es} : Reflexive (PathEquiv es)

Path equivalence is reflexive.

theorem Path.pathEquiv_symm (es : EventStructure) {c₁ c₂ : Conf es} : Symmetric (PathEquiv es)

Path equivalence is symmetric.

theorem Path.pathEquiv_trans (es : EventStructure) {c₁ c₂ : Conf es} : Transitive (PathEquiv es)

Path equivalence is transitive.

theorem Path.trace_comp (es : EventStructure) {c₁ c₂ c₃ : Conf es} (p₁₂ : Path es c₁ c₂) (p₂₃ : Path es c₂ c₃) : trace es (path_comp es p₁₂ p₂₃) = trace es p₁₂ ++ trace es p₂₃

Trace of path composition is concatenation of traces.

def Path.Async (es : EventStructure) (c₁ c₂ : Conf es) : Type

Asynchronous path: paths quotiented by path equivalence.

Equations

• Path.Async es c₁ c₂ = Quotient (Path.pathSetoid es c₁ c₂)

def Path.Async.mk (es : EventStructure) {c₁ c₂ : Conf es} (p : Path es c₁ c₂) : Async es c₁ c₂

Lift a path to an asynchronous path.

Equations

• Path.Async.mk es p = ⟦p⟧

def Path.Async.async_path_id (es : EventStructure) (c : Conf es) : Async es c c

Identity asynchronous path.

Equations

• Path.Async.async_path_id es c = Path.Async.mk es (Path.path_id es c)

def Path.Async.async_path_comp (es : EventStructure) {c₁ c₂ c₃ : Conf es} (p₁₂ : Async es c₁ c₂) (p₂₃ : Async es c₂ c₃) : Async es c₁ c₃

Composition of asynchronous paths.

Equations

• Path.Async.async_path_comp es p₁₂ p₂₃ = Quotient.lift₂ (fun (p₁₂ : Path es c₁ c₂) (p₂₃ : Path es c₂ c₃) => Path.Async.mk es (Path.path_comp es p₁₂ p₂₃)) ⋯ p₁₂ p₂₃

theorem Path.Async.async_path_id_comp (es : EventStructure) {c₁ c₂ : Conf es} (p : Async es c₁ c₂) : async_path_comp es (async_path_id es c₁) p = p

Left identity law for asynchronous path composition.

theorem Path.Async.async_path_comp_id (es : EventStructure) {c₁ c₂ : Conf es} (p : Async es c₁ c₂) : async_path_comp es p (async_path_id es c₂) = p

Right identity law for asynchronous path composition.

theorem Path.Async.assoc (es : EventStructure) {c₁ c₂ c₃ c₄ : Conf es} (p₁₂ : Async es c₁ c₂) (p₂₃ : Async es c₂ c₃) (p₃₄ : Async es c₃ c₄) : async_path_comp es (async_path_comp es p₁₂ p₂₃) p₃₄ = async_path_comp es p₁₂ (async_path_comp es p₂₃ p₃₄)

Associativity law for asynchronous path composition.

instance pathCategory (es : EventStructure) : CategoryTheory.Category.{0, 0} (Conf es)

The path category of an event structure.

Equations

• pathCategory es = { Hom := Path es, id := Path.path_id es, comp := fun {X Y Z : Conf es} => Path.path_comp es, id_comp := ⋯, comp_id := ⋯, assoc := ⋯ }

instance asyncPathCategory (es : EventStructure) : CategoryTheory.Category.{0, 0} (Conf es)

The asynchronous path category of an event structure.

Equations

• asyncPathCategory es = { Hom := Path.Async es, id := Path.Async.async_path_id es, comp := fun {X Y Z : Conf es} => Path.Async.async_path_comp es, id_comp := ⋯, comp_id := ⋯, assoc := ⋯ }