Category Archives: Uncategorized

HoTT 2019 Last Call

Last call for submissions INTERNATIONAL CONFERENCE AND SUMMER SCHOOL ON HOMOTOPY TYPE THEORY 12-17 August 2019 Carnegie Mellon University, Pittsburgh USA https://hott.github.io/HoTT-2019 Submission of talks and registration are open for the International Homotopy Type Theory conference (HoTT 2019), to be … Continue reading

Posted in Meeting, Uncategorized | 1 Comment

Introduction to Univalent Foundations of Mathematics with Agda

I am going to teach HoTT/UF with Agda at the Midlands Graduate School in April, and I produced lecture notes that I thought may be of wider use and so I am advertising them here. The source files I used … Continue reading

Posted in Uncategorized | Leave a comment

Cubical Agda

Last year I wrote a post about cubicaltt on this blog. Since then there have been a lot of exciting developments in the world of cubes. In particular there are now two cubical proof assistants that are currently being developed … Continue reading

Posted in Uncategorized | 29 Comments

Differential Geometry in Modal HoTT

As some of you might remember, back in 2015 at the meeting of the german mathematical society in Hamburg, Urs Schreiber presented three problems or “exercises” as he called it back then. There is a page about that on the … Continue reading

Posted in Uncategorized | 8 Comments

A self-contained, brief and complete formulation of Voevodsky’s univalence axiom

I have often seen competent mathematicians and logicians, outside our circle, making technically erroneous comments about the univalence axiom, in conversations, in talks, and even in public material, in journals or the web. For some time I was a bit … Continue reading

Posted in Uncategorized | Leave a comment

Impredicative Encodings of Inductive Types in HoTT

I recently completed my master’s thesis under the supervision of Steve Awodey and Jonas Frey. A copy can be found here. Known impredicative encodings of various inductive types in System F, such as the type of natural numbers do not … Continue reading

Posted in Applications, Foundations, Uncategorized | 5 Comments

In memoriam: Vladimir Voevodsky

https://www.ias.edu/news/2017/vladimir-voevodsky

Posted in Uncategorized | Leave a comment