The infinity groupoid models of type theory have already revolutionized our understanding of equality in type theory. So far, the 21st century has been an incre

The infinity groupoid models of type theory have already revolutionized our understanding of equality in type theory. So far, the 21st century has been an incredible time for logicians. There are also older, and very different topological models for typed lambda calculi (see e.g. http://www.cs.bham.ac.uk/~mhe/papers/entcs87.pdf http://www.cs.bham.ac.uk/~mhe/papers/entcs87.pdf). These motivate things like Escardo's "seemingly impossible functional programs" (http://math.andrej.com/2007/09/28/seemingly-impossible-functional-programs/ http://math.andrej.com/2007/09/28/seemingly-impossible-funct...) and, along different lines, Abstract Stone Duality (http://www.paultaylor.eu/ASD/ http://www.paultaylor.eu/ASD/).