UC interfaces and open boundaries

This file introduces the smallest structural layer for open concurrent systems.

The current concurrent semantic center, ProcessOver, describes closed residual processes whose step protocols already live inside the system. For UC-style openness, contextual plugging, and general interaction with an environment, we also need a typed notion of:

• what traffic may enter a component,
• what traffic may leave it, and
• how such open boundaries compose.

The design here is intentionally minimal and purely structural. Every definition is an abbrev over existing PFunctor / chart / lens machinery, so the established theory is reused definitionally while presenting names that read naturally in the interaction setting.

• Interface is PFunctor: ports A and per-port messages B a.
• Interface.Packet I is one concrete boundary message on interface I.
• Interface.Hom I J is PFunctor.Chart I J (forward packet transport, covariant on both components).
• Interface.QueryHom I J is PFunctor.Lens I J (query retargeting with response pullback, contravariant on the fibre).
• Interface.Equiv I J is the chart-level interface isomorphism.
• Interface.comp I J is the composition monoidal product on polynomial functors (PFunctor.comp), modelling sequential dependence where one interface's response determines the next interface's port.
• Interface.compUnit is the composition unit (the identity polynomial functor: one port, one message).
• PortBoundary is a directed pair of input and output interfaces.
• PortBoundary.swap, tensor, empty, and PortBoundary.Hom are the basic operations for open composition.

The most important distinction in this file is:

• Hom acts on packets that have already been produced.
• QueryHom acts on one-step observations / queries that are still waiting for a response.

So Hom pushes traffic forward, while QueryHom retargets an interaction and pulls the eventual response back. The composition product is only functorial for QueryHom (lenses), not for Hom (charts), because the fibre-level map must be contravariant.

This file also introduces the first equivalence layer:

• Interface.Equiv for interface isomorphisms, and
• PortBoundary.Equiv for the corresponding variance-aware isomorphisms of directed open boundaries.

These structures are the starting point for expressing tensor unit, associativity, and symmetry at the boundary level without hard-coding more primitive operations into OpenTheory.

This file does not yet define open worlds, plugging, or runtime semantics. Those later layers should build on these typed boundary primitives rather than re-introducing their own packet/interface vocabulary.

References

• Niu, Spivak (2024), Polynomial Functors: A Mathematical Theory of Interaction — the composition product, charts, lenses, and monoidal structures on polynomial functors used throughout this file

@[reducible, inline]

abbrev Interaction.UC.Interface : Type (max (u_1 + 1) (u_2 + 1))

Interface is the interaction-facing name for PFunctor.

An interface packages:

• a type of ports A, and
• for each port a : A, a type of messages B a.

This is the same dependent-container structure already used throughout the existing PFunctor world. The point of the new name is only to reflect the intended reading: these are typed communication interfaces.

@[reducible, inline]

abbrev Interaction.UC.Interface.Packet (I : Interface) : Type (max uA uB)

Packet I is one concrete message on interface I.

It consists of:

• a chosen port a : I.A, and
• a message m : I.B a carried on that port.

This is exactly PFunctor.Idx I, reused under a boundary-oriented name.

@[reducible, inline]

abbrev Interaction.UC.Interface.Query (I : Interface) (α : Type vA) : Type (max uA uB vA)

Query I α is the continuation-bearing one-step query shape induced by the interface I.

Unlike Packet I, which is just a concrete boundary message, Query I α already stores a continuation returning values of type α. So Query is the right bridge back to the existing PFunctor / oracle world: it does not represent traffic that has already happened, but a one-step interaction that is still waiting for a response.

This is exactly why the interface layer needs two different morphism notions:

• Hom, for translating packets that already exist, and
• QueryHom, for retargeting a query while reinterpreting its eventual response.

At the PFunctor level, this is also the distinction between:

• PFunctor.Chart, which transports concrete packets forward, and
• PFunctor.Lens, which transports continuation-bearing queries.

@[reducible, inline]

abbrev Interaction.UC.Interface.Hom (I : Interface) (J : Interface) : Type (max (max (max uA vA) uB) vB)

Hom I J is the boundary-facing name for PFunctor.Chart I J.

