Open composition algebra with monoidal coherence

This module defines OpenTheory, a boundary-indexed algebra of open systems, together with a granular hierarchy of lawfulness classes capturing increasingly strong equational properties. The split mirrors the categorical distinction between symmetric monoidal, traced symmetric monoidal (Joyal-Street-Verity), and compact closed categories.

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

Data classes (operations beyond the four primitives):

• HasUnit: a distinguished unit : Obj empty (the monoidal unit).
• HasIdWire: a coevaluation idWire : ∀ Γ, Obj (swap Γ ⊗ Γ).

Naturality (Prop classes):

• IsLawfulMap: functoriality of map (identity and composition).
• IsLawfulPar/IsLawfulWire/IsLawfulPlug: naturality of each combinator with respect to boundary adaptation.
• IsLawful: bundles all naturality laws.

Symmetric monoidal coherence:

• IsMonoidal (extends IsLawful, HasUnit): associativity, commutativity (braiding), and left/right unit laws for par.

Trace algebra (JSV traced symmetric monoidal):

• IsTraced (extends IsMonoidal): wire associativity, par-superposition, and wire commutativity.

Compact closure (snake / zig-zag):

• IsCompactClosed (extends IsTraced, HasIdWire): left and right zig-zag identities wire_idWire/wire_idWire_right and unit_eq identifying the monoidal unit with the trivial coevaluation.

Plug factorization:

• HasPlugWireFactor (extends IsCompactClosed): plug derivable from wire via the unit, and the two factorization laws relating closure of parallel and wired composites to closure of one component.

The chain IsMonoidal → IsTraced → IsCompactClosed → HasPlugWireFactor lets each model declare exactly the strength it can honestly satisfy. The free models (Expr.theory, Interp.theory) instantiate the entire chain. The process-backed openTheory in OpenProcessModel.lean instantiates only IsLawful; its monoidal coherence and snake equations hold up to OpenProcessIso, not strict equality.

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 a granular class hierarchy starting at IsLawful and continuing through IsMonoidal, IsTraced, IsCompactClosed, and HasPlugWireFactor (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.

Operation-only data classes

class Interaction.UC.OpenTheory.HasUnit (T : OpenTheory) : Type u

HasUnit T distinguishes a closed object unit : T.Obj empty, intended to play the role of the symmetric monoidal unit.

This is purely a data class. Whether unit actually behaves as a left/right unit for par (up to boundary equivalence) is the content of IsMonoidal.

• unit : T.Obj PortBoundary.empty

  The distinguished unit object on the empty boundary.

class Interaction.UC.OpenTheory.HasIdWire (T : OpenTheory) : Type (max 1 u)

HasIdWire T distinguishes a coevaluation morphism on every boundary, idWire Γ : T.Obj (swap Γ ⊗ Γ), intended to play the role of the categorical unit of duality between Γ and swap Γ.

This is purely a data class. Whether idWire actually satisfies the zig-zag (snake) identities is the content of IsCompactClosed.

• idWire (Γ : PortBoundary) : T.Obj (Γ.swap.tensor Γ)

  The identity-wire / coevaluation on boundary Γ: a process exposing swap Γ ⊗ Γ that behaves as a bidirectional relay.

Naturality (functoriality of map and naturality of par/wire/plug)

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)

Symmetric monoidal coherence

class Interaction.UC.OpenTheory.IsMonoidal (T : OpenTheory) extends T.IsLawful, T.HasUnit : Type u

IsMonoidal T extends IsLawful T and HasUnit T with the symmetric monoidal coherence laws for par: 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 HasUnit.unit W) = W
• par_rightUnit {Δ : PortBoundary} (W : T.Obj Δ) : T.map (PortBoundary.Equiv.tensorEmptyRight Δ).toHom (T.par W HasUnit.unit) = W

Trace algebra (Joyal-Street-Verity traced symmetric monoidal)

class Interaction.UC.OpenTheory.IsTraced (T : OpenTheory) extends T.IsMonoidal : Type u

IsTraced T extends IsMonoidal T with the three trace axioms of a Joyal-Street-Verity traced symmetric monoidal category, formulated for the binary wire operator: wire associativity (vanishing II), wire-par superposition, and wire commutativity (yanking via the symmetry).

These axioms make sense without HasIdWire or any snake equation: they are purely about the algebra of wire itself and how it interacts with par. A model satisfies IsTraced exactly when its wire operation behaves like a JSV trace; the existence of duals (i.e., compact closure) is a separate class layered on top.

• 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 HasUnit.unit W) = W
• par_rightUnit {Δ : PortBoundary} (W : T.Obj Δ) : T.map (PortBoundary.Equiv.tensorEmptyRight Δ).toHom (T.par W HasUnit.unit) = W
• 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.

• 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.

Compact closure (snake / zig-zag identities)

class Interaction.UC.OpenTheory.IsCompactClosed (T : OpenTheory) extends T.IsTraced, T.HasIdWire : Type (max 1 u)

IsCompactClosed T extends IsTraced T and HasIdWire T with the snake (zig-zag) identities relating the coevaluation idWire to wire, plus the identification unit_eq of the monoidal unit with the trivial coevaluation.

