heterogeneous.cppm File Reference

Set expressions ACROSS carriers: the product \(A \times B\), the sum \(A + B\), and the one widening the library ships, ℕ ↪ ℤ. More...

#include <concepts>
#include <cstddef>
#include <functional>
#include <type_traits>
#include <utility>
#include <variant>
import dedekind.sets:terms;
import dedekind.category;

Include dependency graph for heterogeneous.cppm:

Classes
struct	dedekind::sets::universe_cardinality< 𝔸< T, L, C > >
struct	dedekind::sets::product_cardinality< Finite, Finite >
struct	dedekind::sets::product_cardinality< Finite, ℵ< N > >
struct	dedekind::sets::product_cardinality< ℵ< N >, Finite >
struct	dedekind::sets::product_cardinality< ℵ< M >, ℵ< N > >
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). More...
struct	dedekind::sets::sum_universe< 𝔸< X, LA, CA >, 𝔸< Y, LB, CB > >
struct	dedekind::sets::Inject< K, UA, UB >
	\(\exists_{\iota_K}\): a set of the summand as the set of the sum that is it on its summand and empty on the other, kept as a sum (the strength reduction a | Ø → a is the inverse direction). The left adjoint of Restrict. More...
struct	dedekind::sets::Restrict< K, UA, UB >
	\(\iota_K^{-1}\) as an arrow: the restriction, lifted into the sum's logic (a summand given in a smaller logic sits in the sum's by \(\Sigma \hookrightarrow \Omega\)). The right adjoint of Inject. Defined on every presentation restriction reaches: the sums, their lattice nodes, the boundaries. More...
struct	dedekind::category::monotone_trait< dedekind::sets::Inject< K, UA, UB >, std::less_equal<> >
	The pushforward and the pullback along an injection preserve inclusion, and \(\exists_{\iota_K} \dashv \iota_K^{-1}\): \(\iota[a] \subseteq s \iff a \subseteq \iota^{-1}(s)\), the image–preimage adjunction, for every sum; \(\iota\) monic makes the unit the identity. More...
struct	dedekind::category::monotone_trait< dedekind::sets::Restrict< K, UA, UB >, std::less_equal<> >
struct	dedekind::category::is_adjoint< dedekind::sets::Inject< K, UA, UB >, dedekind::sets::Restrict< K, UA, UB >, std::less_equal<> >
struct	dedekind::sets::detail_sum_witness::Injections< A, B >
	The injections of the coproduct std::variant<A, B> as a named operation (IsCoproduct's Op, #881): inl / inr place a value by index, so equal summands stay apart (variant<int, int>). Static members, as the concept asks for Op::inl(a) / Op::inr(b). More...

Namespaces
namespace	dedekind::sets
namespace	dedekind::category

Concepts
concept	dedekind::sets::NatZedPair
	The two carriers of the one cross-carrier pair the library ships, ℕ ↪ ℤ on the variant proxies: A is a set object over Cardinality, B one over SignedCardinality, in the same species. Any set object qualifies (a halfspace, a comprehension, a node): only χ is read.
concept	dedekind::sets::HeterogeneousPair
	Two set objects on different carriers (the ℕ / ℤ pair aside): the operands of a sum.

Typedefs
template<typename A, typename B>
using	dedekind::sets::ProductMembership
	Membership of a cartesian product: \((x, y) \in A \times B \iff x \in A \wedge y \in B\), the meet of the two cylinders \(\chi_A \circ \pi_1\) and \(\chi_B \circ \pi_2\). So \(\chi_{A \times B} = \wedge \circ (\chi_A \times \chi_B)\) and \(A \times B = (A \times Y) \cap (X \times B)\): no predicate of its own, the library's meet (in the join of the factors' species, each answer lifted) over its projections composed with the factors.
