Steve Awodey, Robert Harper: Homotopy type theory: unified foundations of mathematics and computation. ACM SIGLOG News 2(1): 37-44 (2015)