iso.cppm File Reference

The retract / iso-enabling arrow surface: the constructions that turn a factorisation class into a downstream decidability class. More...

#include <concepts>
#include <type_traits>
#include <utility>
import dedekind.category:natural;

Include dependency graph for iso.cppm:

Classes
struct	dedekind::category::IsoRetract< F >
	The retract of an IsIsomorphism: its total inverse arrow wrapped in an always-engaged std::optional. More...

Namespaces
namespace	dedekind::category

Concepts
concept	dedekind::category::IsRetractableArrow
	A monic arrow that ships with a structurally-known retract, a partial inverse retract(f) : Cod<F> → Maybe<Dom<F>>, discoverable via ADL on F.

Functions
template<typename F> requires IsIsomorphism<std::remove_cvref_t<F>> && requires(const std::remove_cvref_t<F>& cf, const Cod<F>& y) { inverse(cf)(y); }
constexpr auto	dedekind::category::retract (F f)
	Blanket retract for any IsIsomorphism: wraps inverse(f) in always-Some (see IsoRetract). This is what makes IsIsomorphism ⟹ IsRetractableArrow hold with no manual hook.

Detailed Description

The retract / iso-enabling arrow surface: the constructions that turn a factorisation class into a downstream decidability class.

@partition :iso

Copyright

2026 The Dedekind Authors Licensed under the Apache License, Version 2.0.

iso__What_Lives_Here

The "advanced" arrow constructions, extracted from :morphism so the arrow base keeps only the lean factorisation primitives (IsArrow / IsMonicArrow / IsEpicArrow / IsIsomorphism stay there), mirroring how the is_involutive machinery was extracted into :involution:

• IsRetractableArrow, a monic arrow carrying a partial inverse: the concept the :image decidability seam dispatches on;
• IsoRetract and the blanket retract, the wiring IsIsomorphism ⟹ IsRetractableArrow, so a sound iso is retractable by construction (its total inverse wrapped in always-Some), with no manual, unaudited hook.

iso__Retract_As_Kleisli

A retract is a Kleisli arrow into the maybe monad, retract(f) : Cod<F> → Maybe<Dom<F>>, spelled honestly with category::Maybe and the unit η (maybe_monad) from :functor / :natural, not raw std::optional. That is why this partition sits downstream of :natural (:morphism → :natural → :iso): it removes the layering inversion in which :morphism (importing only :species) reached for a raw optional that is really Maybe.

iso__Branch_On_Iso

Dispatch branches on iso: the :image ImageChi iso specialisation and the DSL image(iso, Set) overload (#657) take precedence over the retract path (guarded !IsIsomorphism), so an iso uses its own tighter path and only monic-but-not-iso arrows take the retract route. The blanket iso retract additionally gates on the inverse arrow being const-invocable (the #823 discipline), so a mutable-inverse-only iso is not advertised retractable.

Wikipedia: Section (category theory); Kleisli category; Equaliser (mathematics).

Note

"Every standard construction is induced by a pair of adjoint functors." Heinrich Kleisli, Proc. Amer. Math. Soc. 16(3) (1965), pp. 544-546: the title of the note showing every monad (a "standard construction") resolves through the Kleisli category. Fitting, since a retract here is a Kleisli arrow, the structure handed back through the unit η. (Kleisli wrote in English; no translation needed.)

@build_order imports :morphism, :functor, :natural; upstream of :image (which dispatches on IsRetractableArrow).