Dedekind 0.0.0
A structuralist C++23 Module Library
Loading...
Searching...
No Matches
dedekind::sequences::𝔸< T, L, C > Struct Template Referencefinal
module dedekind.sequences

The universal set over the carrier T: the terminal object ⊤ of Sub(T), the reified type constraint. More...

Collaboration diagram for dedekind::sequences::𝔸< T, L, C >:
Collaboration graph
[legend]

Classes

struct  Member
 Member-shape mirror of Subobject's: every element of T is a member of U via the always-True classifier; the wrapper carries the T-value the IsSubobject contract reads back through ι. More...

Public Types

using Domain = T
 The carrier: 𝔸 is the subobject \(T \hookrightarrow T\).
using Codomain = typename L::Ω
 The classifier's truth object L::Ω.
using cardinality_type = C
 The cardinality class of the carrier (Finite for bool, ℵ_0 by default; see default_cardinality_t).
using base_set_type = 𝔸<T, L, C>
using is_universal_boundary = void
 Tag read by the boundary-object dispatch (Ø carries its dual).
using logic_species = L
 The logic species L the classifier is valued in.
using is_terminal_object_tag = void
 𝔸 is the terminal object of the subobject poset Sub(U): the top ⊤, classified by the always-true predicate χ_U ≡ ⊤, with the unique arrow S → U from every subobject. Dual to Ø's initiality tag; opts U into :limit's IsTerminalObject (the tag-discovery branch :lattice::LatticeTop already uses). #881.

Public Member Functions

constexpr T ι (const Member &m) const
 ι: U ↣ T — the canonical identity inclusion. Every member of the universal set is by construction an element of the ambient T; ι unwraps the Member's T-value.
constexpr auto operator! () const
 The duality ¬⊤ = ⊥: the complement of the universe is Ø.
constexpr L::Ω operator<= (const 𝔸 &) const
constexpr bool operator== (const 𝔸 &) const
 Two universes over one carrier are equal (the type is the set).
template<typename L2, typename C2>
requires (!std::same_as<L2, L> || !std::same_as<C2, C>)
constexpr bool operator== (const 𝔸< T, L2, C2 > &) const
 Cross-(L, C) identity: the universe of a carrier T is the universe regardless of logic species or cardinality annotation, so 𝔸<T>{} == r holds when a complement-pair join elevates r to an 𝔸<T,L2,C2> — the same spirit as Ø's cross-carrier equality.
constexpr L::Ω operator() (const T &) const
 The axiom of total presence: χ(x) = ⊤ for every x.
template<typename D = T>
requires IsPairing<D>
constexpr L::Ω operator() (const leg_1_t< D > &, const leg_2_t< D > &) const
 χ on the components: over a product carrier the universe is the full relation, r(a, b) = r(⟨a, b⟩) (#1047).
constexpr L::Ω contains (const T &v) const
 Membership as a named query: 𝔸<T>{}.contains(v) reads more directly than 𝔸<T>{}(v) at listing sites. Returns L::Ω so the contract matches sets::Set::contains.
constexpr cardinality_type cardinality () const
 The cardinality class as a value (Finite / ℵ_0 tag).
template<HasSetComplement S>
constexpr auto operator^ (const S &s) const
 Symmetric difference with the universe is complement: \(\top \,\triangle\, S = \neg S\) (every x is in ⊤, so it is in exactly one of the two iff it is not in S). ~ is the SET complement (a set object, found by ADL at instantiation); ! would be the predicate complement, an arrow.

Static Public Attributes

static const 𝔸 χ
 The characteristic map is the set itself (χ ≡ ⊤).
template<typename Op>
static constexpr bool is_associative_v
template<typename Op>
static constexpr bool is_idempotent_v

Friends

template<typename S>
requires (!requires { typename S::T; }) && (!requires { typename S::is_variable; })
constexpr L::Ω operator<= (const S &, const 𝔸 &)

Detailed Description

template<typename T, IsOckhamAlgebra L = Boole, IsCardinality C = default_cardinality_t<T>>
struct dedekind::sequences::𝔸< T, L, C >

The universal set over the carrier T: the terminal object ⊤ of Sub(T), the reified type constraint.

Intentional but decidable: the rule "x ∈ 𝔸" always returns True. The topos-theoretic reading is direct: 𝔸 is the universal (top) set over carrier T; the subobject classifier is L::Ω. One name for the type and the value, symmetric with Ø: the value spelling is 𝔸<T>{} (paper Listing 6 reads auto 𝔹 = 𝔸<bool>{}), the type spelling 𝔸<T> (so IsSetObject<𝔸<T>>, no decltype).

Template Parameters
Tthe carrier (unconstrained on purpose: a non-regular carrier makes IsLSet / IsSet false rather than the name ill-formed).
Lthe logic species the classifier is valued in (IsOckhamAlgebra).
Cthe cardinality class (IsCardinality); defaults to default_cardinality_t.

Member Function Documentation

◆ operator<=()

template<typename T, IsOckhamAlgebra L = Boole, IsCardinality C = default_cardinality_t<T>>
L::Ω dedekind::sets::𝔸< T, L, C >::operator<= ( const 𝔸< T, L, C > & ) const
inlineconstexpr

◆ operator<=

template<typename T, IsOckhamAlgebra L = Boole, IsCardinality C = default_cardinality_t<T>>
template<typename S>
requires (!requires { typename S::T; }) && (!requires { typename S::is_variable; })
L::Ω operator<= ( const S & ,
const 𝔸< T, L, C > &  )
friend

boundaries__Lattice_Axiom_2

Everything is a part of the universe 𝔸. Constraint: Exclude Variables (which have a member T) to let symbolic expressions handle their own comparisons.

Member Data Documentation

◆ is_associative_v

template<typename T, IsOckhamAlgebra L = Boole, IsCardinality C = default_cardinality_t<T>>
template<typename Op>
bool dedekind::sets::𝔸< T, L, C >::is_associative_v
staticconstexpr
Initial value:
=
std::is_same_v<Op, std::bit_and<base_set_type>> ||
std::is_same_v<Op, std::bit_or<base_set_type>>

boundaries__Algebraic_Axioms_2

◆ is_idempotent_v

template<typename T, IsOckhamAlgebra L = Boole, IsCardinality C = default_cardinality_t<T>>
template<typename Op>
bool dedekind::sets::𝔸< T, L, C >::is_idempotent_v
staticconstexpr
Initial value:
=
std::is_same_v<Op, std::bit_and<base_set_type>> ||
std::is_same_v<Op, std::bit_or<base_set_type>>
The documentation for this struct was generated from the following file: