Open composition algebra with monoidal coherence

This module defines OpenTheory, a boundary-indexed algebra of open systems, together with a hierarchy of lawfulness classes capturing increasingly strong equational properties.

Operations

• map adapts how an exposed boundary is presented.
• par places two open systems side by side (tensor of boundaries).
• wire internalizes one shared boundary between two open systems.
• plug closes an open system against a matching context on the swapped boundary.

Class hierarchy

• IsLawfulMap: functoriality of map (identity and composition).
• IsLawfulPar/IsLawfulWire/IsLawfulPlug: naturality of each combinator with respect to boundary adaptation.
• IsLawful: bundles all naturality laws.
• Monoidal: symmetric monoidal coherence for par (associativity, commutativity, left and right unit laws via a distinguished unit object).
• CompactClosed: compact closed structure (idWire as coevaluation, plug derivable from wire, zig-zag identity for wire_idWire).

Concrete realizations include the free models (Expr.theory, Interp.theory) and the process-backed openTheory in OpenProcessModel.lean.

structure Interaction.UC.OpenTheory : Type (u + 1)

OpenTheory is a boundary-indexed algebra of open systems.

For each directed boundary Δ, Obj Δ is the type of systems that still expose Δ to an external context. The structure then specifies three primitive composition operations:

• map changes how an exposed boundary is presented, without changing the internal system;
• par places two open systems side by side and exposes the tensor of their boundaries;
• wire connects one shared boundary between two open systems and leaves the remaining outer boundaries exposed; and
• plug closes an open system against a matching context on the swapped boundary, yielding a closed system.

Lawfulness is stratified into three levels via the class hierarchy IsLawful ≤ Monoidal ≤ CompactClosed (see the module docstring).

Universe polymorphism: one ambient pair of universes for ports and messages on both sides of every boundary, keeping PortBoundary.swap inside the same family of objects.

• Obj : PortBoundary → Type u

  Obj Δ is the type of open systems exposing boundary Δ.

  The boundary is directed: Δ.In is what the surrounding context may send into the system, and Δ.Out is what the system may emit back out.

• map {Δ₁ Δ₂ : PortBoundary} : Δ₁.Hom Δ₂ → self.Obj Δ₁ → self.Obj Δ₂

  Adapt the exposed boundary of an open system along a structural boundary morphism.

  This changes only the presentation of the boundary. The intended reading is that map φ W is the same internal system as W, but viewed through the interface adaptation φ.

• par {Δ₁ Δ₂ : PortBoundary} : self.Obj Δ₁ → self.Obj Δ₂ → self.Obj (Δ₁.tensor Δ₂)

  Place two open systems side by side.

  The resulting system exposes the tensor of the two boundaries: the outside world may interact independently with either side.

• wire {Δ₁ Γ Δ₂ : PortBoundary} : self.Obj (Δ₁.tensor Γ) → self.Obj (Γ.swap.tensor Δ₂) → self.Obj (Δ₁.tensor Δ₂)

  Connect one shared boundary between two open systems.

  If the left system exposes boundary Δ₁ ⊗ Γ and the right system exposes boundary swap Γ ⊗ Δ₂, then wire connects the shared middle boundary Γ internally and leaves only the outer boundaries Δ₁ and Δ₂ exposed.

  This is the first local composition primitive beyond plain parallel juxtaposition. It is the right operation for assembling open systems incrementally without forcing immediate total closure.

• plug {Δ : PortBoundary} : self.Obj Δ → self.Obj Δ.swap → self.Obj PortBoundary.empty

  Close an open system against a matching plug.

  If W : Obj Δ is an open system and K : Obj (PortBoundary.swap Δ) is a context exposing the opposite boundary, then plug W K is the structurally closed result of connecting those two boundaries together.

  This is the minimal closure operation needed for UC-style contextual comparison. More general partial internalization operations can be added later if they are genuinely needed.

class Interaction.UC.OpenTheory.IsLawfulMap (T : OpenTheory) : Prop

IsLawfulMap T states that boundary adaptation in T behaves functorially.

This is the first law layer for OpenTheory, and the one we can state without committing to any further monoidal/coherence structure on boundaries.

• map_id {Δ : PortBoundary} (W : T.Obj Δ) : T.map (PortBoundary.Hom.id Δ) W = W

  Adapting a system along the identity boundary morphism does nothing.

• map_comp {Δ₁ Δ₂ Δ₃ : PortBoundary} (g : Δ₂.Hom Δ₃) (f : Δ₁.Hom Δ₂) (W : T.Obj Δ₁) : T.map (g.comp f) W = T.map g (T.map f W)

  Adapting along a composite boundary morphism is the same as adapting in two successive steps.

class Interaction.UC.OpenTheory.IsLawfulPar (T : OpenTheory) extends T.IsLawfulMap : Prop

