The sum of two set objects: the subobject (a, b) of the coproduct of their carriers, \(|a + b| = |a| + |b|\) (the join on the cardinal lattice, as for the product). Reduced where the types decide it: More...

Detailed Description

template<typename UA, typename UB>
struct dedekind::sets::sum_universe< UA, UB >

The sum of two set objects: the subobject (a, b) of the coproduct of their carriers, \(|a + b| = |a| + |b|\) (the join on the cardinal lattice, as for the product). Reduced where the types decide it:

an empty summand ( \(a + \varnothing_Y \cong a\)): the set lies in the image of one injection, a monic arrow, and pulls back along it without loss, so the ambient narrows to that summand's carrier (strength reduction, as \(a \vee \bot = a\) carried through \(\iota\)); A sum of two universes stays a sum (χ ≡ ⊤ on it) and keeps its summands, so each keeps its own cardinality.
Parameters

a,b the summands.

The universe of the sum of two universes: the coproduct carrier, the join of the species, the join of the cardinality classes (as for the product).

The documentation for this struct was generated from the following file:

src/main/modules/dedekind/sets/heterogeneous.cppm