Fibrations in Directed Type Theory

TL;DR

This paper develops the theory of cocartesian fibrations within synthetic simplicial type theory, using novel equivalences and formalizes the results in a proof assistant.

Contribution

It introduces a new approach to cocartesian fibrations in synthetic simplicial type theory and formalizes the findings using the rzk proof assistant.

Findings

Defined cocartesian fibrations and proved their closure properties.

Established an equivalence between LARI adjunctions and initial sections.

Formalized the work in the rzk proof assistant.

Abstract

We study $\infty$-categories in the synthetic simplicial type theory developed by Riehl and Shulman. In particular, we define cocartesian fibrations and prove their closure properties using a novel equivalence between LARI adjunctions and initial sections. We formalize our work using the experimental proof assistant rzk and upstream our work to the formalization effort by Riehl et al. In addition to our new work, we also give an introduction to general type theory, homotopy type theory, and the simplicial type theory used by the rest of the thesis.