IsLawfulPar T states that parallel composition in T is natural with respect to boundary adaptation.

This is the first structural law for par that does not require introducing a separate theory of boundary isomorphisms. Associativity and unit laws can be added later once that boundary-equivalence vocabulary is in place.

• map_id {Δ : PortBoundary} (W : T.Obj Δ) : T.map (PortBoundary.Hom.id Δ) W = W
• map_comp {Δ₁ Δ₂ Δ₃ : PortBoundary} (g : Δ₂.Hom Δ₃) (f : Δ₁.Hom Δ₂) (W : T.Obj Δ₁) : T.map (g.comp f) W = T.map g (T.map f W)
• map_par {Δ₁ Δ₁' Δ₂ Δ₂' : PortBoundary} (f₁ : Δ₁.Hom Δ₁') (f₂ : Δ₂.Hom Δ₂') (W₁ : T.Obj Δ₁) (W₂ : T.Obj Δ₂) : T.map (f₁.tensor f₂) (T.par W₁ W₂) = T.par (T.map f₁ W₁) (T.map f₂ W₂)

  Mapping a side-by-side composite along a tensor boundary morphism is the same as mapping each side independently before composing them in parallel.

class Interaction.UC.OpenTheory.IsLawfulWire (T : OpenTheory) extends T.IsLawfulMap : Prop

IsLawfulWire T states that partial wiring in T is natural with respect to boundary adaptation.

This is the first law for local composition: adapting the still-exposed left/right outer boundaries can be pushed inside a wire.

Transporting the shared middle boundary itself is a subtler question because PortBoundary.Hom.swap is contravariant. The corresponding law should be stated later using boundary equivalences or a more symmetric vocabulary.

• map_id {Δ : PortBoundary} (W : T.Obj Δ) : T.map (PortBoundary.Hom.id Δ) W = W
• map_comp {Δ₁ Δ₂ Δ₃ : PortBoundary} (g : Δ₂.Hom Δ₃) (f : Δ₁.Hom Δ₂) (W : T.Obj Δ₁) : T.map (g.comp f) W = T.map g (T.map f W)
• map_wire {Δ₁ Δ₁' Γ Δ₂ Δ₂' : PortBoundary} (f₁ : Δ₁.Hom Δ₁') (f₂ : Δ₂.Hom Δ₂') (W₁ : T.Obj (Δ₁.tensor Γ)) (W₂ : T.Obj (Γ.swap.tensor Δ₂)) : T.map (f₁.tensor f₂) (T.wire W₁ W₂) = T.wire (T.map (f₁.tensor (PortBoundary.Hom.id Γ)) W₁) (T.map ((PortBoundary.Hom.id Γ.swap).tensor f₂) W₂)

  Partial wiring is natural in its still-exposed outer boundaries.

  The shared middle boundary is held fixed in this first law layer. That keeps the statement well aligned with the variance of PortBoundary.Hom while still capturing the most important structural behavior of wire.

class Interaction.UC.OpenTheory.IsLawfulPlug (T : OpenTheory) extends T.IsLawfulMap : Prop

IsLawfulPlug T states that plugging in T is natural with respect to boundary adaptation.

This is the first structural law for plug: adapting the open side before closure is equivalent to adapting the matching plug on the swapped boundary.

• map_id {Δ : PortBoundary} (W : T.Obj Δ) : T.map (PortBoundary.Hom.id Δ) W = W
• map_comp {Δ₁ Δ₂ Δ₃ : PortBoundary} (g : Δ₂.Hom Δ₃) (f : Δ₁.Hom Δ₂) (W : T.Obj Δ₁) : T.map (g.comp f) W = T.map g (T.map f W)
• map_plug {Δ₁ Δ₂ : PortBoundary} (f : Δ₁.Hom Δ₂) (W : T.Obj Δ₁) (K : T.Obj Δ₂.swap) : T.plug (T.map f W) K = T.plug W (T.map f.swap K)

  Boundary adaptation may be pushed across a plug by swapping the same adaptation onto the context side.

class Interaction.UC.OpenTheory.IsLawful (T : OpenTheory) extends T.IsLawfulPar, T.IsLawfulWire, T.IsLawfulPlug : Prop

IsLawful T is the first bundled law package for an open-composition theory.

At this stage it only records:

• functoriality of map,
• naturality of par, and
• naturality of wire, and
• naturality of plug.

Unit, associativity, and symmetry laws for open composition should be added later, once the library settles on the right notion of boundary equivalence.

