Matthew Weaver will present his Pre FPO "Bicubical Directed Type Theory" on Friday, December 10, 2021 at 2:30pm via zoom. Zoom Link: https://princeton.zoom.us/j/93770491933?pwd=S0g5TW9OR0xEenFOOHBGeHdkK29rdz09 Meeting ID: 937 7049 1933 Passcode: 110745 Committee: Andrew Appel (Advisor) Daniel Licata (Reader) Zachary Kincaid (Reader) David Walker (Examiner) Aarti Gupta (Examiner) Title: Bicubical Directed Type Theory Abstract: In homotopy type theory, each type is equipped with an abstract notion of path, corresponding to the morphisms of a higher groupoid. Voevodsky's univalence axiom states that the type of paths between types is equivalent (a generalization of isomorphism) to the type of equivalences between types, and can be seen as extending type theory with a generic program for lifting equivalences between types along any type family. Defining this lifting for all dependent types is quite subtle, but univalence has recently been given a computational interpretation in various cubical type theories. A natural question is whether there are any directed analogues of homotopy type theory, where types are equipped with a notion of directed morphism and correspond to higher categories, generalizing groupoids. In such a setting, one possible directed analogue of univalence would circumscribe a class of type constructors that represent covariant functors, and provide a means to automatically lift a function or directed morphism along such a type constructor. Directed type theory with directed univalence has some potential applications to computer science that are not possible in ordinary homotopy type theory, such as providing a convenient language for coding the functorial specification of abstract syntax. One 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. While ordinary homotopy type theory has models in simplicial sets (a model of homotopy types) the Riehl-Shulman type theory is based on a model in bisimplicial sets, capturing these two notions of path and directed morphism. While this suffices for formalizing mathematics, for applications to computer science we would like a computational interpretation of the type theory, and it is not yet known whether there are constructive models of standard homotopy type theory in simplicial sets. Thus, in this thesis, we instead consider a cubical setting, and give a constructive model of a directed type theory with directed univalence in bicubical sets. We formalize much of this model using Agda as the internal language of a 1-topos, following 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 (covariant functors valued in types that themselves have trivial morphism structure), 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 some recent work on constructive sheaf models by Coquand, Ruch, and Sattler, which builds on Shulman's characterization of fibrations in injective model structures as algebras for the cobar construction. Concretely, this means equipping each fibrant type with an additional operation (an equivalence with the cobar construction on it), from which the final part of the directed univalence equivalence can be defined. In the presence of directed univalence, one would additionally hope for a theory containing directed higher inductive types (DHITs). These types allow for one to inductively define types containing directed structure, and in conjunction with directed univalence allow for novel proof techniques in verification; in particular, the combination allows one to directly formalize functorial semantics using the internal categorical structure of types. We introduce a schema for DHITs based off of the schema for higher inductive types in cubical type theory by Cavallo and Harper. As a part of this work, we additionally define schemas for regular inductive types and higher inductive types. Lastly, we demonstrate how DHITs can be used with directed univalence to encode functorial semantics for formal verification.