dedekind::sets::Subobjects< T, L > Struct Template Reference

The subobjects of a carrier in a logic, \(\mathrm{Sub}(T, L)\) ( \(\mathrm{Sub}(\mathbb{A}_T)\), \(\chi\) valued in L), as an object: the domain or codomain of an arrow on sets — the complement, the pushforward along an injection. No one type is this object: every set object over the carrier in that logic presents it (the expression grammar is a type-indexed family: 𝔸, a comprehension, a Meet / Join / Not node), and the universe, its top, is the representative, so category::IsArrow checks an arrow on sets at the universe and asks the result to be a set object over it (morphism__Objects_And_Their_Presentations). A universe's cardinality class is a bound, not part of the object. More...

Public Types
using	archetype = 𝔸<T, L>

Static Public Attributes
template<typename S>
static constexpr bool	presents

Detailed Description

template<typename T, IsOckhamAlgebra L = Boole>
struct dedekind::sets::Subobjects< T, L >

The subobjects of a carrier in a logic, \(\mathrm{Sub}(T, L)\) ( \(\mathrm{Sub}(\mathbb{A}_T)\), \(\chi\) valued in L), as an object: the domain or codomain of an arrow on sets — the complement, the pushforward along an injection. No one type is this object: every set object over the carrier in that logic presents it (the expression grammar is a type-indexed family: 𝔸, a comprehension, a Meet / Join / Not node), and the universe, its top, is the representative, so category::IsArrow checks an arrow on sets at the universe and asks the result to be a set object over it (morphism__Objects_And_Their_Presentations). A universe's cardinality class is a bound, not part of the object.

Template Parameters

T	the carrier.
L	the logic species.

Member Data Documentation

presents

template<typename T, IsOckhamAlgebra L = Boole>

template<typename S>

bool dedekind::sets::Subobjects< T, L >::presents

staticconstexpr

Initial value:

= requires {
    requires IsSetObject<S>;
    requires std::same_as<typename S::Domain, T>;
    requires std::same_as<typename S::logic_species, L>;
  }

---

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

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