• map_id {Δ : PortBoundary} (W : T.Obj Δ) : T.map (PortBoundary.Hom.id Δ) W = W
• map_comp {Δ₁ Δ₂ Δ₃ : PortBoundary} (g : Δ₂.Hom Δ₃) (f : Δ₁.Hom Δ₂) (W : T.Obj Δ₁) : T.map (g.comp f) W = T.map g (T.map f W)
• map_par {Δ₁ Δ₁' Δ₂ Δ₂' : PortBoundary} (f₁ : Δ₁.Hom Δ₁') (f₂ : Δ₂.Hom Δ₂') (W₁ : T.Obj Δ₁) (W₂ : T.Obj Δ₂) : T.map (f₁.tensor f₂) (T.par W₁ W₂) = T.par (T.map f₁ W₁) (T.map f₂ W₂)
• map_wire {Δ₁ Δ₁' Γ Δ₂ Δ₂' : PortBoundary} (f₁ : Δ₁.Hom Δ₁') (f₂ : Δ₂.Hom Δ₂') (W₁ : T.Obj (Δ₁.tensor Γ)) (W₂ : T.Obj (Γ.swap.tensor Δ₂)) : T.map (f₁.tensor f₂) (T.wire W₁ W₂) = T.wire (T.map (f₁.tensor (PortBoundary.Hom.id Γ)) W₁) (T.map ((PortBoundary.Hom.id Γ.swap).tensor f₂) W₂)
• map_plug {Δ₁ Δ₂ : PortBoundary} (f : Δ₁.Hom Δ₂) (W : T.Obj Δ₁) (K : T.Obj Δ₂.swap) : T.plug (T.map f W) K = T.plug W (T.map f.swap K)

class Interaction.UC.OpenTheory.Monoidal (T : OpenTheory) extends T.IsLawful : Type u

Monoidal T extends IsLawful T with the symmetric monoidal coherence laws for par: a unit object, plus associativity, commutativity (braiding), and left/right unit laws up to boundary equivalence.

Pentagon and hexagon coherence conditions are deferred: they are derivable in the free models and hold trivially for the concrete model up to process isomorphism.

• map_id {Δ : PortBoundary} (W : T.Obj Δ) : T.map (PortBoundary.Hom.id Δ) W = W
• map_comp {Δ₁ Δ₂ Δ₃ : PortBoundary} (g : Δ₂.Hom Δ₃) (f : Δ₁.Hom Δ₂) (W : T.Obj Δ₁) : T.map (g.comp f) W = T.map g (T.map f W)
• map_par {Δ₁ Δ₁' Δ₂ Δ₂' : PortBoundary} (f₁ : Δ₁.Hom Δ₁') (f₂ : Δ₂.Hom Δ₂') (W₁ : T.Obj Δ₁) (W₂ : T.Obj Δ₂) : T.map (f₁.tensor f₂) (T.par W₁ W₂) = T.par (T.map f₁ W₁) (T.map f₂ W₂)
• map_wire {Δ₁ Δ₁' Γ Δ₂ Δ₂' : PortBoundary} (f₁ : Δ₁.Hom Δ₁') (f₂ : Δ₂.Hom Δ₂') (W₁ : T.Obj (Δ₁.tensor Γ)) (W₂ : T.Obj (Γ.swap.tensor Δ₂)) : T.map (f₁.tensor f₂) (T.wire W₁ W₂) = T.wire (T.map (f₁.tensor (PortBoundary.Hom.id Γ)) W₁) (T.map ((PortBoundary.Hom.id Γ.swap).tensor f₂) W₂)
• map_plug {Δ₁ Δ₂ : PortBoundary} (f : Δ₁.Hom Δ₂) (W : T.Obj Δ₁) (K : T.Obj Δ₂.swap) : T.plug (T.map f W) K = T.plug W (T.map f.swap K)
• unit : T.Obj PortBoundary.empty
• par_assoc {Δ₁ Δ₂ Δ₃ : PortBoundary} (W₁ : T.Obj Δ₁) (W₂ : T.Obj Δ₂) (W₃ : T.Obj Δ₃) : T.map (PortBoundary.Equiv.tensorAssoc Δ₁ Δ₂ Δ₃).toHom (T.par (T.par W₁ W₂) W₃) = T.par W₁ (T.par W₂ W₃)
• par_comm {Δ₁ Δ₂ : PortBoundary} (W₁ : T.Obj Δ₁) (W₂ : T.Obj Δ₂) : T.map (PortBoundary.Equiv.tensorComm Δ₁ Δ₂).toHom (T.par W₁ W₂) = T.par W₂ W₁
• par_leftUnit {Δ : PortBoundary} (W : T.Obj Δ) : T.map (PortBoundary.Equiv.tensorEmptyLeft Δ).toHom (T.par unit W) = W
• par_rightUnit {Δ : PortBoundary} (W : T.Obj Δ) : T.map (PortBoundary.Equiv.tensorEmptyRight Δ).toHom (T.par W unit) = W

class Interaction.UC.OpenTheory.CompactClosed (T : OpenTheory) extends T.Monoidal : Type (max 1 u)

