Decorations and dependent decorations (Over)

Spec.Decoration Γ spec is concrete nodewise metadata attached to a fixed protocol tree spec, where Γ : Spec.Node.Context is the realized family of node-local information. If a node of spec has move space X, then a decoration provides one value of type Γ X at that node, and recursively decorates every continuation subtree.

This is the basic way to say "the same protocol tree, but with extra data at each node". Typical examples include:

• RoleDecoration, recording who controls a node;
• monad decorations, recording which monad a local action uses at a node;
• oracle decorations, recording what oracle interface is available there.

A context may be written directly, or obtained from a telescope Spec.Node.Schema via Spec.Node.Schema.toContext.

Decoration.Over is the dependent (displayed) variant: its fibers may depend on the context value drawn from an existing decoration.

Naming note: Decoration.Over is nested because it is literally a decoration over a fixed base decoration value. By contrast, ShapeOver and InteractionOver keep the suffix form because they are the primary generalized syntax and semantics layers, not dependent objects over a fixed base Shape or Interaction.

Functorial map / map_id / map_comp for both layers are in this file. Composition along Spec.append is in VCVio.Interaction.Basic.Append.

Because decorations are concrete tree data, they are covariant in node-local contexts: a context morphism Γ → Δ induces a map from decorations by Γ to decorations by Δ. The schema-facing API in Decoration.Schema packages that same idea for realized contexts presented by schemas via Spec.Node.Schema.SchemaMap.

This file also contains the bridge between the semantic and staged views of node metadata: decorating a tree by an extended context Γ.extend A is equivalent to giving a base decoration by Γ together with one dependent Decoration.Over A layer on top of it.

In particular, if a schema is built as (Spec.Node.Schema.singleton Γ).extend A, then Decoration.equivOver A spec is exactly the statement that a decoration of that schema's realized context is the same as a base decoration by Γ plus one displayed layer over it.

The file concludes by lifting this one-step bridge recursively to arbitrary schemas: Spec.Decoration.Schema.View is the staged telescope view of a decoration by S.toContext, and Spec.Decoration.Schema.equivView identifies that staged view with an ordinary decoration of the realized context.

def Interaction.Spec.Decoration (Γ : Node.Context) : Spec → Type (max u v)

Decoration Γ spec is concrete nodewise metadata on the fixed protocol tree spec, for a realized node context Γ.

If a node of spec has move space X, then the decoration stores one value of type Γ X at that node, and recursively stores decorations on every subtree.

This is different from Spec.SyntaxOver:

• a decoration is data on a tree;
• syntax is a specification of local participant objects that consumes such data;
• Spec.ShapeOver is the functorial refinement of that syntax layer.

def Interaction.Spec.Decoration.map {Γ : Node.Context} {Δ : Node.Context} (f : Node.ContextHom Γ Δ) (spec : Spec) : Decoration Γ spec → Decoration Δ spec

Natural transformation between per-node decorations, applied recursively.

@[simp]

theorem Interaction.Spec.Decoration.map_id {Γ : Node.Context} (spec : Spec) (d : Decoration Γ spec) : map (Node.ContextHom.id Γ) spec d = d

theorem Interaction.Spec.Decoration.map_comp {Γ : Node.Context} {Δ : Node.Context} {Λ : Node.Context} (g : Node.ContextHom Δ Λ) (f : Node.ContextHom Γ Δ) (spec : Spec) (d : Decoration Γ spec) : map g spec (map f spec d) = map (g.comp f) spec d

def Interaction.Spec.Decoration.Over {Γ : Node.Context} (F : (X : Type u) → Γ X → Type w) (spec : Spec) : Decoration Γ spec → Type (max u w)

Dependent decoration over d : Decoration Γ spec: at each node, data in F X γ where γ is the context value from d, plus recursive decorations on subtrees.

def Interaction.Spec.Decoration.Over.map {Γ : Node.Context} {F G : (X : Type u) → Γ X → Type w} (f : (X : Type u) → (γ : Γ X) → F X γ → G X γ) (spec : Spec) (d : Decoration Γ spec) : Over F spec d → Over G spec d