These laws say that swap Γ is a categorical dual of Γ, witnessed by idWire Γ as the coevaluation. In our setting the trace algebra and the duality structure are independent (since wire is a primitive, not derived from η/ε), so IsCompactClosed extends IsTraced rather than living side-by-side with it: a model that satisfies IsCompactClosed also has a JSV trace.

• 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 HasUnit.unit W) = W
• par_rightUnit {Δ : PortBoundary} (W : T.Obj Δ) : T.map (PortBoundary.Equiv.tensorEmptyRight Δ).toHom (T.par W HasUnit.unit) = W
• 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_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_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₁))
• idWire (Γ : PortBoundary) : T.Obj (Γ.swap.tensor Γ)
• wire_idWire (Γ : PortBoundary) {Δ₂ : PortBoundary} (W₂ : T.Obj (Γ.swap.tensor Δ₂)) : T.wire (HasIdWire.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₁ (HasIdWire.idWire Γ) = W₁

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

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

  The monoidal unit is the coevaluation at the trivial boundary.

Plug-wire factorization

class Interaction.UC.OpenTheory.HasPlugWireFactor (T : OpenTheory) extends T.IsCompactClosed : Type (max 1 u)

HasPlugWireFactor T extends IsCompactClosed T with the three laws identifying plug as a derived operation: plug factors through wire via the unit (plug_eq_wire), and closure of a parallel or wired composite factors through closure of one component (plug_par_left/plug_wire_left).

This is the "everything bundle" used by downstream UC composition theorems: [HasPlugWireFactor T] automatically supplies all of IsCompactClosed T, IsTraced T, IsMonoidal T, IsLawful T, HasUnit T, and HasIdWire T through the inheritance chain.

• 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 HasUnit.unit W) = W
• par_rightUnit {Δ : PortBoundary} (W : T.Obj Δ) : T.map (PortBoundary.Equiv.tensorEmptyRight Δ).toHom (T.par W HasUnit.unit) = W
• 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_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_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₁))
• idWire (Γ : PortBoundary) : T.Obj (Γ.swap.tensor Γ)
• wire_idWire (Γ : PortBoundary) {Δ₂ : PortBoundary} (W₂ : T.Obj (Γ.swap.tensor Δ₂)) : T.wire (HasIdWire.idWire Γ) W₂ = W₂
• wire_idWire_right (Γ : PortBoundary) {Δ₁ : PortBoundary} (W₁ : T.Obj (Δ₁.tensor Γ)) : T.wire W₁ (HasIdWire.idWire Γ) = W₁
• unit_eq : HasUnit.unit = T.map (PortBoundary.Equiv.tensorEmptyLeft PortBoundary.empty).toHom (HasIdWire.idWire PortBoundary.empty)
• 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.

• 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.

Symmetric monoidal coherence

theorem Interaction.UC.OpenTheory.par_assoc {T : OpenTheory} [T.IsMonoidal] {Δ₁ Δ₂ Δ₃ : 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.IsMonoidal] {Δ₁ Δ₂ : 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.IsMonoidal] {Δ : PortBoundary} (W : T.Obj Δ) : T.mapEquiv (PortBoundary.Equiv.tensorEmptyLeft Δ) (T.par HasUnit.unit W) = W

The monoidal unit is a left identity for parallel composition.

@[simp]

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

The monoidal unit is a right identity for parallel composition.

Trace algebra

theorem Interaction.UC.OpenTheory.wire_par_superpose {T : OpenTheory} [T.IsTraced] {Δ₁ Δ₂ Γ Δ₃ : 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.IsTraced] {Δ₁ Γ₁ Γ₂ Δ₃ : 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.IsTraced] {Δ₁ Γ Δ₂ : 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.

Compact closure (snake / zig-zag)

@[simp]

theorem Interaction.UC.OpenTheory.wire_idWire {T : OpenTheory} [T.IsCompactClosed] {Γ Δ₂ : PortBoundary} (W₂ : T.Obj (Γ.swap.tensor Δ₂)) : T.wire (HasIdWire.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.IsCompactClosed] {Γ Δ₁ : PortBoundary} (W₁ : T.Obj (Δ₁.tensor Γ)) : T.wire W₁ (HasIdWire.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.IsCompactClosed] : HasUnit.unit = T.map (PortBoundary.Equiv.tensorEmptyLeft PortBoundary.empty).toHom (HasIdWire.idWire PortBoundary.empty)

The monoidal unit is the coevaluation at the trivial boundary.

Plug-wire factorization

theorem Interaction.UC.OpenTheory.plug_eq_wire {T : OpenTheory} [T.HasPlugWireFactor] {Δ : 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.

theorem Interaction.UC.OpenTheory.plug_par_left {T : OpenTheory} [T.HasPlugWireFactor] {Δ₁ Δ₂ : 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 HasPlugWireFactor.plug_par_left for the full docstring.

theorem Interaction.UC.OpenTheory.plug_wire_left {T : OpenTheory} [T.HasPlugWireFactor] {Δ₁ Γ Δ₂ : 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 HasPlugWireFactor.plug_wire_left for the full docstring.