functor.cppm File Reference

The Functorial Spine (Structure Preservation). More...

#include <algorithm>
#include <concepts>
#include <cstddef>
#include <functional>
#include <optional>
#include <ranges>
#include <string>
#include <tuple>
#include <type_traits>
#include <utility>
import dedekind.category:small;

Include dependency graph for functor.cppm:

Classes
struct	dedekind::category::is_functorial< F >
	Trait: F preserves identities and composition, \(F(\mathrm{id}) = \mathrm{id}\) and \(F(f \gg g) = F(f) \gg F(g)\): the functor laws, a certificate as is_involutive and commutes are, primary std::false_type. A type cannot show them, since \(F(f \gg g)\) and \(F(f) \gg F(g)\) are different types that denote one arrow; a functor that lifts each arrow letterwise, elementwise or not at all declares it, and a composite of functors derives it. More...
struct	dedekind::category::MaybeMap< T, F >
	f on the value an optional holds, none where it holds none: the optional functor's action on an arrow. Its codomain is stated, so an arrow into optionals lifts to one into optionals of optionals, as a Kleisli extension needs, and is never collapsed by deduction. More...
struct	dedekind::category::TupleMap< T, F >
	f on the one element of a one-tuple: the one-tuple functor's action on an arrow. More...
struct	dedekind::category::maybe_functor< T >
	The Intensional Functor for Optional (Maybe) values. More...
struct	dedekind::category::tuple_functor< T >
	The Intensional Functor for 1-tuple values. More...
struct	dedekind::category::is_functorial< maybe_functor< T > >
	The container functors map their one slot or none elementwise: the functor laws hold by construction. More...
struct	dedekind::category::is_functorial< tuple_functor< T > >
struct	dedekind::category::composite_functor< F, G >
	Composite Functor G . F (Maps CatS -> CatT -> CatU). More...
struct	dedekind::category::is_functorial< composite_functor< F, G > >
	A composite of functors is a functor: its laws derived from its legs'. More...
struct	dedekind::category::has_one_value< composite_functor< F, G > >
	A composite of two functors with one value each has one value: its legs leave nothing to choose, although its two members keep it from being an empty type. More...
struct	dedekind::category::f_algebra< Carrier, Functor, Structure >
	A concrete witness for an F-algebra. More...
struct	dedekind::category::f_coalgebra< Carrier, Functor, Structure >
	A concrete witness for an F-coalgebra. More...
struct	dedekind::category::identity_functor< Cat >
struct	dedekind::category::is_functorial< identity_functor< Cat > >
	The identity functor returns each arrow itself: the functor laws hold by construction. More...
struct	dedekind::category::Element< T, Op >
	A monoid as a category with one object, its delooping, and an action of it as a functor out of that category (Mac Lane, CWM §I.2): the action's laws are the functor's. More...
struct	dedekind::category::Delooping< T, Op >
	The delooping \(\mathbf{B}(T, \cdot)\): one object, an arrow per element, composition the operation, the identity its unit. Of the opposite operation, Opposite<Op>, it is the opposite category. More...
struct	dedekind::category::Acting< H, V, S >
	An element acting: the arrow \(v \mapsto h(v, s)\) on the set the monoid acts on. More...
struct	dedekind::category::ActingOn< H, V, S >
	The arrows by which a monoid acts on V, as a category: the image of the delooping under the action. More...
struct	dedekind::category::ActionFunctor< H, V, S >
	A right action as a functor out of the delooping of the monoid it acts by: the one object to V, an element s to \(v \mapsto h(v, s)\). Its functor laws are the action's, \(h(v, 1) = v\) and \(h(h(v, a), b) = h(v, a \cdot b)\), which acting_monoid declares, so they are derived and not declared again. A left action registers the opposite operation, so it is a functor out of the opposite category. More...
struct	dedekind::category::is_functorial< ActionFunctor< H, V, S > >
	An action's functor laws come with the action: derived from acting_monoid, which IsRightAction reads. More...
struct	dedekind::category::LeftActing< Act, M, S >
	A scalar acting on the left: the arrow \(m \mapsto s \cdot m\) of a semimodule. More...
