Definition.idr

Sequencing Product / Existential Composition

Earlier, we said that containers describe data structures and the extension is what makes the description take form as a type inside our programming language \secref{the-extension-of-containers}. For now, we use the extension of container to define the last two operation on containers ▷ and ▶. The first one is well known and is called the “substitution product”, or “container composition”, and allows one data definition to be embedded inside another.

Definition

The sequencing product of containers $(A,\bar{A})⊳(B,\bar{B})$ is given by $((a,\bar{a}):\Sigma (a:A).\bar{A}(a)\to B,\Sigma (y:\bar{A}(a)).\bar{B}(\bar{a}(y)))$

(▷) : Container -> Container -> Container
(▷) a b =
  (x : Ex a b.request) !>
  (Σ (a.response x.ex1) (b.response . x.ex2))

We call this operation the “existential composition” because the backward part reads like “there exists $\bar{A}$ such that $\bar{B}$“.

{
	"versionAtEmbed": "0.3.4",
	"filepath": "Ink/Drawing/2025.9.28 - 23.29pm.drawing",
	"width": 500,
	"aspectRatio": 1
}