Department of

October 2017 November 2017 December 2017 Su Mo Tu We Th Fr Sa Su Mo Tu We Th Fr Sa Su Mo Tu We Th Fr Sa 1 2 3 4 5 6 7 1 2 3 4 1 2 8 9 10 11 12 13 14 5 6 7 8 9 10 11 3 4 5 6 7 8 9 15 16 17 18 19 20 21 12 13 14 15 16 17 18 10 11 12 13 14 15 16 22 23 24 25 26 27 28 19 20 21 22 23 24 25 17 18 19 20 21 22 23 29 30 31 26 27 28 29 30 24 25 26 27 28 29 30 31

Thursday, November 9, 2017

**Abstract:** If homotopy type theory describes a "synthetic theory of ∞-groupoids" is there a similar "synthetic theory of ∞-categories"? In joint work with Mike Shulman, we propose foundations for such a theory motivated by the model of homotopy type theory in the category of Reedy fibrant simplicial spaces, which contains as a full subcategory the ∞-cosmos of Rezk spaces; this model of ∞-categories, first introduced by Rezk, satisfies the requirements of a framework for synthetic ∞-category theory in the sense of joint work with Verity. We introduce simplices and cofibrations into homotopy type theory to probe the internal categorical structure of types, and define Segal types, in which binary composites exist uniquely up to homotopy, and Rezk types, in which the categorical isomorphisms are additionally equivalent to the type-theoretic identities — a "local univalence" condition. In the model these correspond exactly to the Segal and Rezk spaces. We then demonstrate that these simple definitions suffice to develop the synthetic theory of ∞-categories, including functors, natural transformations, co- and contravariant type families with discrete fibers (∞-groupoids), a "dependent" Yoneda lemma that looks like "directed identity-elimination," and the theory of coherent adjunctions.