Matthew Weaver will present his Pre FPO "Bicubical Directed Type Theory" on Friday, December 10, 2021 via zoom.

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.