aboutlogic #05 | Steve Awodey – Homotopy Type Theory, Logic & Philosophy

Homotopy Type Theory, Logic & Philosophy
"I am convinced that my Begriffsschrift will find successful application wherever particular value is placed on the rigor of proofs, as in the foundations of the differential and integral calculus. It seems to me that it would be even easier to extend the domain of this formal language to geometry. Only a few more symbols would need to be added for the intuitive relations occurring there. In this way, one would obtain a kind of analysis situs."

Preface to Begriffsschrift, 1879, Gottlob Frege

Further Reading & Resources:
The Natural Number Game: adam.math.hhu.de/#/g/leanprover-community/nng4
The Xena Project: xenaproject.wordpress.com
Graham Priest: grahampriest.net

Thorsten Altenkirch: cs.nott.ac.uk/~psztxa
Deniz Sarikaya: denizsarikaya.de

Production:
Jan-Niklas Meyer: jammos.com

Many thanks to the Akademie der Wissenschaften in Hamburg for supporting the first season of the podcast.