CompactClosed T extends Monoidal T with a coevaluation morphism (idWire) and laws that connect it to wire and plug.

The idWire Γ process relays messages on the boundary swap Γ ⊗ Γ. The key property wire_idWire says that wiring any process against the identity wire leaves it unchanged (zig-zag identity). Together with plug_eq_wire, this characterizes the compact closed structure.

• map_id {Δ : PortBoundary} (W : T.Obj Δ) : T.map (PortBoundary.Hom.id Δ) W = W
• map_comp {Δ₁ Δ₂ Δ₃ : PortBoundary} (g : Δ₂.Hom Δ₃) (f : Δ₁.Hom Δ₂) (W : T.Obj Δ₁) : T.map (g.comp f) W = T.map g (T.map f W)
• map_par {Δ₁ Δ₁' Δ₂ Δ₂' : PortBoundary} (f₁ : Δ₁.Hom Δ₁') (f₂ : Δ₂.Hom Δ₂') (W₁ : T.Obj Δ₁) (W₂ : T.Obj Δ₂) : T.map (f₁.tensor f₂) (T.par W₁ W₂) = T.par (T.map f₁ W₁) (T.map f₂ W₂)
• map_wire {Δ₁ Δ₁' Γ Δ₂ Δ₂' : PortBoundary} (f₁ : Δ₁.Hom Δ₁') (f₂ : Δ₂.Hom Δ₂') (W₁ : T.Obj (Δ₁.tensor Γ)) (W₂ : T.Obj (Γ.swap.tensor Δ₂)) : T.map (f₁.tensor f₂) (T.wire W₁ W₂) = T.wire (T.map (f₁.tensor (PortBoundary.Hom.id Γ)) W₁) (T.map ((PortBoundary.Hom.id Γ.swap).tensor f₂) W₂)
• map_plug {Δ₁ Δ₂ : PortBoundary} (f : Δ₁.Hom Δ₂) (W : T.Obj Δ₁) (K : T.Obj Δ₂.swap) : T.plug (T.map f W) K = T.plug W (T.map f.swap K)
• unit : T.Obj PortBoundary.empty
• par_assoc {Δ₁ Δ₂ Δ₃ : PortBoundary} (W₁ : T.Obj Δ₁) (W₂ : T.Obj Δ₂) (W₃ : T.Obj Δ₃) : T.map (PortBoundary.Equiv.tensorAssoc Δ₁ Δ₂ Δ₃).toHom (T.par (T.par W₁ W₂) W₃) = T.par W₁ (T.par W₂ W₃)
• par_comm {Δ₁ Δ₂ : PortBoundary} (W₁ : T.Obj Δ₁) (W₂ : T.Obj Δ₂) : T.map (PortBoundary.Equiv.tensorComm Δ₁ Δ₂).toHom (T.par W₁ W₂) = T.par W₂ W₁
• par_leftUnit {Δ : PortBoundary} (W : T.Obj Δ) : T.map (PortBoundary.Equiv.tensorEmptyLeft Δ).toHom (T.par unit W) = W
• par_rightUnit {Δ : PortBoundary} (W : T.Obj Δ) : T.map (PortBoundary.Equiv.tensorEmptyRight Δ).toHom (T.par W unit) = W
• idWire (Γ : PortBoundary) : T.Obj (Γ.swap.tensor Γ)

  The identity wire (coevaluation): a process on the boundary swap Γ ⊗ Γ that relays messages bidirectionally.

• plug_eq_wire {Δ : PortBoundary} (W : T.Obj Δ) (K : T.Obj Δ.swap) : T.plug W K = T.map (PortBoundary.Equiv.tensorEmptyLeft PortBoundary.empty).toHom (T.wire (T.map (PortBoundary.Equiv.tensorEmptyLeft Δ).symm.toHom W) (T.map (PortBoundary.Equiv.tensorEmptyRight Δ.swap).symm.toHom K))

  plug is derivable from wire plus boundary reshaping.

• wire_idWire (Γ : PortBoundary) {Δ₂ : PortBoundary} (W₂ : T.Obj (Γ.swap.tensor Δ₂)) : T.wire (idWire Γ) W₂ = W₂

  Left zig-zag: wiring the identity wire on the left is a no-op.

• wire_idWire_right (Γ : PortBoundary) {Δ₁ : PortBoundary} (W₁ : T.Obj (Δ₁.tensor Γ)) : T.wire W₁ (idWire Γ) = W₁

  Right zig-zag: wiring the identity wire on the right is a no-op.

• unit_eq : Monoidal.unit = T.map (PortBoundary.Equiv.tensorEmptyLeft PortBoundary.empty).toHom (idWire PortBoundary.empty)

  The monoidal unit is the coevaluation at the trivial boundary.

