dedekind::relational::detail_hyperdoctrine_witness::Restrict< K, UA, UB > Struct Template Reference

\(\iota_K^{-1}\) as an arrow: the restriction, lifted into the sum's logic (a summand given in a smaller logic sits in the sum's by \(\Sigma \hookrightarrow \Omega\)). The right adjoint of Inject. Defined on every presentation restriction reaches: the sums, their lattice nodes, the boundaries. More...

Public Types
using	USum = sum_universe_t<UA, UB>
using	L = typename USum::logic_species
using	Domain = Subobjects<typename USum::Domain, L>
using	Codomain

Public Member Functions
template<typename S> requires dedekind::category::Presents<S, Domain> && requires(const S& s) { restriction<K>(s); }
constexpr auto	operator() (const S &s) const

Detailed Description

template<std::size_t K, Is𝔸 UA, Is𝔸 UB>
requires (K == 1 || K == 2)
struct dedekind::relational::detail_hyperdoctrine_witness::Restrict< K, UA, UB >

\(\iota_K^{-1}\) as an arrow: the restriction, lifted into the sum's logic (a summand given in a smaller logic sits in the sum's by \(\Sigma \hookrightarrow \Omega\)). The right adjoint of Inject. Defined on every presentation restriction reaches: the sums, their lattice nodes, the boundaries.

expressions__Sum_Adjunction

The two arrows of a sum, on the objects \(\mathrm{Sub}(X, L)\) and \(\mathrm{Sub}(X + Y, L)\) (Subobjects, :boundaries; L the sum's logic): the pushforward along the injection, \(\exists_{\iota_K} : a \mapsto \iota_K[a]\) (Inject), and the pullback \(\iota_K^{-1}\) (Restrict). Both monotone, and \(\exists_{\iota_K} \dashv \iota_K^{-1}\): a Galois connection, witnessed through category::IsGaloisConnection on these objects — the arrows carry their certificates (monotone, adjoint), read by member discovery. The unit \(\iota_K^{-1}\,\iota_K[a] = a\) holds by type ( \(\iota_K\) is monic, category::Injection); the counit \(\iota_K[\iota_K^{-1} s] \subseteq s\) is witnessed at points.

Template Parameters

K	the summand.
UA,UB	the summands' universes.

Member Typedef Documentation

Codomain

template<std::size_t K, Is𝔸 UA, Is𝔸 UB>

using dedekind::sets::Restrict< K, UA, UB >::Codomain

Initial value:

 
      Subobjects<typename std::conditional_t<K == 1, UA, UB>::Domain, L>

---

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

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