Fiberwise map between dependent decoration families over the same base decoration.

@[simp]

theorem Interaction.Spec.Decoration.Over.map_id {Γ : Node.Context} {F : (X : Type u) → Γ X → Type w} (spec : Spec) (d : Decoration Γ spec) (r : Over F spec d) : map (fun (x : Type u) (x_1 : Γ x) (x_2 : F x x_1) => x_2) spec d r = r

theorem Interaction.Spec.Decoration.Over.map_comp {Γ : Node.Context} {F G H : (X : Type u) → Γ X → Type w} (g : (X : Type u) → (γ : Γ X) → G X γ → H X γ) (f : (X : Type u) → (γ : Γ X) → F X γ → G X γ) (spec : Spec) (d : Decoration Γ spec) (r : Over F spec d) : map g spec d (map f spec d r) = map (fun (X : Type u) (γ : Γ X) => g X γ ∘ f X γ) spec d r

def Interaction.Spec.Decoration.Over.mapBase {Γ : Node.Context} {Δ : Node.Context} {A : (X : Type u) → Γ X → Type w₂} {B : (X : Type u) → Δ X → Type w₂} (f : Node.ContextHom Γ Δ) (g : (X : Type u) → (γ : Γ X) → A X γ → B X (f X γ)) (spec : Spec) (d : Decoration Γ spec) : Over A spec d → Over B spec (Decoration.map f spec d)

Transport a dependent decoration across a map of base contexts.

Given:

• a base-context morphism f : Γ → Δ, and
• a fiberwise map g from A X γ to B X (f X γ),

this sends a displayed decoration over d : Decoration Γ spec to a displayed decoration over Decoration.map f spec d.

theorem Interaction.Spec.Decoration.Over.mapBase_id {Γ : Node.Context} {A : (X : Type u) → Γ X → Type w} (spec : Spec) (d : Decoration Γ spec) (r : Over A spec d) : mapBase (Node.ContextHom.id Γ) (fun (x : Type u) (x_1 : Γ x) (x_2 : A x x_1) => x_2) spec d r ≍ r

theorem Interaction.Spec.Decoration.Over.mapBase_comp {Γ : Node.Context} {Δ : Node.Context} {Λ : Node.Context} {A : (X : Type u) → Γ X → Type w₂} {B : (X : Type u) → Δ X → Type w₂} {C : (X : Type u) → Λ X → Type w₂} (f : Node.ContextHom Γ Δ) (g : Node.ContextHom Δ Λ) (fOver : (X : Type u) → (γ : Γ X) → A X γ → B X (f X γ)) (gOver : (X : Type u) → (δ : Δ X) → B X δ → C X (g X δ)) (spec : Spec) (d : Decoration Γ spec) (r : Over A spec d) : mapBase g gOver spec (Decoration.map f spec d) (mapBase f fOver spec d r) ≍ mapBase (g.comp f) (fun (X : Type u) (γ : Γ X) => gOver X (f X γ) ∘ fOver X γ) spec d r

def Interaction.Spec.Decoration.ofOver {Γ : Node.Context} (A : (X : Type u) → Γ X → Type w) (spec : Spec) (d : Decoration Γ spec) : Over A spec d → Decoration (Node.Context.extend Γ A) spec

Pack a base decoration and one dependent Over layer into a decoration of the extended context Γ.extend A.

This is the tree-level realization of a single schema extension step.

theorem Interaction.Spec.Decoration.map_ofOver {Γ : Node.Context} {Δ : Node.Context} {A : (X : Type u) → Γ X → Type w₂} {B : (X : Type u) → Δ X → Type w₂} (f : Node.ContextHom Γ Δ) (g : (X : Type u) → (γ : Γ X) → A X γ → B X (f X γ)) (spec : Spec) (d : Decoration Γ spec) (r : Over A spec d) : map (Node.Context.extendMap f g) spec (ofOver A spec d r) = ofOver B spec (map f spec d) (Over.mapBase f g spec d r)

