dedekind/conceptdedekind_1_1category_1_1IsTwoMorphism.html

template<typename Α, typename F, typename G>

concept dedekind::category::IsTwoMorphism =

    IsShapedFunctor<F> && IsShapedFunctor<G> &&


    std::same_as<typename F::Σ_cat, typename G::Σ_cat> &&

    std::same_as<typename F::Τ_cat, typename G::Τ_cat> &&

    requires(Α α, typename F::Σ_cat::Arrow::Domain c) {


      requires std::same_as<typename decltype(α(c))::Domain,

                            typename decltype(F{}(F::Σ_cat::id_c(c)))::Domain>;

      requires std::same_as<typename decltype(α(c))::Codomain,

                            typename decltype(G{}(G::Σ_cat::id_c(c)))::Domain>;

    }

dedekind::category::IsShapedFunctor
A 1-morphism mapping CatS -> CatT, refined with the container shape: an IsFunctor that additionally e...
Definition functor.cppm:173

dedekind::category::IsTwoMorphism
The bridge between two specific Functors.
Definition natural.cppm:281