Type Theoretic Methods for Higher Structures

Abstract

The present work is concerned with the study of higher structures through the lens of dependent type theory and categorical logic. We distinguish two main themes, but type theory can be seen as the common ground.

The first part presents some aspects of the theory of (∞,1)-categories in the framework of simplicial homotopy type theory of Riehl and Shulman. We present the theory of limits and colimits in this setting and prove some results, such as universal properties and preservation under adjunctions. We also include the computation of the limit of a family of spaces. In this setting, we also study and characterize exponentiable functors, where our main tools are Segal and Rezk completion of types, which we develop throughout. Importantly, we emphasize the consistency of our definitions by providing explicit comparison results with the bisimplicial sets model of simplicial homotopy type theory.

In the second part, given any weak model category, we associate to it the notion of an infinitary first-order logic. The idea, originally due to Simon Henry, is motivated by Makkai's FOLDS. To build the logic, we use the syntactic specification of dependent type theory of Cartmell's generalized algebraic theories. In the language we build, the cofibrant objects of the weak model category play the role of contexts from which the formulas are constructed. The fibrant objects are the models which validate the formulas. Thus, the formulas refer to properties of the fibrant objects of the weak model category. We prove what we call 'invariance theorems' to show that the language we define is homotopically well-behaved: homotopic variables satisfy the same formulas, equivalent models satisfy the same formulas, equivalent contexts produce equivalent sets of formulas, and Quillen equivalent weak model categories have equivalent languages. The language avoids the so-called "evil properties", and can be seen as a homotopic version of the language for categories introduced by Blanc and Freyd.