The embedding From ↪ To of one species' answers into another's, preserving ⊥, ⊤, ∧, ∨ and ¬ (a De Morgan embedding), so that the set complement ~ commutes with every lift. More...

Detailed Description

template<typename From, typename To>
struct dedekind::category::species_embed< From, To >

The embedding From ↪ To of one species' answers into another's, preserving ⊥, ⊤, ∧, ∨ and ¬ (a De Morgan embedding), so that the set complement ~ commutes with every lift.

Undefined unless the edge is registered. The shipped edges:

L ↪ L (identity, passes any value through);
𝔹 ↪ L for every species (the poles: Rosolini's Σ ↪ Ω);
K₃ ↪ Percent (False ↦ 0, Unknown ↦ 50, True ↦ 100; 50 is Percent's self-dual midpoint, so ¬ is preserved). Parity: an odd chain has a ¬-fixed midpoint and an even one has none, so K₃ and Percent do not embed into Chain<T> (whose ¬ is ~a): no map preserves ¬ across the parity gap. Register a new edge by specialising this struct.

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

src/main/modules/dedekind/category/logic.cppm