Simplicial type theory (STT) was introduced by Riehl and Shulman to leverage homotopy type theory to prove results about (∞,1)-categories. Initial work on simplicial type theory focused on "formal" arguments in higher category theory and, in particular, no non-trivial examples of ∞-category theory were constructible within STT. More recent work has changed this state of affairs by applying techniques developed initially for cubical type theory to construct the ∞-category of spaces. We complete this process by constructing the ∞-category of ∞-categories, recovering one of the main foundational results of ∞-category theory (straightening-unstraightening) purely type-theoretically. We also show how this construction enables new examples of the directed version of the structure identity principle: the structure homomorphism principle.

Riehl and Shulman [1] introduced simplicial type theory (STT), a variant of homotopy type theory which aimed to study not just homotopy theory, but its fusion with category theory: (∞, 1)-category theory. While notoriously technical, manipulating ∞-categories in simplicial type theory is often easier than working with ordinary categories, with the type theory handling infinite stacks of coherences in the background. We capitalize on recent work by Gratzer et al. [2] defining the (∞, 1)-category of ∞-groupoids in STT to define presheaf categories within STT and systematically develop their theory. In particular, we construct the Yoneda embedding, prove the universal property of presheaf categories, refine the theory of adjunctions in STT, introduce the theory of Kan extensions, and prove Quillen’s Theorem A. In addition to a large amount of category theory in STT, we offer substantial evidence that STT can be used to produce difficult results in ∞-category theory at a fraction of the complexity.

We show that restricting the elimination principle of the natural numbers type in Martin-Löf Type Theory (MLTT) to a universe of types not containing ####II-types ensures that all definable functions are primitive recursive. This extends the concept of primitive recursiveness to general types. We discuss extensions to univalent type theories and other notions of computability. We are inspired by earlier work by Martin Hofmann [18], work on Joyal's arithmetic universes [27], and Hugo Herbelin and Ludovic Patey's sketched Calculus of Primitive Recursive Constructions [16].

Working in univalent foundations, we investigate the symmetries of spheres, i.e., the types of the form ####Sn = ####Sn. The case of the circle has a slick answer: the symmetries of the circle form two copies of the circle. For higher-dimensional spheres, the type of symmetries has again two connected components, namely the components of the maps of degree plus or minus one. Each of the two components has Z/2Z as fundamental group. For the latter result, we develop an EHP long exact sequence.

Abstract Working in homotopy type theory, we introduce the notion of n-exactness for a short sequence $F\to E\to B$ of pointed types and show that any fiber sequence $F\hookrightarrow E \twoheadrightarrow B$ of arbitrary types induces a short sequence that is n-exact at $\| E\|_{n-1}$ . We explain how the indexing makes sense when interpreted in terms of n-groups, and we compare our definition to the existing definitions of an exact sequence of n-groups for $n=1,2$ . As the main application, we obtain the long n-exact sequence of homotopy n-groups of a fiber sequence.

We present a development of cellular cohomology in homotopy type theory. Cohomology associates to each space a sequence of abelian groups capturing part of its structure, and has the advantage over homotopy groups in that these abelian groups of many common spaces are easier to compute. Cellular cohomology is a special kind of cohomology designed for cell complexes: these are built in stages by attaching spheres of progressively higher dimension, and cellular cohomology defines the groups out of the combinatorial description of how spheres are attached. Our main result is that for finite cell complexes, a wide class of cohomology theories (including the ones defined through Eilenberg-MacLane spaces) can be calculated via cellular cohomology. This result was formalized in the Agda proof assistant.

We present a development of cellular cohomology in homotopy type theory. Cohomology associates to each space a sequence of abelian groups capturing part of its structure, and has the advantage over homotopy groups in that these abelian groups of many common spaces are easier to compute. Cellular cohomology is a special kind of cohomology designed for cell complexes: these are built in stages by attaching spheres of progressively higher dimension, and cellular cohomology defines the groups out of the combinatorial description of how spheres are attached. Our main result is that for finite cell complexes, a wide class of cohomology theories (including the ones defined through Eilenberg-MacLane spaces) can be calculated via cellular cohomology. This result was formalized in the Agda proof assistant.

We present a development of the theory of higher groups, including infinity groups and connective spectra, in homotopy type theory. An infinity group is simply the loops in a pointed, connected type, where the group structure comes from the structure inherent in the identity types of Martin-Löf type theory. We investigate ordinary groups from this viewpoint, as well as higher dimensional groups and groups that can be delooped more than once. A major result is the stabilization theorem, which states that if an n-type can be delooped n + 2 times, then it is an infinite loop type. Most of the results have been formalized in the Lean proof assistant.

Homotopy type theory is a version of Martin-Löf type theory taking advantage of its homotopical models. In particular, we can use and construct objects of homotopy theory and reason about them using higher inductive types. In this article, we construct the real projective spaces, key players in homotopy theory, as certain higher inductive types in homotopy type theory. The classical definition of ℝPn, as the quotient space identifying antipodal points of the n-sphere, does not translate directly to homotopy type theory. Instead, we define ℝPnby induction on n simultaneously with its tautological bundle of 2-element sets. As the base case, we take ℝP-1to be the empty type. In the inductive step, we take ℝPn+1to be the mapping cone of the projection map of the tautological bundle of ℝPn, and we use its universal property and the univalence axiom to define the tautological bundle on ℝPn+1. By showing that the total space of the tautological bundle of ℝPnis the n-sphere Sn, we retrieve the classical description of ℝPn+1as ℝPnwith an (n + 1)-disk attached to it. The infinite dimensional real projective space ℝP∞, defined as the sequential colimit of ℝPnwith the canonical inclusion maps, is equivalent to the Eilenberg-MacLane space K(ℤ/2ℤ, 1), which here arises as the subtype of the universe consisting of 2-element types. Indeed, the infinite dimensional projective space classifies the 0-sphere bundles, which one can think of as synthetic line bundles. These constructions in homotopy type theory further illustrate the utility of homotopy type theory, including the interplay of type theoretic and homotopy theoretic ideas.