struct	dedekind::category::LeftActingOn< M, S, AddM, AddS, MultS, Act >
	The arrows by which the scalars act on a semimodule, as a category: certified by the semimodule's laws, so its identity is the scalars' unit. More...
struct	dedekind::category::LeftActionFunctor< M, S, AddM, AddS, MultS, Act >
	A semimodule's left action as a functor out of the opposite of the delooping of its scalars' product: \((s t) m = s (t m)\), so s then t along the walk acts as \(t s\), the opposite product, and \(1 m = m\) keeps the identity. Those laws are the semimodule's, which is_linear_action declares, so the functor laws are derived. A left action of a monoid is a right action of its opposite: the right actions are ActionFunctor. More...
struct	dedekind::category::is_functorial< LeftActionFunctor< M, S, AddM, AddS, MultS, Act > >
	A semimodule's functor laws come with it: derived from IsSemimodule. More...
struct	dedekind::category::DaggerFunctor< Dagger, T, Op >
	A dagger as a functor: from the delooping of (T, Op) to that of its opposite, each element to its dagger. The functor laws are the dagger's, \((a b)^\dagger = b^\dagger a^\dagger\), the composition law into the opposite category, and \(1^\dagger = 1\), which an involutive anti-homomorphism keeps; so they are derived from IsDagger and not declared again. Contravariant on the one object, and its own inverse. More...
struct	dedekind::category::is_functorial< DaggerFunctor< Dagger, T, Op > >
	A dagger's functor laws come with the dagger: derived from IsDagger, its involution and its reversal of products. More...

Namespaces
namespace	dedekind::category

