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