A chart translates concrete packets forward from I to J:

• toFunA maps ports, and
• toFunB maps messages along the translated port.

In more operational terms, Hom answers the question:

if a packet actually appears on interface I, how should it be viewed as a packet on interface J?

So Hom is the structural notion of interface adaptation used for concrete boundary traffic. When later layers need continuation-preserving interface maps, they should use QueryHom instead.

@[reducible, inline]

abbrev Interaction.UC.Interface.Equiv (I : Interface) (J : Interface) : Type (max (max (max uA vA) uB) vB)

Equiv I J is the structural notion of interface isomorphism.

Unlike a plain Hom, which only translates packets forward, an Interface.Equiv records an actual equivalence of ports together with an equivalence of messages over each translated port.

This is intentionally based on the existing PFunctor.Equiv representation rather than on chart isomorphisms. For the boundary layer, the stronger structural equivalence is more convenient: the standard coproduct and tensor coherence facts already live at this level, and packet/query translations can be recovered from it when needed.

@[reducible, inline]

abbrev Interaction.UC.Interface.QueryHom (I : Interface) (J : Interface) : Type (max (max (max uA vA) uB) vB)

QueryHom I J is the boundary-facing name for PFunctor.Lens I J.

A query hom translates continuation-bearing queries from I to J:

• toFunA maps the queried port, and
• toFunB reinterprets a response on the translated port back as a response on the original port.

In more operational terms, QueryHom answers the question:

if a component wants to query interface I, how should that query be retargeted to interface J, and how should the eventual response be turned back into an I-response?

So charts are the right notion for concrete packets, while query homs are the right notion for one-step interactive behavior. This is why the message map in QueryHom goes in the opposite direction from Hom: queries move outward, but their responses must be pulled back. The same underlying representation is still PFunctor.Lens; the new name is only there to make the interaction-level role of the abstraction immediately legible.

@[reducible, inline]

abbrev Interaction.UC.Interface.Hom.onPort {I : Interface} {J : Interface} (f : I.Hom J) : I.A → J.A

The port component of an interface chart.

This is the interaction-facing name for PFunctor.Chart.toFunA.

@[reducible, inline]

abbrev Interaction.UC.Interface.Hom.onMsg {I : Interface} {J : Interface} (f : I.Hom J) {a : I.A} : I.B a → J.B (f.onPort a)

The message component of an interface chart.

For each source port a, onMsg translates a concrete message on a into a message on the translated target port f.onPort a.

So onMsg moves in the same direction as the packet itself. This is the interaction-facing name for PFunctor.Chart.toFunB.

@[reducible, inline]

abbrev Interaction.UC.Interface.Hom.id (I : Interface) : I.Hom I

The identity interface translation.

@[reducible, inline]

abbrev Interaction.UC.Interface.Hom.comp {I : Interface} {J : Interface} {K : Interface} (g : J.Hom K) (f : I.Hom J) : I.Hom K

Compose two interface translations.

comp g f first translates packets along f, then along g.

def Interaction.UC.Interface.Hom.mapPacket {I : Interface} {J : Interface} (f : I.Hom J) : I.Packet → J.Packet

Translate one concrete packet along an interface morphism.

@[simp]

theorem Interaction.UC.Interface.Hom.id_comp {I : Interface} {J : Interface} (f : I.Hom J) : (id J).comp f = f

@[simp]

theorem Interaction.UC.Interface.Hom.comp_id {I : Interface} {J : Interface} (f : I.Hom J) : f.comp (id I) = f

theorem Interaction.UC.Interface.Hom.comp_assoc {I : Interface} {J : Interface} {K : Interface} {L : Interface} (h : K.Hom L) (g : J.Hom K) (f : I.Hom J) : h.comp (g.comp f) = (h.comp g).comp f

@[simp]

theorem Interaction.UC.Interface.Hom.mapPacket_id {I : Interface} : (id I).mapPacket = fun (p : I.Packet) => p

@[simp]

theorem Interaction.UC.Interface.Hom.mapPacket_comp {I : Interface} {J : Interface} {K : Interface} (g : J.Hom K) (f : I.Hom J) : (g.comp f).mapPacket = g.mapPacket ∘ f.mapPacket

