Owner-based local syntax builders

This module provides a small derived API for building Spec.SyntaxOver objects from two ingredients:

• an owner function saying which agent controls a node;
• a participant-local LocalView describing what that agent stores when it owns the node versus when it merely observes someone else's move.

This does not replace SyntaxOver or InteractionOver. It is only a structured way to construct common owner-driven interaction patterns on top of the generic core.

In particular, this layer is useful for two-party and multiparty interaction models where every node has one acting party and the other parties follow the chosen move with their passive continuations.

structure Interaction.Spec.Ownership.LocalView (X : Type u) : Type (u + 1)

LocalView X is the local participant interface at one move space X.

It separates the node shape seen by an agent when that agent owns the node from the node shape seen when someone else owns the node.

The owned shape is intentionally unconstrained here. In particular, the common base owned-node form m ((x : X) × Cont x) is just one important specialization of LocalView, not a hard-coded part of the generic syntax core.

• own : (X → Type u) → Type u

  The node representation used when the agent owns the current node.

• other : (X → Type u) → Type u

  The node representation used when some other agent owns the current node.

structure Interaction.Spec.Ownership.LocalRunner (m : Type u → Type u) {X : Type u} (V : LocalView X) : Type (u + 1)

LocalRunner m V gives the operational interpretation of a local view V inside an ambient monad m.

It explains:

• how an owned node produces the chosen move together with the matching continuation;
• how a passive node follows a move chosen elsewhere.

• runOwn {Cont : X → Type u} : V.own Cont → m ((x : X) × Cont x)

  Execute an owned node, producing the chosen move and continuation.

• runOther {Cont : X → Type u} : V.other Cont → (x : X) → m (Cont x)

  Execute a passive node after the owner has chosen move x.

def Interaction.Spec.Ownership.syntaxOver {Agent : Type a} {Γ : Node.Context} [DecidableEq Agent] (owner : {X : Type u_1} → Γ X → Agent) (view : {X : Type u_1} → Γ X → Agent → LocalView X) : SyntaxOver Agent Γ

Build a SyntaxOver from an owner function and participant-local views.

If owner γ = a, then agent a uses its own shape at context γ, while every other agent uses its other shape there.