def Interaction.Spec.Decoration.toOver {Γ : Node.Context} (A : (X : Type u) → Γ X → Type w) (spec : Spec) : Decoration (Node.Context.extend Γ A) spec → (d : Decoration Γ spec) × Over A spec d

Unpack a decoration of the extended context Γ.extend A into:

• its base decoration by Γ, and
• its displayed Decoration.Over A layer above that base.

This is the inverse structural view to Decoration.ofOver.

@[simp]

theorem Interaction.Spec.Decoration.toOver_ofOver {Γ : Node.Context} (A : (X : Type u) → Γ X → Type w) (spec : Spec) (d : Decoration Γ spec) (r : Over A spec d) : toOver A spec (ofOver A spec d r) = ⟨d, r⟩

@[simp]

theorem Interaction.Spec.Decoration.ofOver_toOver {Γ : Node.Context} (A : (X : Type u) → Γ X → Type w) (spec : Spec) (d : Decoration (Node.Context.extend Γ A) spec) : ofOver A spec (toOver A spec d).fst (toOver A spec d).snd = d

def Interaction.Spec.Decoration.equivOver {Γ : Node.Context} (A : (X : Type u) → Γ X → Type w) (spec : Spec) : Decoration (Node.Context.extend Γ A) spec ≃ (d : Decoration Γ spec) × Over A spec d

Equivalence between:

• decorating a tree by the extended context Γ.extend A, and
• decorating it by Γ together with one Decoration.Over A layer.

This is the main bridge from the semantic "single realized context" view to the staged schema/dependent-decoration view.

Concrete example: if a schema is built as (Spec.Node.Schema.singleton Tag).extend Data, then decorations of its realized context Node.Context.extend Tag Data are equivalent to pairs consisting of:

• tags : Decoration Tag spec, and
• datas : Decoration.Over Data spec tags.

@[reducible, inline]

abbrev Interaction.Spec.Decoration.Schema.map {Γ Δ : Node.Context} {S : Node.Schema Γ} {T : Node.Schema Δ} (f : S.SchemaMap T) (spec : Spec) : Decoration S.toContext spec → Decoration T.toContext spec

Map decorations along a schema morphism.

This is just Decoration.map viewed through schema-level sources and targets.

@[simp]

theorem Interaction.Spec.Decoration.Schema.map_id {Γ : Node.Context} {S : Node.Schema Γ} (spec : Spec) (d : Decoration S.toContext spec) : map (Node.Schema.SchemaMap.id S) spec d = d

theorem Interaction.Spec.Decoration.Schema.map_comp {Γ Δ Λ : Node.Context} {S : Node.Schema Γ} {T : Node.Schema Δ} {U : Node.Schema Λ} (g : T.SchemaMap U) (f : S.SchemaMap T) (spec : Spec) (d : Decoration S.toContext spec) : map g spec (map f spec d) = map (g.comp f) spec d

theorem Interaction.Spec.Decoration.Schema.map_ofOver {Γ Δ : Node.Context} {S : Node.Schema Γ} {T : Node.Schema Δ} {A : (X : Type u) → Γ X → Type v} {B : (X : Type u) → Δ X → Type v} (f : S.SchemaMap T) (g : (X : Type u) → (γ : Γ X) → A X γ → B X (f X γ)) (spec : Spec) (d : Decoration Γ spec) (r : Over A spec d) : map (f.extend g) spec (ofOver A spec d r) = ofOver B spec (map f spec d) (Over.mapBase f g spec d r)

def Interaction.Spec.Decoration.Schema.telescope {Γ : Node.Context} (S : Node.Schema Γ) (spec : Spec) : (T : Type (max u v)) × (Decoration Γ spec ≃ T)

Decoration.Schema.telescope S spec packages the staged telescope view of decorations for schema S, together with an equivalence from ordinary decorations by the realized context S.toContext.

The resulting type is the recursively decomposed form of a decoration: each snoc in the schema contributes one more displayed Decoration.Over layer.

