dedekind::sets::Comprehension< Base, Predicate > Struct Template Reference

Inheritance diagram for dedekind::sets::Comprehension< Base, Predicate >:

Collaboration diagram for dedekind::sets::Comprehension< Base, Predicate >:

Public Types
using	cardinality_type = typename datum_cardinality<Predicate, Base>::type
Public Types inherited from dedekind::sets::SetExpr< Comprehension< Base, Predicate >, Base::Domain, comprehension_logic_t< Base, Predicate > >
using	Domain
using	Codomain
using	logic_species

Public Member Functions
constexpr	Comprehension (const Base &b, Predicate p)
	Explicit two-argument constructor. Needed because SetExpr is a base class, so Comprehension is no longer an aggregate — the Comprehension{base, pred} sites (e.g. Singleton::operator|) route here instead of through aggregate init.
constexpr	Comprehension (Predicate p)
	The former over the universe of the carrier: {x ∈ 𝔸 | P} from the predicate alone (the base is default-constructible, as 𝔸<T,L> is). This is the one set former of the Δ₀ core, Comprehension<𝔸<T,L>, P>.
constexpr cardinality_type	cardinality () const
constexpr auto	operator() (const typename Base::Domain &x) const
	χ: the comprehension's characteristic map — x ∈ {S | P} ⟺ x ∈ S ∧ P(x). A comprehension is a set, so it is its own predicate (IsSet ⟹ IsPredicate).
template<typename D = typename Base::Domain> requires IsPairing<D>
constexpr auto	operator() (const leg_1_t< D > &a, const leg_2_t< D > &b) const
	χ on the components of a product carrier: a comprehension over A × B is a binary relation, and r(a, b) is r(⟨a, b⟩), the two presentations of one arrow by the product's universal property, \(\mathrm{Hom}(A\times B, \Omega) \cong \mathrm{Multi}((A, B), \Omega)\) (#1047).
template<typename U> requires (!std::same_as<std::remove_cvref_t<U>, typename Base::Domain>) && requires { requires Predicate::template admits<U>; } && (Is𝔸<Base> || std::invocable<const Base&, const U&>)
constexpr auto	operator() (const U &x) const
	Heterogeneous χ: a value of a type U the datum declares it admits (Predicate::admits) is asked unnarrowed, so Singleton<int>{1}(1.5) is False. The universe is not asked (χ_𝔸 ≡ ⊤); a proper base must itself admit U.
constexpr std::size_t	size () const
	Size when the datum carries it and the base is the whole universe: the point {p} over 𝔸<T> has size 1.
constexpr std::size_t	upper_bound () const
	The ETCS cardinality bound a datum-sized comprehension exposes to bound_meet / bound_join: its exact size.
Public Member Functions inherited from dedekind::sets::SetExpr< Comprehension< Base, Predicate >, Base::Domain, comprehension_logic_t< Base, Predicate > >
constexpr Base::Domain	ι (const Member &m) const

Public Attributes
Base	base
Predicate	predicate

Member Function Documentation

operator()()

template<typename Base, typename Predicate>

template<typename U>
requires (!std::same_as<std::remove_cvref_t<U>, typename Base::Domain>) && requires { requires Predicate::template admits<U>; } && (Is𝔸<Base> || std::invocable<const Base&, const U&>)

auto dedekind::sets::Comprehension< Base, Predicate >::operator() ( const U & x ) const

inlineconstexpr

Heterogeneous χ: a value of a type U the datum declares it admits (Predicate::admits) is asked unnarrowed, so Singleton<int>{1}(1.5) is False. The universe is not asked (χ_𝔸 ≡ ⊤); a proper base must itself admit U.

Template Parameters

U	the foreign carrier.

---

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

• src/main/modules/dedekind/sets/expressions.cppm