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.