dedekind/conceptdedekind_1_1category_1_1HasAxiom7SubobjectClassifier.html

template<typename S>

concept dedekind::category::HasAxiom7SubobjectClassifier =

    IsSubobject<S, typename S::Domain> && requires {

      requires IsSubobject<decltype(classify<typename S::Domain>(

                               classifier_true<typename S::Domain>())),

                           typename S::Domain>;

      requires IsSubobject<decltype(classify<typename S::Domain>(

                               classifier_false<typename S::Domain>())),

                           typename S::Domain>;

      requires IsPullback<

          decltype(pullback<Boole,

                            std::pair<typename S::Domain, typename S::Domain>>(

              id<typename S::Domain>(), id<typename S::Domain>())),

          Identity<typename S::Domain>, Identity<typename S::Domain>>;

    }

dedekind::category::HasAxiom7SubobjectClassifier
ETCS axiom 7 witness: every set is represented by a subobject.
Definition etcs.cppm:171

dedekind::category::IsPullback
The apex of a pullback square over the cospan f: X ⟶ Z, g: Y ⟶ Z: a subobject carrying the two projec...
Definition pullback.cppm:111

dedekind::category::IsSubobject
The categorical witness of a monomorphism ι: S ↣ A — a characteristic morphism χ: A → Ω together with...
Definition topoi.cppm:367

dedekind::category::classifier_false
constexpr auto classifier_false()
The contradiction / bottom predicate  over domain A: the canonical always-false classifier A → Ω,...
Definition topoi.cppm:830

dedekind::category::id
constexpr auto id()
The Identity Factory: Returns the neutral arrow for Species A.
Definition morphism.cppm:634

dedekind::category::classifier_true
constexpr auto classifier_true()
The tautology / top predicate  over domain A: the canonical always-true classifier A → Ω,...
Definition topoi.cppm:821

dedekind::category::pullback
constexpr auto pullback(F_Raw f_raw, G_Raw g_raw)
The Pullback Factory — constructs the Fiber Product X ×_Z Y.
Definition pullback.cppm:173

dedekind::category::Boole
The internal logic of the Classical Topos ({True, False}).
Definition logic.cppm:186

dedekind::category::Identity
The Identity Morphism and Functorial Witness.
Definition morphism.cppm:572