@[reducible, inline]

abbrev Interaction.UC.Interface.QueryHom.onPort {I : Interface} {J : Interface} (f : I.QueryHom J) : I.A → J.A

The port component of an interface query hom.

This is the interaction-facing name for PFunctor.Lens.toFunA.

@[reducible, inline]

abbrev Interaction.UC.Interface.QueryHom.onMsg {I : Interface} {J : Interface} (f : I.QueryHom J) (a : I.A) : J.B (f.onPort a) → I.B a

The message-response component of an interface query hom.

For each queried source port a, onMsg reinterprets a response on the translated target port f.onPort a back as a response on the original port a.

So onMsg moves in the opposite direction from the retargeted query: the query goes out to J, and the response is pulled back to I. This is the interaction-facing name for PFunctor.Lens.toFunB.

@[reducible, inline]

abbrev Interaction.UC.Interface.QueryHom.id (I : Interface) : I.QueryHom I

The identity interface query hom.

@[reducible, inline]

abbrev Interaction.UC.Interface.QueryHom.comp {I : Interface} {J : Interface} {K : Interface} (g : J.QueryHom K) (f : I.QueryHom J) : I.QueryHom K

Compose two interface query homs.

comp g f first transports a query along f, then transports the resulting query along g.

def Interaction.UC.Interface.QueryHom.mapQuery {I : Interface} {J : Interface} {α : Type wA} (f : I.QueryHom J) : I.Query α → J.Query α

Translate one continuation-bearing query along an interface query hom.

If a query asks for a response on interface I, then mapQuery f retargets that query to interface J and uses the query hom to reinterpret the eventual response back on the original side.

So mapQuery is the query-level companion to Hom.mapPacket:

• Hom.mapPacket changes traffic that already exists;
• QueryHom.mapQuery changes the interface against which a pending interaction is asked.

@[simp]

theorem Interaction.UC.Interface.QueryHom.id_comp {I : Interface} {J : Interface} (f : I.QueryHom J) : (id J).comp f = f

@[simp]

theorem Interaction.UC.Interface.QueryHom.comp_id {I : Interface} {J : Interface} (f : I.QueryHom J) : f.comp (id I) = f

theorem Interaction.UC.Interface.QueryHom.comp_assoc {I : Interface} {J : Interface} {K : Interface} {L : Interface} (h : K.QueryHom L) (g : J.QueryHom K) (f : I.QueryHom J) : h.comp (g.comp f) = (h.comp g).comp f

@[simp]

theorem Interaction.UC.Interface.QueryHom.mapQuery_id {I : Interface} {α : Type wA} : (id I).mapQuery = fun (q : I.Query α) => q

@[simp]

theorem Interaction.UC.Interface.QueryHom.mapQuery_comp {I : Interface} {J : Interface} {K : Interface} {α : Type wA} (g : J.QueryHom K) (f : I.QueryHom J) : (g.comp f).mapQuery = g.mapQuery ∘ f.mapQuery

@[reducible, inline]

abbrev Interaction.UC.Interface.empty : Interface

The empty interface with no ports and therefore no packets.

@[reducible, inline]

abbrev Interaction.UC.Interface.sum (I : Interface) (J : Interface) : Interface

Disjoint sum of interfaces.

A packet on sum Σ Τ is either:

• a packet on Σ, tagged by Sum.inl, or
• a packet on Τ, tagged by Sum.inr.

This is the structural operation used later for side-by-side composition of open boundaries.

This is just the ordinary coproduct of polynomial functors. To keep the representation definitionally simple, both sides share the same message universe. That is already the regime used by the current open-composition layer, so no extra universe-lifting machinery is needed here.

def Interaction.UC.Interface.Hom.sum {I₁ : Interface} {I₂ : Interface} {J₁ : Interface} {J₂ : Interface} (f₁ : I₁.Hom J₁) (f₂ : I₂.Hom J₂) : (I₁.sum I₂).Hom (J₁.sum J₂)

Combine two interface charts side by side.

The resulting chart acts independently on the left and right summands of the disjoint-sum interface.