• wire_assoc {Δ₁ Γ₁ Γ₂ Δ₃ : PortBoundary} (W₁ : T.Obj (Δ₁.tensor Γ₁)) (W₂ : T.Obj (Γ₁.swap.tensor Γ₂)) (W₃ : T.Obj (Γ₂.swap.tensor Δ₃)) : T.wire (T.wire W₁ W₂) W₃ = T.wire W₁ (T.wire W₂ W₃)

  Wire associativity: sequential wiring can be reassociated.

  Wiring W₁ with W₂ through Γ₁ and then with W₃ through Γ₂ equals wiring W₂ with W₃ through Γ₂ first, then with W₁ through Γ₁.

• wire_par_superpose {Δ₁ Δ₂ Γ Δ₃ : PortBoundary} (W₁ : T.Obj Δ₁) (W₂ : T.Obj (Δ₂.tensor Γ)) (W₃ : T.Obj (Γ.swap.tensor Δ₃)) : T.wire (T.map (PortBoundary.Equiv.tensorAssoc Δ₁ Δ₂ Γ).symm.toHom (T.par W₁ W₂)) W₃ = T.map (PortBoundary.Equiv.tensorAssoc Δ₁ Δ₂ Δ₃).symm.toHom (T.par W₁ (T.wire W₂ W₃))

  Wire-par superposition (left): if the left factor of a parallel composition does not share a boundary with the second wire argument, it can be factored out of the wire. This is one of the axioms of traced symmetric monoidal categories.

• wire_comm {Δ₁ Γ Δ₂ : PortBoundary} (W₁ : T.Obj (Δ₁.tensor Γ)) (W₂ : T.Obj (Γ.swap.tensor Δ₂)) : T.wire W₁ W₂ = T.map (PortBoundary.Equiv.tensorComm Δ₂ Δ₁).toHom (T.wire (T.map (PortBoundary.Equiv.tensorComm Γ.swap Δ₂).toHom W₂) (T.map (PortBoundary.Equiv.tensorComm Δ₁ Γ).toHom W₁))

  Wire commutativity: the roles of the two wire factors are interchangeable up to boundary reshaping.

• plug_par_left {Δ₁ Δ₂ : PortBoundary} (W₁ : T.Obj Δ₁) (W₂ : T.Obj Δ₂) (K : T.Obj (Δ₁.tensor Δ₂).swap) : T.plug (T.par W₁ W₂) K = T.plug W₁ (T.map (PortBoundary.Equiv.tensorEmptyRight Δ₁.swap).toHom (T.wire K (T.map (PortBoundary.Equiv.tensorEmptyRight Δ₂).symm.toHom W₂)))

  Plug-par factorization (left): plugging a parallel composition against a context factors into wiring the right component into the context, then plugging the left component against the result.

  This is the "vanishing tensor" axiom of traced monoidal categories: a full contraction over a tensor boundary Δ₁ ⊗ Δ₂ decomposes into two sequential contractions, first over Δ₂ and then over Δ₁.

• plug_wire_left {Δ₁ Γ Δ₂ : PortBoundary} (W₁ : T.Obj (Δ₁.tensor Γ)) (W₂ : T.Obj (Γ.swap.tensor Δ₂)) (K : T.Obj (Δ₁.tensor Δ₂).swap) : T.plug (T.wire W₁ W₂) K = T.plug W₁ (T.wire K (T.map (PortBoundary.Equiv.tensorComm Γ.swap Δ₂).toHom W₂))

  Plug-wire factorization (left): closing a wired composition against a context factors through the left wire component.

  The right component W₂ is wired into the context K through the Δ₂ boundary, producing a plug for Δ₁ ⊗ Γ, and then W₁ is plugged against the result.

@[reducible, inline]

abbrev Interaction.UC.OpenTheory.Closed (T : OpenTheory) : Type u

Closed T is the type of closed systems in the open-composition theory T.

These are precisely the systems with no remaining exposed inputs or outputs.

@[reducible, inline]

abbrev Interaction.UC.OpenTheory.Plug (T : OpenTheory) (Δ : PortBoundary) : Type u

Plug T Δ is the type of contexts that can close a Δ-shaped open system in the theory T.

Such a context exposes the swapped boundary: it accepts what the open system emits, and emits what the open system accepts.

@[reducible, inline]

abbrev Interaction.UC.OpenTheory.close (T : OpenTheory) {Δ : PortBoundary} : T.Obj Δ → T.Plug Δ → T.Closed

Close an open system against a matching plug.

This is just the plug operation restated using the helper names Closed and Plug, which often match the UC / contextual-equivalence reading more closely than the raw swapped-boundary formulation.

@[reducible, inline]

