A singleton morphism-carrier F (its default value is the arrow) whose dagger is a left inverse: the named non-linear intermediate (Heunen & Vicary). For a value-level carrier, use the is_isometry predicate instead. More...

Concept definition

template<typename F, typename Dagger, typename Op>
concept dedekind::category::IsIsometry =  IsDagger<Dagger, F, Op> && std::default_initializable<F> &&
                     requires { requires is_isometry<Dagger, Op>(F{}); }

Detailed Description

A singleton morphism-carrier F (its default value is the arrow) whose dagger is a left inverse: the named non-linear intermediate (Heunen & Vicary). For a value-level carrier, use the is_isometry predicate instead.