The arrow reading of the Rosolini dominance inclusion \(\iota:\mathbb{B}\hookrightarrow\Omega\) (lift_logic): a decided bool answer embeds as the target species' poles (⊥↦False, ⊤↦True). The canonical order-PRESERVING arrow, and the covariant codomain axis of a classifier \(\chi:A\to\Omega\) (#908). More...

Public Types
using	Domain = bool
	𝔹, the decided core \(\{\bot,\top\}\).
using	Codomain = typename L::Ω
	Ω, the target answer-lattice.

Public Member Functions
constexpr Codomain	operator() (bool b) const

Detailed Description

template<typename L>
struct dedekind::category::LiftLogic< L >

The arrow reading of the Rosolini dominance inclusion \(\iota:\mathbb{B}\hookrightarrow\Omega\) (lift_logic): a decided bool answer embeds as the target species' poles (⊥↦False, ⊤↦True). The canonical order-PRESERVING arrow, and the covariant codomain axis of a classifier \(\chi:A\to\Omega\) (#908).

Where NegationArrow is the order-reversing (contravariant) arrow on Ω, LiftLogic is its monotone (covariant) sibling: it carries the Domain / Codomain typedefs that make lift_logic an IsArrow, so :posetal can register it is_monotone_v — ⊥≤⊤ maps to False≤True, an order embedding. This is exactly the lift_logic "wrapped in a typed arrow" that :topoi asks for (#846), and the covariant leg the two-axis reading (#894/#897) postcomposes onto. It is the covariant mirror of NegationArrow's antitone witness.

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

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

Public Types

Public Member Functions

Detailed Description