abbrev Interaction.UC.OpenTheory.mapEquiv (T : OpenTheory) {Δ₁ Δ₂ : PortBoundary} : Δ₁.Equiv Δ₂ → T.Obj Δ₁ → T.Obj Δ₂

Transport an open system along a boundary equivalence.

This is the equivalence-level companion to map: instead of an arbitrary one-way boundary adaptation, it uses a canonical directed boundary isomorphism. In practice this is the convenient way to reassociate, swap, or drop empty boundary fragments once those facts have been expressed as PortBoundary.Equivs.

@[simp]

theorem Interaction.UC.OpenTheory.map_id {T : OpenTheory} [T.IsLawfulMap] {Δ : PortBoundary} (W : T.Obj Δ) : T.map (PortBoundary.Hom.id Δ) W = W

Adapting along the identity boundary morphism leaves an open system unchanged.

theorem Interaction.UC.OpenTheory.map_comp {T : OpenTheory} [T.IsLawfulMap] {Δ₁ Δ₂ Δ₃ : PortBoundary} (g : Δ₂.Hom Δ₃) (f : Δ₁.Hom Δ₂) (W : T.Obj Δ₁) : T.map (g.comp f) W = T.map g (T.map f W)

Adapting along a composite boundary morphism is the same as adapting in two successive steps.

@[simp]

theorem Interaction.UC.OpenTheory.mapEquiv_refl {T : OpenTheory} [T.IsLawfulMap] {Δ : PortBoundary} (W : T.Obj Δ) : T.mapEquiv (PortBoundary.Equiv.refl Δ) W = W

Mapping along the identity boundary equivalence does nothing.

theorem Interaction.UC.OpenTheory.mapEquiv_trans {T : OpenTheory} [T.IsLawfulMap] {Δ₁ Δ₂ Δ₃ : PortBoundary} (e₁ : Δ₁.Equiv Δ₂) (e₂ : Δ₂.Equiv Δ₃) (W : T.Obj Δ₁) : T.mapEquiv (e₁.trans e₂) W = T.mapEquiv e₂ (T.mapEquiv e₁ W)

Mapping along a composite boundary equivalence is the same as mapping in two successive equivalence-guided steps.

@[simp]

theorem Interaction.UC.OpenTheory.mapEquiv_symm_cancel {T : OpenTheory} [T.IsLawfulMap] {Δ₁ Δ₂ : PortBoundary} (e : Δ₁.Equiv Δ₂) (W : T.Obj Δ₁) : T.mapEquiv e.symm (T.mapEquiv e W) = W

@[simp]

theorem Interaction.UC.OpenTheory.mapEquiv_cancel_symm {T : OpenTheory} [T.IsLawfulMap] {Δ₁ Δ₂ : PortBoundary} (e : Δ₁.Equiv Δ₂) (W : T.Obj Δ₂) : T.mapEquiv e (T.mapEquiv e.symm W) = W

theorem Interaction.UC.OpenTheory.map_par {T : OpenTheory} [T.IsLawfulPar] {Δ₁ Δ₁' Δ₂ Δ₂' : PortBoundary} (f₁ : Δ₁.Hom Δ₁') (f₂ : Δ₂.Hom Δ₂') (W₁ : T.Obj Δ₁) (W₂ : T.Obj Δ₂) : T.map (f₁.tensor f₂) (T.par W₁ W₂) = T.par (T.map f₁ W₁) (T.map f₂ W₂)

Parallel composition is natural with respect to boundary adaptation.

theorem Interaction.UC.OpenTheory.mapEquiv_par {T : OpenTheory} [T.IsLawfulPar] {Δ₁ Δ₁' Δ₂ Δ₂' : PortBoundary} (e₁ : Δ₁.Equiv Δ₁') (e₂ : Δ₂.Equiv Δ₂') (W₁ : T.Obj Δ₁) (W₂ : T.Obj Δ₂) : T.mapEquiv (e₁.tensorCongr e₂) (T.par W₁ W₂) = T.par (T.mapEquiv e₁ W₁) (T.mapEquiv e₂ W₂)

Parallel composition is natural with respect to boundary equivalences.

This is the equivalence-guided companion to map_par: canonical reshaping of the left and right boundaries may be pushed inside par.

theorem Interaction.UC.OpenTheory.map_wire {T : OpenTheory} [T.IsLawfulWire] {Δ₁ Δ₁' Γ Δ₂ Δ₂' : PortBoundary} (f₁ : Δ₁.Hom Δ₁') (f₂ : Δ₂.Hom Δ₂') (W₁ : T.Obj (Δ₁.tensor Γ)) (W₂ : T.Obj (Γ.swap.tensor Δ₂)) : T.map (f₁.tensor f₂) (T.wire W₁ W₂) = T.wire (T.map (f₁.tensor (PortBoundary.Hom.id Γ)) W₁) (T.map ((PortBoundary.Hom.id Γ.swap).tensor f₂) W₂)

