Role-aware refinement and bridge to Decoration.Over

Role.Refine S carries sender data S X and skips receiver nodes (no PUnit padding). Conversion to Spec.Decoration.Over with fiber Role.SenderData is an equivalence; map laws commute with append, replicate, and stateChain.

@[reducible]

def Interaction.Role.Refine (S : Type u → Type v) (spec : Spec) : RoleDecoration spec → Type (max u v)

Role-aware displayed data: S X at sender nodes; ∀ recursion at receiver nodes.

def Interaction.Role.Refine.map {S : Type u → Type v} {T : Type u → Type w} (f : (X : Type u) → S X → T X) (spec : Spec) (roles : RoleDecoration spec) : Refine S spec roles → Refine T spec roles

Natural transformation of sender fibers, applied recursively.

def Interaction.Role.Refine.append {S : Type u → Type v} {s₁ : Spec} {s₂ : s₁.Transcript → Spec} {r₁ : RoleDecoration s₁} {r₂ : (tr₁ : s₁.Transcript) → RoleDecoration (s₂ tr₁)} : Refine S s₁ r₁ → ((tr₁ : s₁.Transcript) → Refine S (s₂ tr₁) (r₂ tr₁)) → Refine S (s₁.append s₂) (Spec.Decoration.append r₁ r₂)

Append refinements over appended role decorations.

def Interaction.Role.Refine.replicate {S : Type u → Type v} {spec : Spec} {roles : RoleDecoration spec} (sd : Refine S spec roles) (n : ℕ) : Refine S (spec.replicate n) (Spec.Decoration.replicate roles n)

Replicate along Spec.replicate / Spec.Decoration.replicate.

def Interaction.Role.Refine.stateChain {S : Type u → Type v} {Stage : ℕ → Type u} {spec : (i : ℕ) → Stage i → Spec} {advance : (i : ℕ) → (s : Stage i) → (spec i s).Transcript → Stage (i + 1)} {roles : (i : ℕ) → (s : Stage i) → RoleDecoration (spec i s)} (sdeco : (i : ℕ) → (s : Stage i) → Refine S (spec i s) (roles i s)) (n i : ℕ) (s : Stage i) : Refine S (Spec.stateChain Stage spec advance n i s) (Spec.Decoration.stateChain roles n i s)

Chain a family of refinements along Spec.stateChain.

def Interaction.Role.SenderData (S : Type u → Type v) (X : Type u) : Role → Type v

Fiber S X at sender and PUnit at receiver (for the Decoration.Over bridge).

def Interaction.Role.SenderData.map {S T : Type u → Type v} (f : (X : Type u) → S X → T X) (X : Type u) (r : Role) : SenderData S X r → SenderData T X r

Functorial update of SenderData under f : ∀ X, S X → T X.

@[simp]

theorem Interaction.Role.Refine.map_id {S : Type u → Type v} (spec : Spec) (roles : RoleDecoration spec) (rr : Refine S spec roles) : map (fun (X : Type u) (s : S X) => s) spec roles rr = rr

theorem Interaction.Role.Refine.map_comp {S : Type u → Type v} {T : Type u → Type w} {U : Type u → Type w₂} (g : (X : Type u) → T X → U X) (f : (X : Type u) → S X → T X) (spec : Spec) (roles : RoleDecoration spec) (rr : Refine S spec roles) : map g spec roles (map f spec roles rr) = map (fun (X : Type u) => g X ∘ f X) spec roles rr

theorem Interaction.Role.Refine.map_append {S T : Type u → Type v} (f : (X : Type u) → S X → T X) {s₁ : Spec} {s₂ : s₁.Transcript → Spec} {rd₁ : RoleDecoration s₁} {rd₂ : (tr₁ : s₁.Transcript) → RoleDecoration (s₂ tr₁)} (sd₁ : Refine S s₁ rd₁) (sd₂ : (tr₁ : s₁.Transcript) → Refine S (s₂ tr₁) (rd₂ tr₁)) : map f (s₁.append s₂) (Spec.Decoration.append rd₁ rd₂) (sd₁.append sd₂) = (map f s₁ rd₁ sd₁).append fun (tr₁ : s₁.Transcript) => map f (s₂ tr₁) (rd₂ tr₁) (sd₂ tr₁)

