Swapping roles #
Involutivity of Role.swap, compatibility with RoleDecoration.map, and interaction with
appended role decorations.
@[simp]
theorem
Interaction.RoleDecoration.swap_append
{s₁ : Spec}
{s₂ : s₁.Transcript → Spec}
(r₁ : RoleDecoration s₁)
(r₂ : (tr₁ : s₁.Transcript) → RoleDecoration (s₂ tr₁))
:
(Spec.Decoration.append r₁ r₂).swap = (Spec.Decoration.swap r₁).append fun (tr₁ : s₁.Transcript) => Spec.Decoration.swap (r₂ tr₁)
Swapping commutes with appended role decorations.