Department of

October 2017 November 2017December 2017Su Mo Tu We Th Fr Sa Su Mo Tu We Th Fr Sa Su Mo Tu We Th FrSa1 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 151622 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.