Kristina Sojakova

Higher Inductive Types as Homotopy-Initial Algebras Degree Type: Ph.D. in Computer Science
Advisor(s): Steven Awodey, Frank Pfenning
Graduated: August 2016

Abstract:

Homotopy type theory is a new field of mathematics based on the recently discovered correspondence between Martin-Löf's constructive type theory and abstract homotopy theory. We have a powerful interplay between these disciplines – we can use geometric intuition to formulate new concepts in type theory and, conversely, use type-theoretic machinery to verify and often simplify existing mathematical proofs. Higher inductive types form a crucial part of this new system since they allow us to represent mathematical objects from a variety of domains, such as spheres, tori, pushouts, and quotients, in the type theory.

In this thesis we formulated and investigated a class of higher inductive types we call W-quotients which generalize Martin-Löf's well-founded trees to a higherdimensional setting. We have shown that a propositional variant of W-quotients, whose computational behavior is determined up to a higher path, is characterized by the universal property of being a homotopy-initial algebra. As a corollary we derived that W-quotients in the strict form are homotopy-initial. A number of other higher inductive types (such as spheres, suspensions, and type quotients) arise as special cases of W-quotients, and the characterization of these as homotopyinitial algebras thus follows as a corollary to our main result.

We have investigated further higher inductive types – arbitrary truncations, set quotients, and groupoid quotients – and established analogous characterizations in terms of the universal property of homotopy-initiality. Furthermore, we showed that set and groupoid quotients can be recovered from W-quotients and truncations.

Thesis Committee:
Frank Pfenning (Co-Advisor)
Steve Awodey (Co-Advisor)
Robert Harper
Thierry Coquand (University of Gothenburg)
Nicola Gambino (University of Leeds)

Frank Pfenning, Head, Computer Science Department
Andrew W. Moore, Dean, School of Computer Science

Keywords:
Higher Inductive Type, Homotopy-Initial Algebra, Homotopy Type Theory