The category of bisimplicial sets admits a model of homotopy type theory, due to Shulman, and also a model of (∞, 1)-categories, due to Rezk. The subcategory of (∞, 1)-categories defines an "∞-cosmos" — a simplicial enriched category of fibrant objects studied by Riehl-Verity — within which it is possible to develop the the basic category theory of (∞, 1)-categories "synthetically" i.e., in ignorance of the fact that the objects being discussed are bisimplicial sets. Motivated by these observations, this talk will discuss preliminary work in progress, joint with Michael Shulman, with the aim of developing a synthetic theory of (∞, 1)-categories in HoTT.