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.

Contents

Creation of Coproducts

cop< S1, S2, ..., Sk > : Str, Str, ... -> Cop, [ Map ]
cop< [ S1, S2, ..., Sk ] > : [ Str, Str, ... ] -> Cop, [ Map ]
Given a list or a sequence of two or more structures S1, S2, ..., Sk, this function creates and returns their coproduct C as well as a sequence of maps [m1, m2, ..., mk] that provide the injections mi: Si -> 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.
V2.28, 13 July 2023