I report on progress on an ongoing project - joint work with P. Lumsdaine and V. Voevodsky - that was first presented at the HoTT/UF workshop in Warsaw in 2015. (However, the talk is self-contained.)

One goal of the project is to relate various categorical structures that have been used in the study of semantics of type theory. Our project takes place in univalent type theory, where those structures can be compared in a meaningful way on the level of types and functions between them. More specifically, we consider categories with families, (split) type categories and categories with display maps: we construct maps between the types of these structures, and exhibit properties of the constructed maps.

One particularity of category theory in univalent type theory is the distinction between (pre-)categories and univalent categories. The "Rezk completion" associates to any category a univalent one, satisfying a universal property. In the second part of our project we study how the various structures carry over from a category to its Rezk completion.