IsNaturalTransformation Concept Reference

α : F ⟹ G More...

Concept definition

template<>
concept IsNaturalTransformation = 

Detailed Description

α : F ⟹ G

natural__Naturality_Condition

For every object $X$ in the source category, $\eta$ provides a component arrow $\eta_X: F(X) \to G(X)$ such that for any morphism $f: X \to Y$, the naturality square commutes: $G(f) \circ \eta_X = \eta_Y \circ F(f)$.

A Natural Transformation η: F ⟹ G is a family of morphisms that provides a structural bridge between two functorial contexts. Unlike a Functor which maps species, the Transformation maps the context itself.

Defines Natural Transformations as 2-cells, acting as morphisms between Functors. For any two functors F, G: C -> D, a natural transformation provides a family of morphisms in the target category D that satisfies the naturality square, enabling structural translation between different species-mappings.

In this library's single-species categories, object labels are recovered via the identity arrow id_c(x). As a result, component arrows such as η_x are checked by lifting identity arrows and reading off the resulting domain object, rather than by ranging over a separate textbook object class.

Note

"Logic teaches us that on such and such a road we are sure of not meeting an obstacle; it does not tell us which is the road that leads to the desired end." – Henri Poincare, Science and Method (1908)