using	dedekind::sets::CanonicalIntSet = 𝔸<int>
using	dedekind::sets::CanonicalIntProductSet
using	dedekind::sets::CanonicalIntProductDomain = typename CanonicalIntProductSet::Domain
using	dedekind::sets::detail_product_witness::TF = std::remove_cvref_t<decltype(t * f)>
template<typename UA, typename UB>
using	dedekind::sets::sum_universe_t = typename sum_universe<UA, UB>::type
using	dedekind::sets::detail_sum_witness::S = std::remove_cvref_t<decltype(s)>
using	dedekind::sets::detail_sum_witness::In = Injections<bool, int>
using	dedekind::sets::detail_sum_witness::USum = sum_universe_t<𝔸<bool>, 𝔸<int>>
using	dedekind::sets::detail_sum_witness::TK = std::remove_cvref_t<decltype(tk)>
using	dedekind::sets::detail_sum_witness::In1 = Inject<1, 𝔸<bool>, 𝔸<int>>
using	dedekind::sets::detail_sum_witness::Re1 = Restrict<1, 𝔸<bool>, 𝔸<int>>
using	dedekind::sets::detail_sum_witness::FiniteInt = 𝔸<int, Boole, Finite>

Functions
template<typename A, typename B> requires NatZedPair<A, B>
constexpr auto	dedekind::sets::operator& (const A &lhs, const B &rhs)
	Cross-carrier meet: a set over ℕ & a set over ℤ → a set over ℕ (carrier strength-reduction; closes a slice of #362). The intersection is contained in ℕ, so the result carrier is Cardinality.
template<typename A, typename B> requires NatZedPair<B, A>
constexpr auto	dedekind::sets::operator& (const A &lhs, const B &rhs)
	Symmetric: a set over ℤ & a set over ℕ delegates to the canonical direction; the result still tightens to ℕ.
constexpr bool	dedekind::sets::detail::sc_is_negative_finite (const SignedCardinality &v) noexcept
	Helpers for the partial inverse of lift_cardinality_to_signed (the canonical ℕ ↪ ℤ embedding).
constexpr bool	dedekind::sets::detail::sc_is_in_natural_image (const SignedCardinality &v) noexcept
constexpr Cardinality	dedekind::sets::detail::project_signed_to_natural (const SignedCardinality &v) noexcept
template<typename A, typename B> requires NatZedPair<A, B>
constexpr auto	dedekind::sets::operator| (const A &lhs, const B &rhs)
	Cross-carrier join: a set over ℕ | a set over ℤ → a set over ℤ (carrier widening; closes a slice of #362). The union may contain negative integers from the rhs side, so the result carrier widens to ℤ.
template<typename A, typename B> requires NatZedPair<B, A>
constexpr auto	dedekind::sets::operator| (const A &lhs, const B &rhs)
	Symmetric: a set over ℤ | a set over ℕ delegates to the canonical direction; the result still widens to ℤ.
template<typename A, typename B>
constexpr ProductMembership< A, B >	dedekind::sets::product_membership (const A &a, const B &b)
	The product's membership, built from its factors.
template<typename T1, typename L1, typename P1, typename T2, typename L2, typename P2, typename C1, typename C2> requires dedekind::category::HaveLogicJoin< typename Comprehension<𝔸<T1, L1, C1>, P1>::logic_species, typename Comprehension<𝔸<T2, L2, C2>, P2>::logic_species>
constexpr auto	dedekind::sets::cartesian_product (const Comprehension< 𝔸< T1, L1, C1 >, P1 > &a, const Comprehension< 𝔸< T2, L2, C2 >, P2 > &b)
	Cartesian product of two sets: {(a,b) | a ∈ A, b ∈ B}.
template<typename A, typename LA, typename CA, typename B, typename LB, typename CB> requires dedekind::category::HaveLogicJoin<LA, LB>
constexpr auto	dedekind::sets::cartesian_product (const 𝔸< A, LA, CA > &a, const 𝔸< B, LB, CB > &b)
	\(\mathbb{A}_A \times \mathbb{A}_B = \mathbb{A}_{A\times B}\): the product of two universes is the universe over the pair carrier, in the join of the factors' species.
template<IsSetObject A, IsSetObject B>
constexpr auto	dedekind::sets::cartesian_product (const A &a, const B &b)
	Cartesian product over arbitrary set objects.
template<typename A, typename LA, typename CA, typename B, typename LB, typename CB> requires std::same_as<LA, LB>
constexpr auto	dedekind::sets::operator* (const 𝔸< A, LA, CA > &a, const 𝔸< B, LB, CB > &b)
	The universal set of products: \(\mathbb{A}_A \times \mathbb{A}_B = \mathbb{A}_{A\times B}\), spelled as the universe over the product carrier (IsProduct).
template<typename T1, typename L1, typename P1, typename T2, typename L2, typename P2, typename C1, typename C2> requires std::same_as<L1, L2>
constexpr auto	dedekind::sets::operator* (const Comprehension< 𝔸< T1, L1, C1 >, P1 > &a, const Comprehension< 𝔸< T2, L2, C2 >, P2 > &b)
	Infix sugar for cartesian product over sets.
template<IsSetObject A, IsSetObject B>
constexpr auto	dedekind::sets::operator* (const A &a, const B &b)
	Infix sugar for cartesian product over ambient species values. A set is also an arrow (its χ), and IsSetObject says so, so this overload is more constrained than the arrows' * (the product functor, category:cartesian): on sets, * is the cartesian product.
template<typename T1, typename T2, typename L, typename C, typename A, typename B>
constexpr auto	dedekind::sets::component (const Comprehension< 𝔸< std::pair< T1, T2 >, L, C >, ProductMembership< A, B > > &s, dedekind::category::At< 1 >)
	The product of two set objects is their categorical product, not only their carriers' (#970, #1039): π_1 / π_2 on A × B return the factor set objects, which the membership already carries. With the carrier-level IsProduct above and the universes' (boundaries), IsProduct<decltype(A * B), A, B> holds for set objects.
template<typename T1, typename T2, typename L, typename C, typename A, typename B>
constexpr auto	dedekind::sets::component (const Comprehension< 𝔸< std::pair< T1, T2 >, L, C >, ProductMembership< A, B > > &s, dedekind::category::At< 2 >)
template<Is𝔸 USum, IsSetObject A, IsSetObject B>
constexpr auto	dedekind::sets::sum_over (const A &a, const B &b)
	The subobject (a, b) of the sum over the universe USum, as built: no reduction. sum reduces first; the pushforward Inject never does.
template<IsSetObject A, IsSetObject B>
constexpr auto	dedekind::sets::sum (const A &a, const B &b)
template<typename A, typename B> requires HeterogeneousPair<A, B>
constexpr auto	dedekind::sets::operator| (const A &a, const B &b)
	a | b on different carriers: their sum.
template<typename A, typename B> requires HeterogeneousPair<A, B>
constexpr auto	dedekind::sets::operator& (const A &, const B &)
	a & b on different carriers: the summands of a sum are disjoint, so the meet is the empty set of the sum.
template<std::size_t K, typename X, typename Y, typename L, typename C, typename A, typename B> requires (K == 1 || K == 2)
constexpr auto	dedekind::sets::restriction (const Comprehension< 𝔸< std::variant< X, Y >, L, C >, SumMembership< A, B > > &s)
	The restriction of a set of a sum to its k-th summand, \(\iota_k^{-1}(s)\): the forward map of the lattice isomorphism \(\mathrm{Sub}(X + Y) \cong \mathrm{Sub}(X) \times \mathrm{Sub}(Y)\). A pair of sets is no set: the sum itself is the coproduct of its summands in Set, not their product, so it carries no π_k.
template<std::size_t K, typename X, typename Y, typename T2, typename L, typename C, typename A, typename B> requires (K == 1 || K == 2) && requires(const A& a) { restriction<K>(a); }
constexpr auto	dedekind::sets::restriction (const Comprehension< 𝔸< std::pair< std::variant< X, Y >, T2 >, L, C >, ProductMembership< A, B > > &r)
	A relation out of a sum restricted to one summand: \((A + B) \times C \cong A \times C + B \times C\) (distributivity), so \((\iota_k \times \mathrm{id})^{-1}(s \times c) = \iota_k^{-1}(s) \times c\). A relation Either<a, b> ⇸ c that only accepts a is the relation a ⇸ c.
template<std::size_t K, typename X, typename Y, typename L, typename C> requires (K == 1 || K == 2)
constexpr auto	dedekind::sets::restriction (const 𝔸< std::variant< X, Y >, L, C > &)
	\(\iota_K^{-1}\) is a lattice homomorphism (a pullback preserves \(\wedge, \vee, \neg, \bot, \top\)): the restriction reaches through the lattice's nodes to the sums beneath, and the boundaries restrict to the boundaries — the universe of the sum to the universe of the summand (the sum's cardinality class kept: a sound bound, the summand's own is not recorded on a bare universe), Ø to Ø.
template<std::size_t K, typename X, typename Y, typename L> requires (K == 1 || K == 2)
constexpr auto	dedekind::sets::restriction (const Ø< std::variant< X, Y >, L > &)
template<std::size_t K, typename A> requires (K == 1 || K == 2) && requires(const A& a) { restriction<K>(a); }
constexpr auto	dedekind::sets::restriction (const dedekind::category::Not< A > &n)
template<std::size_t K, typename A, typename B> requires (K == 1 || K == 2) && requires(const A& a, const B& b) { restriction<K>(a); restriction<K>(b); }
constexpr auto	dedekind::sets::restriction (const dedekind::category::Meet< A, B > &m)
template<std::size_t K, typename A, typename B> requires (K == 1 || K == 2) && requires(const A& a, const B& b) { restriction<K>(a); restriction<K>(b); }
constexpr auto	dedekind::sets::restriction (const dedekind::category::Join< A, B > &j)

Variables
constexpr auto	dedekind::sets::detail_product_witness::t = 𝔸<bool>{} & (π == true)
constexpr auto	dedekind::sets::detail_product_witness::f = 𝔸<bool>{} & (π == false)
template<typename S>
constexpr bool	dedekind::sets::is_empty_set_v = false
	Whether S is an empty set by its type (Ø).
template<typename T, typename L>
constexpr bool	dedekind::sets::is_empty_set_v< Ø< T, L > > = true
constexpr auto	dedekind::sets::detail_sum_witness::t = 𝔸<bool>{} & (π == true)
constexpr auto	dedekind::sets::detail_sum_witness::three = 𝔸<int>{} & (π == 3)
constexpr auto	dedekind::sets::detail_sum_witness::s = t | three
constexpr auto	dedekind::sets::detail_sum_witness::tk = lift_to<Kleene>(t)
constexpr auto	dedekind::sets::detail_sum_witness::seven = 𝔸<int>{} & (π == 7)
constexpr auto	dedekind::sets::detail_sum_witness::r = (t | three) * seven

Detailed Description

Set expressions ACROSS carriers: the product \(A \times B\), the sum \(A + B\), and the one widening the library ships, ℕ ↪ ℤ.

@partition :heterogeneous

Copyright

2026 The Dedekind Authors Licensed under the Apache License, Version 2.0.

heterogeneous__Scope

:expressions is the homogeneous grammar: the former, \(\wedge \vee \neg\) and their laws on the subobjects of ONE carrier. A binary operation on set objects over DIFFERENT carriers lands in a universal construction on the carriers (#1039): a * b in the product \(X \times Y\) (std::pair, IsProduct, with the factors as its legs), a | b in the sum \(X + Y\) (std::variant, IsCoproduct, the summands its restrictions), a & b across carriers the empty set of the sum. The sum's two arrows Inject / Restrict ( \(\exists_\iota \dashv \iota^{-1}\)) are the first instance of the hyperdoctrine (relational:graph). The ℕ / ℤ pair keeps its identification along the embedding (NatZedPair), the sole exception to "different carriers build a sum", pending the ℕ / ℤ re-implementation (#1035).

Wikipedia: Product (category theory), Coproduct, Extensive category.

Function Documentation

sc_is_negative_finite()

bool dedekind::sets::detail::sc_is_negative_finite ( const SignedCardinality & v )

constexprnoexcept

Helpers for the partial inverse of lift_cardinality_to_signed (the canonical ℕ ↪ ℤ embedding).

sc_is_in_natural_image(v) returns whether v lies in the image of ℕ inside SignedCardinality — equivalently, whether v is neither negative finite, -ℵ_0, nor NaZ. When that predicate holds, project_signed_to_natural(v) projects v back to Cardinality. Calling project_signed_to_natural on values outside the image violates its precondition.

This is the operational shadow of "ℕ ⊂ ℤ as a partial reverse": the injection ℕ ↪ ℤ has a partial inverse on the non-negative fragment of ℤ. std::optional is intentionally not used here — the predicate-then-project split keeps the cross-carrier operator| below in pure constexpr-friendly territory and lets the predicate be reused on the Set's branching choice.