Category theory's compositional grammar GCat is the least fixed point of the meta-rule M that sends any essentially algebraic theory to the theory of structure-preserving maps between its models. The same fixed-point architecture — iterate the internal hom from the initial object, take the ω-colimit, invoke Lambek — produces a reflexive object D ≅ D, D in any monoidal closed locally finitely presentable category. This reflexive object is a model of the untyped lambda calculus: universal computation from the Lambek isomorphism alone, no external enumeration required. The monograph builds this result across seven papers: a constructive derivation of category theory from primitives (Elements), the identification of GCat as least fixed point (Grammar), five converging lines of evidence for the fixed-point condition (Computation), the substrate-independent specification identity via D = 1 (Adjunction), the convergence of mathematical and epistemological derivations (Method), and the demonstration that computation is constructively posterior to dimensionality (Dimensionality). A Lean 4 companion (42 files, 0 sorry, 0 custom axioms) verifies the core chain from Adámek's theorem through the lambda calculus model.
Building similarity graph...
Analyzing shared references across papers
Loading...
Larsen James Close
Building similarity graph...
Analyzing shared references across papers
Loading...
Larsen James Close (Sat,) studied this question.
www.synapsesocial.com/papers/69ada885bc08abd80d5bb7dc — DOI: https://doi.org/10.5281/zenodo.18899777