Matthew Weaver will present his FPO "Bicubical Directed Type Theory" on October 31, 2024 at 11am in CS 301.
Matthew Weaver will present his FPO "Bicubical Directed Type Theory" on October 31, 2024 at 11am in CS 301.
The members of his committee are as follows:
Andrew Appel (Advisor)
Daniel Licata (Advisor/Wesleyan University)
Zachary Kincaid (Reader)
David Walker (Examiner)
Aarti Gupta (Examiner)Title: Bicubical Directed Type TheoryDirected type theory is an analogue of homotopy type theory where types represent categories, generalizing groupoids. A classical, bisimplicial approach to directed type theory, developed by Riehl and Shulman, is based on equipping each type with both a notion of path and a separate notion of directed morphism. In this setting, a directed analogue of the univalence axiom asserts that there is a universe of covariant discrete fibrations whose directed morphisms correspond to functions—a higher-categorical analogue of the category of sets and functions. While this approach suffices for formalizing mathematics, for applications to computer science we would like a computational interpretation of directed type theory. In this thesis we give a constructive model of a directed type theory with directed univalence in bicubical sets. We formalize much of this in Agda following the approach of Orton and Pitts. First, building on the cubical techniques used to give computational models of homotopy type theory, we show that there is a universe of covariant discrete fibrations with a partial directed univalence principle asserting that functions are a retract of morphisms in this universe. To complete this retraction into an equivalence, we refine the model using Coquand, Ruch, and Sattler’s work on constructive sheaf models. We introduce the cobar modality and by restricting to fibrant types that are also cobar modal, we are able to complete our construction of directed univalence. We then describe a generalization of the fibrant Riehl-Shulman extension types. We prove this in the setting of an arbitrary presheaf category with respect to a new notion of fibrancy that is given by a generic filling problem. This abstraction is general enough to capture all of the current presheaf models of type theories and their classifications of types specified by filling problems. In addition, this result extends the potential syntax of these type theories to be able to internally express any of these filling problems as fibrant types. We use this to then define a type theory in which the user can internally define classifying universes for any such filling problem. Lastly, we overview our implementation of bicubical directed type theory.
