Vladimir Voevodsky - An Intuitive Introduction to Motivic Homotopy Theory

Given at The Clay Mathematics Institute (CMI) 2002 Annual Meeting, this is a talk meant to be intelligible to non-mathematicians. As a non-mathematician, I think he's done a good job. As a mathematician, I can't really say. He did point out something I think is very significant, which is that there is a deep connection between Periodicity in Clifford Algebras and in Homotopy Groups of spheres. See Bott Periodicity Theorem. So it's a kind of linking of Algebraic Geometry and Geometric Algebra. I am also starting to get an idea of what "set theory in higher dimensions" might be about. See Curt Jaimungal Interviews Gabriele Carcassi and Andrej Bauer and Ronald Brown On Monads and Groupoids and Alexander Grothendieck on his idea for a Science Fiction Novel on Motives.

19:35 Formally defining a Category. Considering the category of Topological spaces,"Instead of looking at the structure of an object, we look at his social relationships". See Digital Chalk - Nathan Doing Topology PhD Qualifying Exam Problems (Live).

Subscribe to PoincareDuality. See the Wikipedia page Poincaré duality.

That post I made in a cafe in Mexico should have had a trailer:

Subscribe to Sony Pictures Entertainment.

There is another connection with Logic:

Steve Awodey - Univalent Foundations Seminar (November 19, 2012) appeared on YouTube 17 Aug 2016, two years after I corresponded with Steve Awodey about this!

17:27 When he starts explaining fibers we don't get to see what he's drawing on the board, unfortunately. See also Fundamental groupoid. 21:01 The result is Scott's Topological Interpretation of the Lambda Calculus extended to dependently typed Lambda Calculus with Identity types. 24:55 On expressivity. The terms of order 0 and 1, "points" and "paths", have the structure of a groupoid. See again Curt Jaimungal Interviews Gabriele Carcassi, and  Toby Explaining Category Theory, Bob Ross Style.

This is Voevodsky's lecture on Type Systems of November 21, 2012:

For the rest of this series of three lectures, see Daniel Tubbenhauer on Diagrammatic Algebra and Quantum Topology.

Subscribe to IAS.

This was the day before yesterday:

This was yesterday:

Maybe I'll try again today? I did!

And I thought I'd made a video about this earlier, but I can't find it, so here's another one with more anecdotes: This is about Tim Griffin's correspondence between classical logic and simply-typed lambda calculus with a type of "call-with-current-continuation".

See A Formulae-as-Types Notion of Control by Timothy G. Griffin (POPL 90) From the conclusion:

This paper has shown that a formulae-as-typed correspondence can be defined between classical propositional logic and a typed Idealized Scheme containing a control operator similar to Scheme’s call/cc. It should be noted, however, that the paper merely presents a formal correspondence between classical logic and Idealized Scheme. At this point there still remains the question: Why should there be any correspondence at all? Whether or not there is a “deeper reason” underlying the correspondence is unclear at this time.