@[simp]

theorem Interaction.UC.Interface.Hom.sum_id {I₁ : Interface} {I₂ : Interface} : (id I₁).sum (id I₂) = id (I₁.sum I₂)

theorem Interaction.UC.Interface.Hom.sum_comp {I₁ : Interface} {I₂ : Interface} {J₁ : Interface} {J₂ : Interface} {K₁ : Interface} {K₂ : Interface} (g₁ : J₁.Hom K₁) (f₁ : I₁.Hom J₁) (g₂ : J₂.Hom K₂) (f₂ : I₂.Hom J₂) : (g₁.comp f₁).sum (g₂.comp f₂) = (g₁.sum g₂).comp (f₁.sum f₂)

def Interaction.UC.Interface.Hom.inl (I₁ : Interface) (I₂ : Interface) : I₁.Hom (I₁.sum I₂)

Left inclusion into a disjoint sum of interfaces.

Maps a packet on I₁ to the left summand of sum I₁ I₂.

def Interaction.UC.Interface.Hom.inr (I₁ : Interface) (I₂ : Interface) : I₂.Hom (I₁.sum I₂)

Right inclusion into a disjoint sum of interfaces.

Maps a packet on I₂ to the right summand of sum I₁ I₂.

@[simp]

theorem Interaction.UC.Interface.Hom.mapPacket_inl (I₁ : Interface) (I₂ : Interface) (pkt : I₁.Packet) : (inl I₁ I₂).mapPacket pkt = ⟨Sum.inl pkt.fst, pkt.snd⟩

@[simp]

theorem Interaction.UC.Interface.Hom.mapPacket_inr (I₁ : Interface) (I₂ : Interface) (pkt : I₂.Packet) : (inr I₁ I₂).mapPacket pkt = ⟨Sum.inr pkt.fst, pkt.snd⟩

@[simp]

theorem Interaction.UC.Interface.Hom.comp_sum_inl {I₁ : Interface} {I₂ : Interface} {J₁ : Interface} {J₂ : Interface} (f₁ : I₁.Hom J₁) (f₂ : I₂.Hom J₂) : (f₁.sum f₂).comp (inl I₁ I₂) = (inl J₁ J₂).comp f₁

@[simp]

theorem Interaction.UC.Interface.Hom.comp_sum_inr {I₁ : Interface} {I₂ : Interface} {J₁ : Interface} {J₂ : Interface} (f₁ : I₁.Hom J₁) (f₂ : I₂.Hom J₂) : (f₁.sum f₂).comp (inr I₁ I₂) = (inr J₁ J₂).comp f₂

@[reducible, inline]

abbrev Interaction.UC.Interface.QueryHom.sum {I₁ : Interface} {I₂ : Interface} {J₁ : Interface} {J₂ : Interface} (f₁ : I₁.QueryHom J₁) (f₂ : I₂.QueryHom J₂) : (I₁.sum I₂).QueryHom (J₁.sum J₂)

Combine two interface query homs side by side.

The resulting query hom retargets left and right coproduct queries independently.

@[simp]

theorem Interaction.UC.Interface.QueryHom.sum_id {I₁ : Interface} {I₂ : Interface} : (id I₁).sum (id I₂) = id (I₁.sum I₂)

theorem Interaction.UC.Interface.QueryHom.sum_comp {I₁ : Interface} {I₂ : Interface} {J₁ : Interface} {J₂ : Interface} {K₁ : Interface} {K₂ : Interface} (g₁ : J₁.QueryHom K₁) (f₁ : I₁.QueryHom J₁) (g₂ : J₂.QueryHom K₂) (f₂ : I₂.QueryHom J₂) : (g₁.comp f₁).sum (g₂.comp f₂) = (g₁.sum g₂).comp (f₁.sum f₂)

@[reducible, inline]

abbrev Interaction.UC.Interface.Equiv.toHom {I : Interface} {J : Interface} (e : I.Equiv J) : I.Hom J

The forward packet translation carried by an interface equivalence.

@[reducible, inline]

abbrev Interaction.UC.Interface.Equiv.invHom {I : Interface} {J : Interface} (e : I.Equiv J) : J.Hom I

