If homotopy type theory describes a "synthetic theory of ∞-groupoids" is there a similar directed type theory that describes a "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, a framework for synthetic ∞-category theory developed in 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.