dedekind::category::IsNaturalTransformation Concept Reference

A family of components, one per object, whose square commutes at every arrow of the source: \(\alpha_Y \circ F(f) = G(f) \circ \alpha_X\) for each \(f : X \to Y\), read at an arbitrary arrow of the source category's one arrow type, not only at its identities, where every family passes. More...

Concept definition

template<typename Α, typename F, typename G>
concept dedekind::category::IsNaturalTransformation = 
    IsTwoMorphism<Α, F, G> &&
    requires(Α α, F f_map, G g_map, typename F::Σ_cat::Arrow f,
             typename F::Σ_cat::Arrow::Domain c) {
      requires detail_natural::IsNaturalSquare<
          Α, F, G, decltype(f_map(f)), decltype(g_map(f)), decltype(α(c))>;
    }

Detailed Description

A family of components, one per object, whose square commutes at every arrow of the source: \(\alpha_Y \circ F(f) = G(f) \circ \alpha_X\) for each \(f : X \to Y\), read at an arbitrary arrow of the source category's one arrow type, not only at its identities, where every family passes.

@theorem Naturality (F ⟹ G)