The inverse packet translation carried by an interface equivalence.

@[reducible, inline]

abbrev Interaction.UC.Interface.Equiv.refl (I : Interface) : I.Equiv I

The identity interface equivalence.

@[reducible, inline]

abbrev Interaction.UC.Interface.Equiv.symm {I : Interface} {J : Interface} (e : I.Equiv J) : J.Equiv I

Reverse an interface equivalence.

@[reducible, inline]

abbrev Interaction.UC.Interface.Equiv.trans {I : Interface} {J : Interface} {K : Interface} (e₁ : I.Equiv J) (e₂ : J.Equiv K) : I.Equiv K

Compose two interface equivalences.

trans e₁ e₂ first changes the interface along e₁, then along e₂.

def Interaction.UC.Interface.Equiv.sumCongr {I₁ : Interface} {I₂ : Interface} {J₁ : Interface} {J₂ : Interface} (e₁ : I₁.Equiv J₁) (e₂ : I₂.Equiv J₂) : (I₁.sum I₂).Equiv (J₁.sum J₂)

Interface equivalence is preserved under disjoint sum.

@[simp]

theorem Interaction.UC.Interface.Equiv.toHom_sumCongr {I₁ : Interface} {I₂ : Interface} {J₁ : Interface} {J₂ : Interface} (e₁ : I₁.Equiv J₁) (e₂ : I₂.Equiv J₂) : (e₁.sumCongr e₂).toHom = e₁.toHom.sum e₂.toHom

The forward packet translation of sumCongr is exactly the coproduct of the forward packet translations on each summand.

def Interaction.UC.Interface.Equiv.emptySum (I : Interface) : (empty.sum I).Equiv I

The empty interface is a left unit for disjoint sum.

def Interaction.UC.Interface.Equiv.sumEmpty (I : Interface) : (I.sum empty).Equiv I

The empty interface is a right unit for disjoint sum.

def Interaction.UC.Interface.Equiv.sumComm (I : Interface) (J : Interface) : (I.sum J).Equiv (J.sum I)

Disjoint sum of interfaces is commutative up to equivalence.

def Interaction.UC.Interface.Equiv.sumAssoc (I : Interface) (J : Interface) (K : Interface) : ((I.sum J).sum K).Equiv (I.sum (J.sum K))

Disjoint sum of interfaces is associative up to equivalence.

@[reducible, inline]

abbrev Interaction.UC.Interface.comp (I : Interface) (J : Interface) : Interface

Composition product of interfaces (the composition monoidal product on polynomial functors; see Niu–Spivak 2024).

A position of comp I J is a pair of:

• a port a : I.A on the outer interface, and
• for each response m : I.B a on that port, a port of the inner interface: a function I.B a → J.A.

A direction at a composed position ⟨a, f⟩ is a dependent pair ⟨u, v⟩ where u : I.B a is a response on port a and v : J.B (f u) is a response on the resulting inner port.

This models sequential dependence: one interface's response determines which port of the next interface is activated.

@[reducible, inline]

abbrev Interaction.UC.Interface.compUnit : Interface

The monoidal unit for the composition product.

This is the polynomial functor with one port carrying one message: comp I compUnit ≃ I ≃ comp compUnit I.

@[reducible, inline]

abbrev Interaction.UC.Interface.QueryHom.compMap {I₁ : Interface} {I₂ : Interface} {J₁ : Interface} {J₂ : Interface} (f₁ : I₁.QueryHom J₁) (f₂ : I₂.QueryHom J₂) : (I₁.comp I₂).QueryHom (J₁.comp J₂)

Bifunctorial action of query homs on the composition product.

Given query homs f₁ : QueryHom I₁ J₁ and f₂ : QueryHom I₂ J₂, produces a query hom on the composed interfaces.

There is no corresponding Hom.compMap because charts (covariant on both components) are not functorial for the composition product; the composition product requires contravariance on B, which only lenses provide.

@[reducible, inline]

abbrev Interaction.UC.Interface.Equiv.compAssoc (I : Interface) (J : Interface) (K : Interface) : ((I.comp J).comp K).Equiv (I.comp (J.comp K))

