A value of the sort D is read in the sort C: the same sort, or a truth chain along the dominance into C's species (𝔹 ↪ K₃, the registered lift_logic). The one coercion of the grammar; any other pair of carriers meets through an arrow applied, never implied. More...

Concept definition

template<typename D, typename C>
concept dedekind::sets::EmbedsInto =  std::same_as<D, C> || requires {
  typename dedekind::category::classifier_logic_t<C>;
  requires std::same_as<typename dedekind::category::classifier_logic_t<C>::Ω,
                        C>;
  requires dedekind::category::LiftableInto<
      D, dedekind::category::classifier_logic_t<C>>;
}

Detailed Description

A value of the sort D is read in the sort C: the same sort, or a truth chain along the dominance into C's species (𝔹 ↪ K₃, the registered lift_logic). The one coercion of the grammar; any other pair of carriers meets through an arrow applied, never implied.

Template Parameters

D	the value's sort.
C	the sort it is read in.