@[reducible, inline]

abbrev Interaction.Spec.Decoration.Schema.View {Γ : Node.Context} (S : Node.Schema Γ) (spec : Spec) : Type (max u v)

Decoration.Schema.View S spec is the staged telescope view carried by the recursive schema decomposition theorem Decoration.Schema.telescope.

@[reducible, inline]

abbrev Interaction.Spec.Decoration.Schema.unpack {Γ : Node.Context} (S : Node.Schema Γ) (spec : Spec) : Decoration Γ spec → View S spec

Unpack an ordinary decoration into the staged telescope view determined by a schema.

@[reducible, inline]

abbrev Interaction.Spec.Decoration.Schema.pack {Γ : Node.Context} (S : Node.Schema Γ) (spec : Spec) : View S spec → Decoration Γ spec

Pack a staged schema-decoration view back into an ordinary decoration of the realized context.

@[simp]

theorem Interaction.Spec.Decoration.Schema.pack_unpack {Γ : Node.Context} (S : Node.Schema Γ) (spec : Spec) (d : Decoration Γ spec) : pack S spec (unpack S spec d) = d

@[simp]

theorem Interaction.Spec.Decoration.Schema.unpack_pack {Γ : Node.Context} (S : Node.Schema Γ) (spec : Spec) (d : View S spec) : unpack S spec (pack S spec d) = d

@[reducible, inline]

abbrev Interaction.Spec.Decoration.Schema.mapView {Γ Δ : Node.Context} {S : Node.Schema Γ} {T : Node.Schema Δ} (f : S.SchemaMap T) (spec : Spec) : View S spec → View T spec

Map the staged telescope view of decorations along a schema morphism.

This is the schema-view analogue of Decoration.Schema.map: pack the staged view into an ordinary decoration, map that decoration along the schema morphism, then unpack it into the staged view for the target schema.

@[simp]

theorem Interaction.Spec.Decoration.Schema.unpack_map {Γ Δ : Node.Context} {S : Node.Schema Γ} {T : Node.Schema Δ} (f : S.SchemaMap T) (spec : Spec) (d : Decoration S.toContext spec) : unpack T spec (map f spec d) = mapView f spec (unpack S spec d)

@[simp]

theorem Interaction.Spec.Decoration.Schema.pack_mapView {Γ Δ : Node.Context} {S : Node.Schema Γ} {T : Node.Schema Δ} (f : S.SchemaMap T) (spec : Spec) (d : View S spec) : pack T spec (mapView f spec d) = map f spec (pack S spec d)

@[simp]

theorem Interaction.Spec.Decoration.Schema.mapView_id {Γ : Node.Context} {S : Node.Schema Γ} (spec : Spec) (d : View S spec) : mapView (Node.Schema.SchemaMap.id S) spec d = d

theorem Interaction.Spec.Decoration.Schema.mapView_comp {Γ Δ Λ : Node.Context} {S : Node.Schema Γ} {T : Node.Schema Δ} {U : Node.Schema Λ} (g : T.SchemaMap U) (f : S.SchemaMap T) (spec : Spec) (d : View S spec) : mapView g spec (mapView f spec d) = mapView (g.comp f) spec d

@[reducible, inline]

abbrev Interaction.Spec.Decoration.Schema.Prefix.map {Γ Δ : Node.Context} {S : Node.Schema Γ} {T : Node.Schema Δ} (p : S.Prefix T) (spec : Spec) : Decoration T.toContext spec → Decoration S.toContext spec

Project decorations along a syntactic schema prefix.

This is the tree-level forgetting map induced by the schema morphism Node.Schema.Prefix.toSchemaMap.

@[reducible, inline]

abbrev Interaction.Spec.Decoration.Schema.equivView {Γ : Node.Context} (S : Node.Schema Γ) (spec : Spec) : Decoration Γ spec ≃ View S spec

Equivalence between an ordinary decoration by the realized context of S and its staged telescope view.

This is the recursive schema-level form of Decoration.equivOver.