Univalent

This talk is intended for a general audience. The recent discovery of an interpretation of constructive type theory into abstract homotopy theory has led to a new approach to foundations with both intrinsic geometric content and a computational...

(Continued from September 26, 2012)