The composition product is associative up to interface equivalence.

@[reducible, inline]

abbrev Interaction.UC.Interface.Equiv.compUnitRight (I : Interface) : (I.comp compUnit).Equiv I

compUnit is a right unit for composition.

@[reducible, inline]

abbrev Interaction.UC.Interface.Equiv.compUnitLeft (I : Interface) : (compUnit.comp I).Equiv I

compUnit is a left unit for composition.

structure Interaction.UC.PortBoundary : Type 1

PortBoundary is a directed open boundary for a component or world.

• In is the interface of packets accepted from the outside.
• Out is the interface of packets emitted to the outside.

The direction matters: later plugging and contextual composition should not identify incoming and outgoing traffic.

• In : Interface
• Out : Interface

def Interaction.UC.PortBoundary.empty : PortBoundary

The empty open boundary: no inputs and no outputs.

def Interaction.UC.PortBoundary.swap (Δ : PortBoundary) : PortBoundary

Swap the direction of a boundary.

This is the structural operation underlying plugging: the outputs expected by one side become inputs for the other, and vice versa.

def Interaction.UC.PortBoundary.tensor (Δ₁ Δ₂ : PortBoundary) : PortBoundary

Side-by-side composition of open boundaries.

Inputs and outputs are combined by disjoint sum, so the resulting boundary exposes both components in parallel.

structure Interaction.UC.PortBoundary.Hom (Δ₁ Δ₂ : PortBoundary) : Type

PortBoundary.Hom Δ₁ Δ₂ is a structural adaptation from boundary Δ₁ to boundary Δ₂.

The variance matches the operational reading:

• inputs are contravariant: a consumer of Δ₂.In can be fed by packets from Δ₁.In only if we know how to translate Δ₂-inputs back into Δ₁-inputs;
• outputs are covariant: packets produced on Δ₁.Out are translated forward into Δ₂.Out.

This is the boundary-level notion later used for interface adaptation and structural plugging.

• onIn : Δ₂.In.Hom Δ₁.In
• onOut : Δ₁.Out.Hom Δ₂.Out

theorem Interaction.UC.PortBoundary.Hom.ext {Δ₁ Δ₂ : PortBoundary} (f g : Δ₁.Hom Δ₂) (hIn : f.onIn = g.onIn) (hOut : f.onOut = g.onOut) : f = g

Two boundary adaptations are equal when their input and output interface maps are equal.

theorem Interaction.UC.PortBoundary.Hom.ext_iff {Δ₁ Δ₂ : PortBoundary} {f g : Δ₁.Hom Δ₂} : f = g ↔ f.onIn = g.onIn ∧ f.onOut = g.onOut

def Interaction.UC.PortBoundary.Hom.tensor {Δ₁ Δ₂ Δ₁' Δ₂' : PortBoundary} (f₁ : Δ₁.Hom Δ₁') (f₂ : Δ₂.Hom Δ₂') : (Δ₁.tensor Δ₂).Hom (Δ₁'.tensor Δ₂')

Combine two boundary adaptations side by side.

This is the boundary-level companion to PortBoundary.tensor: the left and right adaptations act independently on the corresponding summands.

def Interaction.UC.PortBoundary.Hom.swap {Δ₁ Δ₂ : PortBoundary} (f : Δ₁.Hom Δ₂) : Δ₂.swap.Hom Δ₁.swap

Swap the direction of a boundary adaptation.

This is the structural boundary-level counterpart of PortBoundary.swap: incoming and outgoing interface maps exchange roles.

def Interaction.UC.PortBoundary.Hom.id (Δ : PortBoundary) : Δ.Hom Δ

The identity boundary adaptation.

def Interaction.UC.PortBoundary.Hom.comp {Δ₁ Δ₂ Δ₃ : PortBoundary} (g : Δ₂.Hom Δ₃) (f : Δ₁.Hom Δ₂) : Δ₁.Hom Δ₃

Compose two boundary adaptations.

comp g f first adapts Δ₁ to Δ₂, then adapts Δ₂ to Δ₃.

