Anjolina Grisi de Oliveira / Arthur Freitas Ramos / Ruy J.G.B. de Queiroz
Librería Samer Atenea
Kálamo Books
Librería Elías (Asturias)
Librería Kolima (Madrid)
Librería Proteo (Málaga)
When are two proofs of the same proposition equal? This book answers through computational paths - explicit syntactic witnesses that record how one proof-term rewrites into another. Continuing the programme begun in The Functional Interpretation of Logical Deduction (2011), it extends the Curry-Howard correspondence and the tradition of labelled deductive systems into a rewrite calculus of proof equalities. Part I develops a 77-rule rewrite system on paths, proves it confluent and terminating, and derives decidable path equivalence from unique normal forms. Part II uncovers the higher-dimensional structure latent in this calculus: paths assemble into a weak ω-groupoid, with 2-cells as derivations between paths, 3-cells as coherences between derivations, and the Eckmann-Hilton argument recovered directly from rewrite combinatorics. Part III turns outward - to path induction and the J-eliminator, the failure of UIP and the resulting proof-relevance, fundamental groupoids of combinatorial spaces, and the framework’s relationship to Homotopy Type Theory, category theory, and higher algebra. The approach shares conceptual ground with HoTT but diverges in its commitments: where HoTT posits univalence and higher inductive types, computational paths offer explicit rewrite witnesses and effective normalisation, with path equivalence rendered decidable rather than postulated. A companion Lean 4 formalization machine-checks the core constructions and major theorems. Aimed at logicians, type theorists, and mathematicians concerned with the computational content of equality, the volume is self-contained - appendices cover term rewriting and higher groupoids - while charting a research programme that reaches toward dependent types, directed rewriting, and homotopical semantics.
