The Rosolini inclusion arrow \(\iota : \Sigma \hookrightarrow \Omega\): a map between truth-objects out of the decided fragment. More...

Concept definition

template<typename E>
concept dedekind::category::IsDominanceInclusion = 
    IsArrow<E> && std::same_as<Dom<E>, bool> && IsΩ<Cod<E>>

Detailed Description

The Rosolini inclusion arrow \(\iota : \Sigma \hookrightarrow \Omega\): a map between truth-objects out of the decided fragment.

A signature-level witness for the dominance inclusion: an IsArrow whose domain is the Boolean dominance \(\Sigma = @c bool\) and whose codomain is a classifier \(\Omega\) (any IsΩ). lift_logic (category/logic.cppm) is the underlying map bool ↪ Ternary; a typed arrow wrapping it (a Domain=bool, Codomain=Ternary functor, e.g. the DominanceIota witness in topoi_test.cpp) inhabits this concept — lift_logic itself is a free function template and has no Domain / Codomain, so it is not directly an IsArrow. For an undecidable (Ω-)set this ι is a proper mono that adjoins the Unknown point; in ETCS it collapses to id ( \(\Sigma = \Omega\)). The mono/order-embedding semantics are the intent (laws exercised in tests); the concept fixes the shape Σ → Ω. See #846.

See also: G. Rosolini, Continuity and Effectiveness in Topoi (Oxford, 1986); Robinson & Rosolini, Categories of Partial Maps (1988). lift_logic is the underlying ι map (wrap in a typed arrow to inhabit the concept); design note: https://github.com/vincentk/dedekind/issues/267#issuecomment-5711242416