Per-party local-view profiles for multiparty interaction

This file packages the most structured native multiparty interface built on top of Interaction.Multiparty.Core.

A node of move space X is decorated not merely by one local view, but by a whole profile assigning each party its own LocalView X. The endpoint of one fixed party is then obtained by projecting that profile to the chosen party.

This is the most direct structured way to describe multiparty nodes with:

• one active controller of the move;
• parties that observe the full move;
• parties that observe only a quotient of the move; and
• parties that observe nothing at all.

@[reducible, inline]

abbrev Interaction.Multiparty.Profile.ViewProfile (Party : Type u) : Spec.Node.Context

ViewProfile Party X assigns to each party its local view of a node whose move space is X.

This is the intended structured node-local metadata for adversarial and multiparty interaction: one actual global move may give different local observations to different parties.

@[reducible, inline]

abbrev Interaction.Multiparty.Profile.Decoration (Party : Type u) : Spec → Type (u + 1)

A Decoration Party spec assigns one local-view profile to every node of spec.

At a node with move space X, the attached profile says, for each party, how that party locally sees the chosen move x : X.

@[reducible, inline]

abbrev Interaction.Multiparty.Profile.Strategy (m : Type u → Type u) {Party : Type u} (me : Party) (spec : Spec) (views : Decoration Party spec) (Output : spec.Transcript → Type u) : Type u

Profile.Strategy m me spec views Output is the local endpoint type of the fixed party me under the local-view profiles recorded by views.

This is obtained by projecting each node's full per-party profile to the view of me, then reusing the generic multiparty Strategy.