Functorial local syntax over interaction trees

This file introduces the functorial refinement of the local syntax core.

SyntaxOver in Basic/Syntax is the most general local syntax object: it describes which node object an agent has at one protocol node, with no assumption that recursive continuations can be reindexed generically.

ShapeOver is the functorial refinement of that base notion: it equips a SyntaxOver with a continuation map. This is exactly the extra structure needed to define generic output transport such as ShapeOver.mapOutput.

Many important interaction objects are syntax without being shapes in this sense: if recursive continuations are hidden under an opaque outer constructor, then a generic continuation map may not exist. This is why SyntaxOver is the semantic base layer, while ShapeOver is the stronger interface used when continuations are exposed functorially enough.

Naming note: ShapeOver keeps the suffix form because it is the primary functorial refinement of syntax, with plain Shape recovered as the trivial-context specialization. This differs from Decoration.Over, which is literally dependent data over a fixed base decoration value.

structure Interaction.ShapeOver {P : PFunctor.{uA, uB}} {Q : PFunctor.{uA₂, uB₂}} (l : P.Lens Q) (Agent : Type a) (Γ : P.A → Type vΓ) extends Interaction.SyntaxOver l Agent Γ : Type (max (max (max (max a uA) uB₂) vΓ) (w + 1))

ShapeOver l Agent Γ is functorial local syntax over an arbitrary control polynomial executed through a runtime lens l.

It refines SyntaxOver l Agent Γ with a node-level continuation map. At a control position pos : P.A, recursive continuations are indexed by runtime directions Q.B (l.toFunA pos), and the lens determines which control child each runtime direction selects.

• Node (agent : Agent) (pos : P.A) (γ : Γ pos) : (Q.B (l.toFunA pos) → Type w) → Type w
• map {agent : Agent} {pos : P.A} {γ : Γ pos} {A B : Q.B (l.toFunA pos) → Type w} : ((d : Q.B (l.toFunA pos)) → A d → B d) → self.Node agent pos γ A → self.Node agent pos γ B

  Transform the recursive continuation payload of one local node object. The agent, control position, node-local context, and runtime move shape are unchanged.

@[implicit_reducible]

instance Interaction.ShapeOver.instCoeSyntaxOver {P : PFunctor.{uA, uB}} {Q : PFunctor.{uA₂, uB₂}} {l : P.Lens Q} {Agent : Type a} {Γ : P.A → Type vΓ} : Coe (ShapeOver l Agent Γ) (SyntaxOver l Agent Γ)

def Interaction.ShapeOver.forAgent {P : PFunctor.{uA, uB}} {Q : PFunctor.{uA₂, uB₂}} {l : P.Lens Q} {Agent : Type a} {Γ : P.A → Type vΓ} (shape : ShapeOver l Agent Γ) (agent : Agent) : ShapeOver l PUnit.{u_2 + 1} Γ

Restrict a participant-indexed shape to one fixed agent.

The resulting singleton-agent shape has the same node objects and continuation map as shape at agent; the dummy PUnit agent argument is ignored.

def Interaction.ShapeOver.comap {P : PFunctor.{uA, uB}} {Q : PFunctor.{uA₂, uB₂}} {l : P.Lens Q} {Agent : Type a} {Γ : P.A → Type vΓ} {Δ : P.A → Type vΔ} (f : (pos : P.A) → Γ pos → Δ pos) (shape : ShapeOver l Agent Δ) : ShapeOver l Agent Γ

Reindex a functorial local syntax object contravariantly along a node metadata map.

@[simp]

theorem Interaction.ShapeOver.comap_id {P : PFunctor.{uA, uB}} {Q : PFunctor.{uA₂, uB₂}} {l : P.Lens Q} {Agent : Type a} {Γ : P.A → Type vΓ} (shape : ShapeOver l Agent Γ) : comap (fun (x : P.A) (γ : Γ x) => γ) shape = shape

theorem Interaction.ShapeOver.comap_comp {P : PFunctor.{uA, uB}} {Q : PFunctor.{uA₂, uB₂}} {l : P.Lens Q} {Agent : Type a} {Γ : P.A → Type vΓ} {Δ : P.A → Type vΔ} {Λ : P.A → Type vΛ} (shape : ShapeOver l Agent Λ) (g : (pos : P.A) → Δ pos → Λ pos) (f : (pos : P.A) → Γ pos → Δ pos) : comap f (comap g shape) = comap (fun (pos : P.A) => g pos ∘ f pos) shape