Creation Functions

There are two versions of the coproduct constructor. Ordinarily, coproducts will be constructed from a list of structures. These structures are called the constituents of the coproduct. A single sequence argument is allowed as well to be able to create coproducts of parameterized families of structures conveniently.

Creation of Coproducts

cop< S₁, S₂, ..., Sₖ >: Str, Str, ... -> Cop, [ Map ]

cop< [ S₁, S₂, ..., Sₖ ] >: [ Str, Str, ... ] -> Cop, [ Map ]

Given a list or a sequence of two or more structures \(S_1\), \(S_2\), \(\ldots\), \(S_k\), this function creates and returns their coproduct \(C\) as well as a sequence of maps [\(m_1\), \(m_2\), \(\ldots\), \(m_k\)] that provide the injections \(m_i\colon S_i\rightarrow C\).

Creation of Coproduct Elements

Coproduct elements are usually created by the injections returned as the second return value from the cop<> constructor. The bang (!) operator may also be used but only if the type of the relevant constituent is unique for the particular coproduct.

m(e): Map, Elt -> CopElt

Given a coproduct injection map \(m\) and an element of one of the constituents of the coproduct \(C\), create the coproduct element version of \(e\).

C ! e: Cop, Elt -> CopElt

Given a coproduct \(C\) and an element \(e\) of one of the constituents of \(C\) such that the type of that constituent is unique within that coproduct, create the coproduct element version of \(e\).