selected publications academic article Types are weak ω -groupoids. Proceedings of The London Mathematical Society. 102:370-394. 2010