InitialObjectArrow<Init, Target> — the unique arrow from the initial object into any subobject (Init → Target), i.e. the empty function / the ⊥-of-Sub(U) leg. Dual to inclusion_arrow: where that reifies an inclusion into the ambient, this reifies the initiality mediator out of Ø. Gated on category::IsInitialObject<Init> so only a genuine initial object (Ø, tagged) can be the source; the body forwards the (vacuous) Member value and is unreachable in practice (Ø has no members). Canonical span leg for a pushout A ← Ø → B, replacing hand-rolled per-instance span structs. #881. More...

Public Types
using	Domain = typename Init::Member
using	Codomain = typename Target::Member

Public Member Functions
constexpr Codomain	operator() (const Domain &m) const

Detailed Description

template<typename Init, typename Target>
requires dedekind::category::IsInitialObject<Init> && dedekind::category::IsSubobject<Init, typename Init::Domain> && dedekind::category::IsSubobject<Target, typename Target::Domain>
struct dedekind::sets::InitialObjectArrow< Init, Target >

InitialObjectArrow<Init, Target> — the unique arrow from the initial object into any subobject (Init → Target), i.e. the empty function / the ⊥-of-Sub(U) leg. Dual to inclusion_arrow: where that reifies an inclusion into the ambient, this reifies the initiality mediator out of Ø. Gated on category::IsInitialObject<Init> so only a genuine initial object (Ø, tagged) can be the source; the body forwards the (vacuous) Member value and is unreachable in practice (Ø has no members). Canonical span leg for a pushout A ← Ø → B, replacing hand-rolled per-instance span structs. #881.

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

src/main/modules/dedekind/sets/expressions.cppm

Public Types

Public Member Functions

Detailed Description