Computational Paths. The Calculus of Equality

Name: Computational Paths. The Calculus of Equality
Price: 55.08 AUD
Availability: OutOfStock
ISBN: 9781848905153

Arthur Freitas Ramos, Ruy J G B de Queiroz, Anjolina Grisi de Oliveira

$64.95 $55.08

Paperback

Not in-store but you can order this
How long will it take?

Availability Information

We source books from suppliers in Australia and overseas. For books we don't currently have in stock, the time it takes to get them from our suppliers can vary widely - from a few days to a few months - so we check each book with each supplier to determine the expected time it will take to be supplied to us.

We will update you on expected arrival time to us. If this delay is too long, please let us know within 2 business days and we can give you options regarding cancelling or adjusting your order. More details on cancelling your order can be found in our Terms of Trade.

To find out the anticipated arrival time for specific items prior to ordering, please contact us by phone or email:

Phone +61 2 9264 3111, or 1800 4 BOOKS (1800 4 26657) if outside Sydney:
option 1 Abbey's Bookshop (Crime, History, Science, Kids & more) • info@abbeys.com.au
option 2 Language Book Centre (ESL & Foreign Languages) • language@abbeys.com.au
option 3 Galaxy Bookshop (Sci-fi, Fantasy, Romance, Graphic Novels) • sf@galaxybooks.com.au

QTY:

English

College Publications
11 May 2026

Mathematical logic; Algebra; Applied mathematics

Summary
Details

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.

By: Arthur Freitas Ramos, Ruy J G B de Queiroz, Anjolina Grisi de Oliveira
Imprint: College Publications
Dimensions: Height: 234mm, Width: 156mm, Spine: 29mm
Weight: 780g
ISBN: 9781848905153
ISBN 10: 1848905157
Pages: 564
Publication Date: 11 May 2026
Audience: General/trade , ELT Advanced
Format: Paperback
Publisher's Status: Active