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

\(\exists_{\iota_K}\): a set of the summand as the set of the sum that is it on its summand and empty on the other, kept as a sum (the strength reduction a | Ø → a is the inverse direction). The left adjoint of Restrict. More...

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

Public Member Functions
template<typename S> requires dedekind::category::Presents<S, Domain>
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::Inject< K, UA, UB >

\(\exists_{\iota_K}\): a set of the summand as the set of the sum that is it on its summand and empty on the other, kept as a sum (the strength reduction a | Ø → a is the inverse direction). The left adjoint of Restrict.

Template Parameters

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

Member Typedef Documentation

Domain

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

using dedekind::sets::Inject< K, UA, UB >::Domain

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