Monthly Archives: April 2014

HoTT awarded a MURI

We are pleased to announce that a research team based at Carnegie Mellon University has received a $7.5 million, five-year grant from the US Air Force Office of Scientific Research, as part of the highly competitive, DoD Multidisciplinary University Research Initiative … Continue reading

Posted in News | 2 Comments

Higher Lenses

Lenses are a very powerful and practically useful functional construct. They represent “first class” fields for a data structure. Lenses arose in work on bidirectional programming (for example, in Boomerang), and in Haskell, people have given many different definitions of … Continue reading

Posted in Applications | 17 Comments

Eilenberg-MacLane Spaces in HoTT

For those of you who have been waiting with bated breath to find out what happened to your favorite characters after the end of Chapter 8 of the HoTT book, there is now a new installment: Eilenberg-MacLane Spaces in Homotopy Type Theory Dan … Continue reading

Posted in Applications, Code, Higher Inductive Types, Paper, Univalence | 6 Comments