Formalising Foundations in Dependent Type Theories
See Vladimir Voevodsky - What if Current Foundations of Mathematics are Inconsistent . Subscribe to Formalization Seminar Cambridge . Subscribe to ItaLean Conference . The state of the art three years ago: Subscribe to Lean Prover Community . I came here because I heard this talk by Simon Willerton last week and he seems to be able to interpret some ideas like extanaturality from higher category theory into 2-category theory, but I am not sure about that: he doesn't say that's what he's done, it's just how it seems to me. Subscribe to Topos Institute .