Membership of a sum: the copairing \([\chi_a, \chi_b]\), each answer lifted into the join of the summands' species. A named functor (the product's dual is the meet of its cylinders, ProductMembership).
More...
Public Types | |
| using | logic_species |
Public Member Functions | |
| constexpr logic_species::Ω | operator() (const std::variant< typename A::Domain, typename B::Domain > &v) const |
| χ at a value of the sum, the coproduct of the carriers. | |
Public Attributes | |
| A | a |
| B | b |
Detailed Description
struct dedekind::sets::SumMembership< A, B >
Membership of a sum: the copairing \([\chi_a, \chi_b]\), each answer lifted into the join of the summands' species. A named functor (the product's dual is the meet of its cylinders, ProductMembership).
expressions__Sums
A binary operation over set objects on different carriers lands in their sum (#1039): the ambient is the coproduct std::variant<X, Y> (tagged: a value is in one summand), and \(\mathrm{Sub}(X + Y) \cong \mathrm{Sub}(X)
\times \mathrm{Sub}(Y)\), natural in X, Y, for every species (the coproduct's universal property on \(\chi : X + Y \to \Omega\)). So a set of the sum is a pair of sets: a | b is (a, b), its χ the copairing \([\chi_a, \chi_b]\), and its restrictions to the summands give a / b back. The isomorphism is one of lattices: a pair of sets is no set, and the set a | b is, as an object, the coproduct a + b (IsCoproduct on the carrier), not a product. a & b meets in the same ambient: the summands are disjoint, so it is Ø. The ℕ / ℤ pair keeps its widening union (NatZedPair): ℕ embeds in ℤ, an identification the tagged sum does not make.
Member Typedef Documentation
◆ logic_species
| using dedekind::sets::SumMembership< A, B >::logic_species |
The documentation for this struct was generated from the following file:
- src/main/modules/dedekind/sets/heterogeneous.cppm