@[simp]

theorem Interaction.UC.PortBoundary.Hom.id_comp {Δ₁ Δ₂ : PortBoundary} (f : Δ₁.Hom Δ₂) : (id Δ₂).comp f = f

@[simp]

theorem Interaction.UC.PortBoundary.Hom.comp_id {Δ₁ Δ₂ : PortBoundary} (f : Δ₁.Hom Δ₂) : f.comp (id Δ₁) = f

theorem Interaction.UC.PortBoundary.Hom.comp_assoc {Δ₁ Δ₂ Δ₃ Δ₄ : PortBoundary} (h : Δ₃.Hom Δ₄) (g : Δ₂.Hom Δ₃) (f : Δ₁.Hom Δ₂) : h.comp (g.comp f) = (h.comp g).comp f

@[simp]

theorem Interaction.UC.PortBoundary.Hom.tensor_id {Δ₁ Δ₂ : PortBoundary} : (id Δ₁).tensor (id Δ₂) = id (Δ₁.tensor Δ₂)

theorem Interaction.UC.PortBoundary.Hom.tensor_comp {Δ₁ Δ₂ Δ₃ Δ₄ Δ₁' Δ₂' : PortBoundary} (g₁ : Δ₁'.Hom Δ₃) (f₁ : Δ₁.Hom Δ₁') (g₂ : Δ₂'.Hom Δ₄) (f₂ : Δ₂.Hom Δ₂') : (g₁.comp f₁).tensor (g₂.comp f₂) = (g₁.tensor g₂).comp (f₁.tensor f₂)

@[simp]

theorem Interaction.UC.PortBoundary.Hom.swap_id {Δ : PortBoundary} : (id Δ).swap = id Δ.swap

theorem Interaction.UC.PortBoundary.Hom.swap_comp {Δ₁ Δ₂ Δ₃ : PortBoundary} (g : Δ₂.Hom Δ₃) (f : Δ₁.Hom Δ₂) : (g.comp f).swap = f.swap.comp g.swap

@[simp]

theorem Interaction.UC.PortBoundary.Hom.swap_swap {Δ₁ Δ₂ : PortBoundary} (f : Δ₁.Hom Δ₂) : f.swap.swap = f

structure Interaction.UC.PortBoundary.Equiv (Δ₁ Δ₂ : PortBoundary) : Type

PortBoundary.Equiv Δ₁ Δ₂ is the variance-aware notion of boundary isomorphism.

It is described directly in terms of interface equivalences:

• onIn is an equivalence from Δ₂.In to Δ₁.In, reflecting the contravariant role of inputs;
• onOut is an equivalence from Δ₁.Out to Δ₂.Out, reflecting the covariant role of outputs.

This is the right structure for expressing coherence laws of open composition: the exposed boundary may change shape, but only up to a canonical directed isomorphism.

• onIn : Δ₂.In.Equiv Δ₁.In
• onOut : Δ₁.Out.Equiv Δ₂.Out

@[reducible, inline]

abbrev Interaction.UC.PortBoundary.Equiv.toHom {Δ₁ Δ₂ : PortBoundary} (e : Δ₁.Equiv Δ₂) : Δ₁.Hom Δ₂

The forward boundary adaptation carried by a boundary equivalence.

@[reducible, inline]

abbrev Interaction.UC.PortBoundary.Equiv.invHom {Δ₁ Δ₂ : PortBoundary} (e : Δ₁.Equiv Δ₂) : Δ₂.Hom Δ₁

The inverse boundary adaptation carried by a boundary equivalence.

@[reducible, inline]

abbrev Interaction.UC.PortBoundary.Equiv.refl (Δ : PortBoundary) : Δ.Equiv Δ

The identity boundary equivalence.

@[reducible, inline]

abbrev Interaction.UC.PortBoundary.Equiv.symm {Δ₁ Δ₂ : PortBoundary} (e : Δ₁.Equiv Δ₂) : Δ₂.Equiv Δ₁

Reverse a boundary equivalence.

@[reducible, inline]

