About Logic - Interview with Steve Awodey

This is really great! Something just clicked for me about equality types (4:39). 

See Univalence as a principle of logic and Kripke-Joyal forcing for type theory and uniform fibrations.

24:05 the quote from Frege is 

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

26:15 How the discrete types are identified in type theory. 

29:07 Thorsten on the question of the discreteness of the equality type and infinity groupoids being a very natural idea from the perspective of geometry.

35:08 On Identity types, Univalence and Equality of Types.

See Another Excellent Talk on HoTT by Steve Awodey and Emily Riehl's "Infinity Categories for Undergraduates" Talk on Curt Jaimungal's Podcast. 

See Egbert Rijke's book Introduction to Homotopy Type Theory. 

The book on the shelf behind Thorsten is Conceptual Programming with Python. When he got back to Nottingham from a year at Princeton IAS doing Homotopy Type Theory, they made him teach Python to undergraduates and this book was the result.

Subscribe to About Logic.