natural.cppm File Reference

Natural Transformations (The Slide between Functors). More...

#include <concepts>
#include <functional>
#include <optional>
#include <tuple>
#include <utility>
import dedekind.category:small;

Include dependency graph for natural.cppm:

Classes
struct	dedekind::category::maybe_monad_tag
struct	dedekind::category::identity_monad_tag
struct	dedekind::category::tuple_monad_tag
struct	dedekind::category::identity_transformation< F >
	The Identity Natural Transformation for Functor F. More...
struct	dedekind::category::vertical_composition< Α, Β, F, G, H >
	Vertical composition of two 2-morphisms (β . α). More...
struct	dedekind::category::horizontal_composition< Α, Β, F, F_prime, G, G_prime >
	Horizontal composition (Godement product). More...

Namespaces
namespace	dedekind::category

Concepts
concept	dedekind::category::IsDefaultMonadTag
concept	dedekind::category::IsPreTransformation
	The raw family of components.
concept	dedekind::category::IsTwoMorphism
	The bridge between two specific Functors.
concept	dedekind::category::detail_natural::IsConstantFamily
	A family with one component at every object: component(), the arrow its call returns wherever it is called. Commuting with each lifted arrow makes such a family natural; a family whose component depends on the object needs the square at both ends, which no certificate here states.
concept	dedekind::category::detail_natural::IsNaturalSquare
	The naturality square at an arrow f, \(\alpha \circ F(f) = G(f) \circ \alpha\), for a component Ac of one type at every object (the single-species categories), decided by the arrow algebra and never by comparing the two composites' types, which differ for any component but an identity although the arrows they denote agree:
concept	dedekind::category::IsNaturalTransformation
	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.
concept	IsNaturalTransformation
	α : F ⟹ G

Typedefs
template<typename C>
using	dedekind::category::disc_self_endofunctor_t = identity_functor<C>
	Discrete-restriction representative of the textbook Disc / U functor: the identity endofunctor on a discrete category C.
template<typename C>
using	dedekind::category::disc_self_unit_t = identity_transformation<disc_self_endofunctor_t<C>>
	Discrete-restriction representative of the textbook unit η / counit ε of the Disc ⊣ U adjunction: the identity natural transformation on disc_self_endofunctor_t<C>.

Functions
template<typename A>
constexpr Maybe< std::decay_t< A > >	dedekind::category::η (A value)
	The Maybe endofunctor T, implemented via std::optional.
template<typename A> requires std::semiregular<std::decay_t<A>>
constexpr Maybe< std::decay_t< A > >	dedekind::category::η (maybe_monad_tag, A value)
template<typename A> requires std::semiregular<A>
constexpr Maybe< A >	dedekind::category::μ (Maybe< Maybe< A > > const &mma)
	μ for Maybe: flattens nested optional context.
template<typename A> requires std::semiregular<A>
constexpr Maybe< A >	dedekind::category::μ (maybe_monad_tag, Maybe< Maybe< A > > const &mma)
template<typename A> requires IsSpecies<std::decay_t<A>>
constexpr std::tuple< std::decay_t< A > >	dedekind::category::η (tuple_monad_tag, A value)
	The std::tuple<T> Frobenius monad.
template<typename A> requires IsSpecies<A>
constexpr std::tuple< A >	dedekind::category::μ (std::tuple< std::tuple< A > > const &tta)
template<typename A> requires IsSpecies<A>
constexpr std::tuple< A >	dedekind::category::μ (tuple_monad_tag, std::tuple< std::tuple< A > > const &tta)
template<typename A>
constexpr A	dedekind::category::ε (std::tuple< A > const &ta)
template<typename A> requires IsSpecies<A>
constexpr A	dedekind::category::ε (tuple_monad_tag, std::tuple< A > const &ta)
template<typename A> requires IsSpecies<A>
constexpr std::tuple< std::tuple< A > >	dedekind::category::δ (std::tuple< A > const &ta)
template<typename A> requires IsSpecies<A>
constexpr std::tuple< std::tuple< A > >	dedekind::category::δ (tuple_monad_tag, std::tuple< A > const &ta)
template<typename A>
constexpr Identity< std::decay_t< A > >	dedekind::category::η (A value)
	The Identity Functor Id_C. Reified 1-morphism that preserves both objects and arrows exactly.
template<typename A> requires IsSpecies<std::decay_t<A>>
constexpr Identity< std::decay_t< A > >	dedekind::category::η (identity_monad_tag, A value)
template<typename A> requires IsSpecies<A>
constexpr Identity< A >	dedekind::category::μ (Identity< Identity< A > > const &iia)
	Monadic join (μ): Identity<Identity<A>> → Identity. Unwraps a doubly wrapped identity arrow.
template<typename A> requires IsSpecies<A>
constexpr Identity< A >	dedekind::category::μ (identity_monad_tag, Identity< Identity< A > > const &iia)
template<typename A>
constexpr Identity< A >	dedekind::category::ε (Identity< A > const &ia)
template<typename A> requires IsSpecies<A>
constexpr Identity< A >	dedekind::category::ε (identity_monad_tag, Identity< A > const &ia)
template<typename A>
constexpr Identity< Identity< A > >	dedekind::category::δ (Identity< A > const &ia)
	Comonadic duplicate (δ): Identity → Identity<Identity<A>>. Wraps an identity arrow once more.
template<typename A> requires IsSpecies<A>
constexpr Identity< Identity< A > >	dedekind::category::δ (identity_monad_tag, Identity< A > const &ia)

Variables
constexpr maybe_monad_tag	dedekind::category::maybe_monad {}
constexpr identity_monad_tag	dedekind::category::identity_monad {}
constexpr tuple_monad_tag	dedekind::category::tuple_monad {}

Detailed Description

Natural Transformations (The Slide between Functors).

@partition :natural

Copyright

2026 The Dedekind Authors Licensed under the Apache License, Version 2.0.

Note

"Il concetto di trasformazione naturale è il vero motivo per cui sono state inventate le categorie." [Trans: "The concept of natural transformation is the real reason why categories were invented."] — Saunders Mac Lane (paraphrased in the spirit of Paolo Aluffi, Algebra: Chapter 0, AMS 2009).

For every object X, we define a morphism η_X: F⟨X⟩ → G⟨X⟩. To be "Natural," the following square must commute for any f: X → Y:

   η_X

F⟨X⟩ ────→ G⟨X⟩ │ │ F(f)│ │G(f) ↓ ↓ F⟨Y⟩ ────→ G⟨Y⟩ η_Y

Formally: G(f) ∘ η_X = η_Y ∘ F(f)