category.cppm File Reference

Level 0–4: categorical bedrock + ETCS facade. More...

import dedekind.category:partial;

Include dependency graph for category.cppm:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Namespaces
namespace	dedekind::category

Detailed Description

Level 0–4: categorical bedrock + ETCS facade.

Copyright

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

@quote "La structure d’une chose n’est nullement une chose qu’on puisse « saisir » si l’on n’est pas d’abord prêt à s’y fondre." (The structure of a thing is by no means something that one can "grasp" if one is not first prepared to melt into it.) — Alexander Grothendieck, Récoltes et Semailles.

The table of contents for the dedekind.category module is as follows:

1. ATOMS (:species, :morphism, :mereology, :logic): Reification of machine primitives, the Skeletal Arrow, and the grounding of Truth via Parthood. 0.5 INFRASTRUCTURE (:posetal, :small, :discrete, :nno, :cartesian, :limit, :pullback): The universal category-theoretic constructions, including Lawvere's Natural Numbers Object (ETCS Axiom 9; closes #445).
2. IDEALS (:total, :action): The pure laws of total algebra.
3. BRIDGE (:functor, :natural, :monad, :kleisli): The Functorial Spine enabling the Monadic Kleisli lift.
4. REALITY (:numeric, :partial): Reconciling theory with hardware-level indeterminacy and IEEE 754.
5. SKELETAL SIGNATURES (:etcs): The Set-Theoretic Interface (ETCS).

See also

Lawvere, F.W. (1964) "An Elementary Theory of the Category of Sets"

McLarty, C. (1993) "Numbers can be just what they have to"

Note

"It is less than four years since cohomological methods were introduced into algebraic geometry, and it seems certain that they are to overflow the part of mathematics in the coming years, from the foundations up to the most advanced parts." – Alexander Grothendieck, ICM Edinburgh lecture (1958)

Roadmap (work in progress)

• #275 nLab algebra/category hierarchy: the algebraic and categorical hierarchy against the nLab; still open are the quasigroup, the groupoid, the Lie algebra with Jacobi and antisymmetry checked, the general comonoid, the monoidal category with its coherence data (beyond the cartesian IsTensor), the symmetric monoidal and the enriched category, and the multi-object dagger; the band and the Heyting algebra exist as IsMereologicalMeetBand and IsHeytingLatticeCategory.