A singleton morphism-carrier whose dagger is its inverse (isometry and coisometry) — a dagger-iso, \(f^\dagger = f^{-1}\). Hence an IsIsomorphism once lifted into the arrow surface (follow-up). More...

Concept definition

template<typename F, typename Dagger, typename Op>
concept dedekind::category::IsUnitary =  IsIsometry<F, Dagger, Op> &&
                    requires { requires is_coisometry<Dagger, Op>(F{}); }

Detailed Description

A singleton morphism-carrier whose dagger is its inverse (isometry and coisometry) — a dagger-iso, \(f^\dagger = f^{-1}\). Hence an IsIsomorphism once lifted into the arrow surface (follow-up).