Concepts
concept	dedekind::category::IsFunctor
	The textbook functor (#633): an IsArrow whose Domain and Codomain are (small) categories — a 1-morphism in Cat, Mac Lane §I.3 — carrying a morphism map.
concept	dedekind::category::IsShapedFunctor
	A 1-morphism mapping CatS -> CatT, refined with the container shape: an IsFunctor that additionally exposes a type-level object map Shape and the action on arrows, F(f).
concept	dedekind::category::IsIdentityFunctor
concept	dedekind::category::IsEndofunctor
	A structure-preserving mapping from a Category back to itself (F : 𝒞 → 𝒞).
concept	dedekind::category::IsIterativeEndomorphism
	A stabilizing step function on a carrier species.
concept	dedekind::category::IsFAlgebra
	A carrier A equipped with a structure map F<A> -> A.
concept	dedekind::category::IsFCoalgebra
	A carrier A equipped with a structure map A -> F<A>.
concept	dedekind::category::IsEmbeddingFunctor
	A functor that is fully faithful + injective on objects (Mac Lane CWM §IV.4 strong reading; the Yoneda-embedding flavour).
concept	dedekind::category::IsQuotientFunctor
	A functor that is a regular epi / coequalizer presentation (Borceux Handbook §4.3).

Typedefs
template<typename T>
using	dedekind::category::Maybe = std::optional<T>
	The Maybe endofunctor T, implemented via std::optional.
using	dedekind::category::detail_functor_actions::Plus = std::plus<std::size_t>
using	dedekind::category::detail_functor_actions::Adding = ActionFunctor<Plus, std::size_t, std::size_t>
using	dedekind::category::detail_functor_actions::Sum = Element<std::size_t, Plus>
using	dedekind::category::detail_functor_actions::Scaling = LeftActionFunctor<std::size_t, std::size_t>
using	dedekind::category::detail_functor_actions::Scalar = Element<std::size_t, Opposite<std::multiplies<std::size_t>>>
using	dedekind::category::detail_functor_actions::Scalars = Delooping<std::size_t, Opposite<std::multiplies<std::size_t>>>

Functions
template<typename 𝗙, typename 𝗚> requires IsArrow<std::decay_t<𝗙>> && IsArrow<std::decay_t<𝗚>> && std::same_as<typename std::decay_t<𝗙>::Codomain, typename std::decay_t<𝗚>::Domain> && IsShapedFunctor<𝗙> && IsShapedFunctor<𝗚> && std::same_as<typename std::remove_cvref_t<𝗙>::Τ_cat, typename std::remove_cvref_t<𝗚>::Σ_cat>
constexpr auto	dedekind::category::operator>> (𝗙 f, 𝗚 g)
template<typename 𝗙, typename 𝗚> requires IsArrow<std::decay_t<𝗙>> && IsArrow<std::decay_t<𝗚>> && std::same_as<typename std::decay_t<𝗙>::Codomain, typename std::decay_t<𝗚>::Domain> && IsShapedFunctor<𝗙> && IsShapedFunctor<𝗚> && std::same_as<typename std::remove_cvref_t<𝗙>::Τ_cat, typename std::remove_cvref_t<𝗚>::Σ_cat> && IsIdentityFunctor<𝗙>
constexpr auto	dedekind::category::operator>> (𝗙, 𝗚 g)
template<typename 𝗙, typename 𝗚> requires IsArrow<std::decay_t<𝗙>> && IsArrow<std::decay_t<𝗚>> && std::same_as<typename std::decay_t<𝗙>::Codomain, typename std::decay_t<𝗚>::Domain> && IsShapedFunctor<𝗙> && IsShapedFunctor<𝗚> && std::same_as<typename std::remove_cvref_t<𝗙>::Τ_cat, typename std::remove_cvref_t<𝗚>::Σ_cat> && IsIdentityFunctor<𝗚>
constexpr auto	dedekind::category::operator>> (𝗙 f, 𝗚)
template<typename 𝗙, typename 𝗚> requires IsArrow<std::decay_t<𝗙>> && IsArrow<std::decay_t<𝗚>> && std::same_as<typename std::decay_t<𝗙>::Codomain, typename std::decay_t<𝗚>::Domain> && IsShapedFunctor<𝗙> && IsShapedFunctor<𝗚> && std::same_as<typename std::remove_cvref_t<𝗙>::Τ_cat, typename std::remove_cvref_t<𝗚>::Σ_cat> && IsIdentityFunctor<𝗙> && IsIdentityFunctor<𝗚>
constexpr auto	dedekind::category::operator>> (𝗙 f, 𝗚)
template<typename 𝗙, typename 𝗚> requires IsShapedFunctor<𝗙> && IsShapedFunctor<𝗚> && std::same_as<typename std::remove_cvref_t<𝗚>::Τ_cat, typename std::remove_cvref_t<𝗙>::Σ_cat>
constexpr auto	dedekind::category::operator<< (𝗙 f, 𝗚 g)
	The "Upstream Fish" (Optional Composition Sugar) g << f => g ∘ f.
template<typename Functor, typename Structure> requires IsEndofunctor<std::remove_cvref_t<Functor>> && IsArrow<std::remove_cvref_t<Structure>>
constexpr auto	dedekind::category::make_f_algebra (Functor functor, Structure structure)
	Factory for F-algebra witnesses.
template<typename Functor, typename Structure> requires IsEndofunctor<std::remove_cvref_t<Functor>> && IsArrow<std::remove_cvref_t<Structure>>
constexpr auto	dedekind::category::make_f_coalgebra (Functor functor, Structure structure)
	Factory for F-coalgebra witnesses.
template<typename T, typename Step, typename Equal = std::equal_to<>> requires IsIterativeEndomorphism<T, Step> && std::predicate<const Equal&, const T&, const T&>
constexpr T	dedekind::category::fixed_point (T seed, Step step, Equal equal={}, std::size_t max_iterations=1024)
	Iteratively compute a fixed point of an endomorphism.
template<typename T, typename Step, typename Equal = std::equal_to<>> requires IsIterativeEndomorphism<T, Step> && std::predicate<const Equal&, const T&, const T&>
constexpr T	dedekind::category::least_fixpoint (T seed, Step step, Equal equal={}, std::size_t max_iterations=1024)
	Alias emphasizing order-theoretic reading of the fixed point.
template<typename T, typename Expand, typename Join, typename Equal = std::equal_to<>> requires std::predicate<const Equal&, const T&, const T&>
constexpr T	dedekind::category::closure (const T &x, Expand expand, Join join, Equal equal={}, std::size_t max_iterations=1024)
	The closure of x under expand: the textbook "closure of @c X under @c Y". It is the least fixpoint of S ↦ x ⊔ expand(S) — the smallest element ⊒ x closed under the one-step expansion expand — equivalently the Kleene join ⨆ₙ expandⁿ(x).

Variables
template<typename F>
constexpr bool	dedekind::category::is_functorial_v
template<typename F>
constexpr bool	dedekind::category::is_identity_functor_v = false
	The unit laws of Cat, decided at the type: an identity functor composes to the other leg itself, \(\mathrm{id} \gg F = F = F \gg \mathrm{id}\), not to a composite around it, as an identity arrow does (:morphism). The overloads repeat the generic one's constraints and add one, so resolution orders them by subsumption (Jlt paper, Listing 1).
template<typename Cat>
constexpr bool	dedekind::category::is_identity_functor_v< identity_functor< Cat > > = true
template<typename F>
constexpr bool	dedekind::category::is_embedding_functor_v = false
	Trait registry for the IsEmbeddingFunctor concept.
template<typename F>
constexpr bool	dedekind::category::is_quotient_functor_v = false
	Trait registry for the IsQuotientFunctor concept.

Detailed Description

The Functorial Spine (Structure Preservation).

@partition :functor

Copyright

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

@quote "एकं सद् विप्रा बहुधा वदन्ति" (Truth is One, though the sages speak of it as many.) — ऋग्वेद (Rig Veda)

functor__The_Functorial_Mapping

A Functor is a bridge between categories that preserves the "Grammar" of the source. In our skeletal framework, a Functor F: T -> U ensures that:

1. Objects are mapped: Every species T has a corresponding F<T>.
2. Morphisms are lifted: Every arrow f: T -> U has a corresponding F(f).
3. Identities are preserved: F(id_T) = id_{F<T>}.
4. Composition is preserved: F(f >> g) = F(f) >> F(g).

Represents a Functor as a morphism between categories (Σ_cat -> Τ_cat). In this library's hierarchy, a Functor is an "arrow between species" that maps morphisms from the source category to the target category while strictly preserving identity and composition laws.

functor__The_Honest_Spine

(Extensional Matter)

With a view to interoperability with primitive types and the std::library, Dedekind distinguishes between the mathematical rule of transformation and the data instances that undergo it. This separation ensures that categorical laws are verified at the structural level before they are applied to values.

1. The Functor (Intensional Functor / Law): Represented by IsShapedFunctor, this is a stateless blueprint acting as a 1-morphism between categories. It owns the action on arrows, F(f), the mathematical recipe for lifting arrows. It requires handles to its Σ_cat and Τ_cat to verify structural integrity (Identity and Composition preservation). Without these handles, a mapping is a mere function; with them, it becomes a verified Functor.
2. The Value (Extensional Value / Matter): This is the concrete instance—an ordinary arrow (IsArrow) or a data container (e.g., Maybe<T>). While the Functor provides the "How," the Value provides the "What." The value is a resident of a category, but it does not own the mapping logic itself.
3. The Bridge: the functor's action on an arrow, F(f), applied to a value, F(f)(ma). No applicator stands between them (#1116).

functor__IsFunctor_Models

Partition

The following types in this partition model IsShapedFunctor:

• identity_functor: Cat -> Cat.
• maybe_functor: Set<T> -> Set<Maybe<T>>.
• tuple_functor: Set<T> -> Set<std::tuple<T>> (the project's Frobenius monad; #632).
• composite_functor: composition G . F for any composable functors.

Notes:

• maybe_functor is a concrete IsShapedFunctor model in this partition, but under the current category choices it is not an IsEndofunctor witness for IsMonad (see :monad for the textbook constraint).

Note

"If we do not succeed in solving a mathematical problem, the reason frequently consists in our failure to recognize the more general standpoint from which the problem before us appears only as a single link in a chain of related problems." – David Hilbert, Mathematical Problems (1900)