Partial wiring is natural with respect to boundary adaptation.

theorem Interaction.UC.OpenTheory.mapEquiv_wire {T : OpenTheory} [T.IsLawfulWire] {Δ₁ Δ₁' Γ Δ₂ Δ₂' : PortBoundary} (e₁ : Δ₁.Equiv Δ₁') (e₂ : Δ₂.Equiv Δ₂') (W₁ : T.Obj (Δ₁.tensor Γ)) (W₂ : T.Obj (Γ.swap.tensor Δ₂)) : T.mapEquiv (e₁.tensorCongr e₂) (T.wire W₁ W₂) = T.wire (T.mapEquiv (e₁.tensorCongr (PortBoundary.Equiv.refl Γ)) W₁) (T.mapEquiv ((PortBoundary.Equiv.refl Γ.swap).tensorCongr e₂) W₂)

Partial wiring is natural with respect to boundary equivalences on the still exposed outer boundaries.

As in map_wire, the shared middle boundary is held fixed in this first law layer. The point is that canonical reassociation or symmetry on the outer interfaces can already be pushed through wire without enlarging the primitive kernel of OpenTheory.

theorem Interaction.UC.OpenTheory.map_plug {T : OpenTheory} [T.IsLawfulPlug] {Δ₁ Δ₂ : PortBoundary} (f : Δ₁.Hom Δ₂) (W : T.Obj Δ₁) (K : T.Obj Δ₂.swap) : T.plug (T.map f W) K = T.plug W (T.map f.swap K)

Plugging is natural with respect to boundary adaptation.

theorem Interaction.UC.OpenTheory.mapEquiv_plug {T : OpenTheory} [T.IsLawfulPlug] {Δ₁ Δ₂ : PortBoundary} (e : Δ₁.Equiv Δ₂) (W : T.Obj Δ₁) (K : T.Obj Δ₂.swap) : T.plug (T.mapEquiv e W) K = T.plug W (T.map e.toHom.swap K)

Plugging is natural with respect to boundary equivalence.

This is the boundary-equivalence form of map_plug: if the exposed side of the open system is reshaped by a canonical directed isomorphism, the same forward boundary adaptation can be pushed across the plug after swapping directions.

The right-hand side is phrased with the swapped boundary Hom directly rather than wrapping it back into mapEquiv. That is intentional: once directions are reversed, the variance becomes clearer at the raw boundary-map level than through a second equivalence wrapper.

theorem Interaction.UC.OpenTheory.par_assoc {T : OpenTheory} [T.Monoidal] {Δ₁ Δ₂ Δ₃ : PortBoundary} (W₁ : T.Obj Δ₁) (W₂ : T.Obj Δ₂) (W₃ : T.Obj Δ₃) : T.mapEquiv (PortBoundary.Equiv.tensorAssoc Δ₁ Δ₂ Δ₃) (T.par (T.par W₁ W₂) W₃) = T.par W₁ (T.par W₂ W₃)

Reassociating a nested parallel composition of three open systems.

theorem Interaction.UC.OpenTheory.par_comm {T : OpenTheory} [T.Monoidal] {Δ₁ Δ₂ : PortBoundary} (W₁ : T.Obj Δ₁) (W₂ : T.Obj Δ₂) : T.mapEquiv (PortBoundary.Equiv.tensorComm Δ₁ Δ₂) (T.par W₁ W₂) = T.par W₂ W₁

Swapping the components of a parallel composition along the tensor commutativity equivalence.

@[simp]

theorem Interaction.UC.OpenTheory.par_leftUnit {T : OpenTheory} [T.Monoidal] {Δ : PortBoundary} (W : T.Obj Δ) : T.mapEquiv (PortBoundary.Equiv.tensorEmptyLeft Δ) (T.par Monoidal.unit W) = W

The monoidal unit is a left identity for parallel composition.

@[simp]

theorem Interaction.UC.OpenTheory.par_rightUnit {T : OpenTheory} [T.Monoidal] {Δ : PortBoundary} (W : T.Obj Δ) : T.mapEquiv (PortBoundary.Equiv.tensorEmptyRight Δ) (T.par W Monoidal.unit) = W

The monoidal unit is a right identity for parallel composition.

theorem Interaction.UC.OpenTheory.plug_eq_wire {T : OpenTheory} [T.CompactClosed] {Δ : PortBoundary} (W : T.Obj Δ) (K : T.Obj Δ.swap) : T.plug W K = T.map (PortBoundary.Equiv.tensorEmptyLeft PortBoundary.empty).toHom (T.wire (T.map (PortBoundary.Equiv.tensorEmptyLeft Δ).symm.toHom W) (T.map (PortBoundary.Equiv.tensorEmptyRight Δ.swap).symm.toHom K))