theorem Interaction.Role.Refine.map_replicate {S T : Type u → Type v} (f : (X : Type u) → S X → T X) {spec : Spec} {roles : RoleDecoration spec} (sd : Refine S spec roles) (n : ℕ) : map f (spec.replicate n) (Spec.Decoration.replicate roles n) (sd.replicate n) = (map f spec roles sd).replicate n

theorem Interaction.Role.Refine.map_stateChain {S T : Type u → Type v} (f : (X : Type u) → S X → T X) {Stage : ℕ → Type u} {spec : (i : ℕ) → Stage i → Spec} {advance : (i : ℕ) → (s : Stage i) → (spec i s).Transcript → Stage (i + 1)} {roles : (i : ℕ) → (s : Stage i) → RoleDecoration (spec i s)} (sdeco : (i : ℕ) → (s : Stage i) → Refine S (spec i s) (roles i s)) (n i : ℕ) (s : Stage i) : map f (Spec.stateChain Stage spec advance n i s) (Spec.Decoration.stateChain roles n i s) (stateChain sdeco n i s) = stateChain (fun (j : ℕ) (t : Stage j) => map f (spec j t) (roles j t) (sdeco j t)) n i s

def Interaction.Role.Refine.toDecorationOver {S : Type u → Type v} (spec : Spec) (roles : RoleDecoration spec) : Refine S spec roles → Spec.Decoration.Over (fun (X : Type u) (r : Role) => SenderData S X r) spec roles

def Interaction.Role.Refine.ofDecorationOver {S : Type u → Type v} (spec : Spec) (roles : RoleDecoration spec) : Spec.Decoration.Over (fun (X : Type u) (r : Role) => SenderData S X r) spec roles → Refine S spec roles

@[simp]

theorem Interaction.Role.Refine.toDecorationOver_ofDecorationOver {S : Type u → Type v} (spec : Spec) (roles : RoleDecoration spec) (dr : Spec.Decoration.Over (fun (X : Type u) (r : Role) => SenderData S X r) spec roles) : toDecorationOver spec roles (ofDecorationOver spec roles dr) = dr

@[simp]

theorem Interaction.Role.Refine.ofDecorationOver_toDecorationOver {S : Type u → Type v} (spec : Spec) (roles : RoleDecoration spec) (rr : Refine S spec roles) : ofDecorationOver spec roles (toDecorationOver spec roles rr) = rr

def Interaction.Role.Refine.equivDecorationOver {S : Type u → Type v} (spec : Spec) (roles : RoleDecoration spec) : Refine S spec roles ≃ Spec.Decoration.Over (fun (X : Type u) (r : Role) => SenderData S X r) spec roles

Canonical equivalence with Decoration.Over at fiber SenderData.

theorem Interaction.Role.Refine.toDecorationOver_map {S T : Type u → Type v} (f : (X : Type u) → S X → T X) (spec : Spec) (roles : RoleDecoration spec) (rr : Refine S spec roles) : toDecorationOver spec roles (map f spec roles rr) = Spec.Decoration.Over.map (fun (X : Type u) (r : Role) => SenderData.map f X r) spec roles (toDecorationOver spec roles rr)

theorem Interaction.Role.Refine.ofDecorationOver_map {S T : Type u → Type v} (f : (X : Type u) → S X → T X) (spec : Spec) (roles : RoleDecoration spec) (dr : Spec.Decoration.Over (fun (X : Type u) (r : Role) => SenderData S X r) spec roles) : ofDecorationOver spec roles (Spec.Decoration.Over.map (fun (X : Type u) (r : Role) => SenderData.map f X r) spec roles dr) = map f spec roles (ofDecorationOver spec roles dr)