Dedekind 0.0.0
A structuralist C++23 Module Library
Loading...
Searching...
No Matches
dedekind::sets::IsSetObjectLeaf Concept Reference
module dedekind.sets

The leaf case: a set object that carries the subobject surface itself (Definition Lwv) together with its two legs. More...

Concept definition

template<typename S>
concept dedekind::sets::IsSetObjectLeaf =
IsLSet<S> && requires(const S& s, const typename S::Domain& x) {
{ universe(s) } -> Is𝔸Of<S>;
classifier(s)(x);
}
dedekind::sets::IsSetObjectLeaf
The leaf case: a set object that carries the subobject surface itself (Definition Lwv) together with ...
Definition boundaries.cppm:551
dedekind::sets::Is𝔸Of
U is the universe leg of S: a universe over the same carrier under the same logic.
Definition boundaries.cppm:544
dedekind::sets::classifier
constexpr S classifier(const S &s)
Default classifier leg: the set is its predicate (Definition Lwv, "the predicate χ_S is the set").
Definition boundaries.cppm:448
dedekind::sets::universe
constexpr 𝔸< T, L, C > universe(const 𝔸< T, L, C > &u)
A universe is its own universe: the fixpoint of the universe leg.
Definition boundaries.cppm:433

Detailed Description

The leaf case: a set object that carries the subobject surface itself (Definition Lwv) together with its two legs.