plug expressed via wire and boundary reshaping.

@[simp]

theorem Interaction.UC.OpenTheory.wire_idWire {T : OpenTheory} [T.CompactClosed] {Γ Δ₂ : PortBoundary} (W₂ : T.Obj (Γ.swap.tensor Δ₂)) : T.wire (CompactClosed.idWire Γ) W₂ = W₂

Left zig-zag: wiring the identity wire on the left is a no-op.

@[simp]

theorem Interaction.UC.OpenTheory.wire_idWire_right {T : OpenTheory} [T.CompactClosed] {Γ Δ₁ : PortBoundary} (W₁ : T.Obj (Δ₁.tensor Γ)) : T.wire W₁ (CompactClosed.idWire Γ) = W₁

Right zig-zag: wiring the identity wire on the right is a no-op.

theorem Interaction.UC.OpenTheory.unit_eq {T : OpenTheory} [T.CompactClosed] : Monoidal.unit = T.map (PortBoundary.Equiv.tensorEmptyLeft PortBoundary.empty).toHom (CompactClosed.idWire PortBoundary.empty)

The monoidal unit is the coevaluation at the trivial boundary.

Wire algebra

theorem Interaction.UC.OpenTheory.wire_par_superpose {T : OpenTheory} [T.CompactClosed] {Δ₁ Δ₂ Γ Δ₃ : PortBoundary} (W₁ : T.Obj Δ₁) (W₂ : T.Obj (Δ₂.tensor Γ)) (W₃ : T.Obj (Γ.swap.tensor Δ₃)) : T.wire (T.mapEquiv (PortBoundary.Equiv.tensorAssoc Δ₁ Δ₂ Γ).symm (T.par W₁ W₂)) W₃ = T.mapEquiv (PortBoundary.Equiv.tensorAssoc Δ₁ Δ₂ Δ₃).symm (T.par W₁ (T.wire W₂ W₃))

Wire-par superposition: the left factor of a parallel composition can be moved outside a wire when it doesn't share the contracted boundary.

theorem Interaction.UC.OpenTheory.wire_assoc {T : OpenTheory} [T.CompactClosed] {Δ₁ Γ₁ Γ₂ Δ₃ : PortBoundary} (W₁ : T.Obj (Δ₁.tensor Γ₁)) (W₂ : T.Obj (Γ₁.swap.tensor Γ₂)) (W₃ : T.Obj (Γ₂.swap.tensor Δ₃)) : T.wire (T.wire W₁ W₂) W₃ = T.wire W₁ (T.wire W₂ W₃)

Wire associativity: sequential wiring can be reassociated.

theorem Interaction.UC.OpenTheory.wire_comm {T : OpenTheory} [T.CompactClosed] {Δ₁ Γ Δ₂ : PortBoundary} (W₁ : T.Obj (Δ₁.tensor Γ)) (W₂ : T.Obj (Γ.swap.tensor Δ₂)) : T.wire W₁ W₂ = T.mapEquiv (PortBoundary.Equiv.tensorComm Δ₂ Δ₁) (T.wire (T.mapEquiv (PortBoundary.Equiv.tensorComm Γ.swap Δ₂) W₂) (T.mapEquiv (PortBoundary.Equiv.tensorComm Δ₁ Γ) W₁))

Wire commutativity: the roles of the two wire factors are interchangeable up to boundary reshaping.

theorem Interaction.UC.OpenTheory.plug_par_left {T : OpenTheory} [T.CompactClosed] {Δ₁ Δ₂ : PortBoundary} (W₁ : T.Obj Δ₁) (W₂ : T.Obj Δ₂) (K : T.Obj (Δ₁.tensor Δ₂).swap) : T.plug (T.par W₁ W₂) K = T.plug W₁ (T.mapEquiv (PortBoundary.Equiv.tensorEmptyRight Δ₁.swap) (T.wire K (T.mapEquiv (PortBoundary.Equiv.tensorEmptyRight Δ₂).symm W₂)))

Plug-par factorization (left): plugging a parallel composition against a context factors through the left component.

See CompactClosed.plug_par_left for the full docstring.

theorem Interaction.UC.OpenTheory.plug_wire_left {T : OpenTheory} [T.CompactClosed] {Δ₁ Γ Δ₂ : PortBoundary} (W₁ : T.Obj (Δ₁.tensor Γ)) (W₂ : T.Obj (Γ.swap.tensor Δ₂)) (K : T.Obj (Δ₁.tensor Δ₂).swap) : T.plug (T.wire W₁ W₂) K = T.plug W₁ (T.wire K (T.mapEquiv (PortBoundary.Equiv.tensorComm Γ.swap Δ₂) W₂))

Plug-wire factorization (left): closing a wired composition against a context factors through the left wire component.

See CompactClosed.plug_wire_left for the full docstring.