Monthly Archives: April 2014

HoTT awarded a MURI

Posted on 29 April 2014 by Steve Awodey

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

Posted on 29 April 2014 by Paolo Capriotti

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

Posted on 15 April 2014 by Dan Licata

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 | 7 Comments