dedekind::category::IsMonicArrow Concept Reference

An arrow declared to be a monomorphism (ι: A ↣ B). More...

Concept definition

template<typename E>
concept dedekind::category::IsMonicArrow = 
    IsArrow<E> && (is_monic_arrow_v<E> || IsIsomorphism<E> ||
                   requires { typename E::is_monic_arrow_tag; })

Detailed Description

An arrow declared to be a monomorphism (ι: A ↣ B).

A monic arrow is injective: if e(x) == e(y) then x == y. The user declares monicity via is_monic_arrow_v<E> = true.

An IsIsomorphism is monic for free: a two-sided inverse makes it injective, so every iso satisfies IsMonicArrow without a separate opt-in. This is the concept-level derivation (an || in the concept body, not an is_monic_arrow_v partial spec): it fires across module boundaries (where a concept-constrained variable-template partial spec does not, cf. the note at algebra:registration) and avoids overlapping the explicit is_monic_arrow_v<Identity<T>> and regular-mono specialisations. Pairs with the blanket iso retract below so that IsIsomorphism ⟹ IsRetractableArrow: a sound iso yields a sound retract by construction (its total inverse wrapped in always-Some), so the mono/retract decidability path is available to isos with no manual, unaudited retract hook.

A third branch reads a structural E::is_monic_arrow_tag typedef, the same tag-discovery idiom IsInitialObject / IsTerminalObject use. It lets a downstream template family opt into monicity (e.g. category::SubobjectInclusion, monic by definition) where an is_monic_arrow_v partial spec would not cross the module boundary — only full specialisations on concrete types do. #881.