Recently, researchers revealed a higher-dimensional structure hidden in type theory, and through it gained a new understanding of identifications, equivalences, quotients, and various new constructs. Novel type theories also arise with explicit access to the once hidden structure. My thesis affirms that we can extend the success of type theory in machine-checkable proofs to areas such as homotopy theory through these new type theories.
I will explain the results that have been machine-checked in my thesis and follow-up papers, with reflection upon new progress and my own experience.
Favonia (Kuen-Bang Hou) works in type theory and programming language theory. They received their Ph.D. from Carnegie Mellon University under the supervision of Professor Robert Harper. Shortly after graduation, they became a postdoc at Institute for Advanced Study in Princeton and then started a tenure-track position at the University of Minnesota, Twin Cities.