abbrev Interaction.UC.PortBoundary.Equiv.trans {Δ₁ Δ₂ Δ₃ : PortBoundary} (e₁ : Δ₁.Equiv Δ₂) (e₂ : Δ₂.Equiv Δ₃) : Δ₁.Equiv Δ₃

Compose two boundary equivalences.

trans e₁ e₂ first changes the exposed boundary along e₁, then along e₂.

def Interaction.UC.PortBoundary.Equiv.tensorCongr {Δ₁ Δ₁' Δ₂ Δ₂' : PortBoundary} (e₁ : Δ₁.Equiv Δ₁') (e₂ : Δ₂.Equiv Δ₂') : (Δ₁.tensor Δ₂).Equiv (Δ₁'.tensor Δ₂')

Boundary equivalence is preserved under tensor.

@[simp]

theorem Interaction.UC.PortBoundary.Equiv.toHom_tensorCongr {Δ₁ Δ₁' Δ₂ Δ₂' : PortBoundary} (e₁ : Δ₁.Equiv Δ₁') (e₂ : Δ₂.Equiv Δ₂') : (e₁.tensorCongr e₂).toHom = e₁.toHom.tensor e₂.toHom

The forward boundary adaptation of tensorCongr is exactly the tensor of the forward boundary adaptations on each factor.

@[reducible, inline]

abbrev Interaction.UC.PortBoundary.Equiv.swapCongr {Δ₁ Δ₂ : PortBoundary} (e : Δ₁.Equiv Δ₂) : Δ₁.swap.Equiv Δ₂.swap

Swapping the direction of boundaries preserves equivalence.

@[simp]

theorem Interaction.UC.PortBoundary.Equiv.toHom_swapCongr {Δ₁ Δ₂ : PortBoundary} (e : Δ₁.Equiv Δ₂) : e.swapCongr.toHom = e.invHom.swap

The forward boundary adaptation of swapCongr is exactly the swapped forward inverse boundary adaptation.

def Interaction.UC.PortBoundary.Equiv.tensorEmptyLeft (Δ : PortBoundary) : (empty.tensor Δ).Equiv Δ

The empty boundary is a left tensor unit.

def Interaction.UC.PortBoundary.Equiv.tensorEmptyRight (Δ : PortBoundary) : (Δ.tensor empty).Equiv Δ

The empty boundary is a right tensor unit.

def Interaction.UC.PortBoundary.Equiv.tensorComm (Δ₁ Δ₂ : PortBoundary) : (Δ₁.tensor Δ₂).Equiv (Δ₂.tensor Δ₁)

Tensor of boundaries is symmetric up to equivalence.

def Interaction.UC.PortBoundary.Equiv.tensorAssoc (Δ₁ Δ₂ Δ₃ : PortBoundary) : ((Δ₁.tensor Δ₂).tensor Δ₃).Equiv (Δ₁.tensor (Δ₂.tensor Δ₃))

Tensor of boundaries is associative up to equivalence.

@[reducible, inline]

abbrev Interaction.UC.PortBoundary.Equiv.swapSwap (Δ : PortBoundary) : Δ.swap.swap.Equiv Δ

Swapping twice yields the original boundary, up to equivalence.

@[simp]

theorem Interaction.UC.PortBoundary.Equiv.symm_toHom_comp_toHom {Δ₁ Δ₂ : PortBoundary} (e : Δ₁.Equiv Δ₂) : e.symm.toHom.comp e.toHom = Hom.id Δ₁

@[simp]

theorem Interaction.UC.PortBoundary.Equiv.toHom_comp_symm_toHom {Δ₁ Δ₂ : PortBoundary} (e : Δ₁.Equiv Δ₂) : e.toHom.comp e.symm.toHom = Hom.id Δ₂

@[simp]

theorem Interaction.UC.PortBoundary.Equiv.tensorComm_comp_tensorComm (Δ₁ Δ₂ : PortBoundary) : (tensorComm Δ₂ Δ₁).toHom.comp (tensorComm Δ₁ Δ₂).toHom = Hom.id (Δ₁.tensor Δ₂)

@[simp]

theorem Interaction.UC.PortBoundary.swap_swap (Δ : PortBoundary) : Δ.swap.swap = Δ