  In this paper, we analyze and compare three of the many algebraic structures
that have been used for modeling dependent type theories: categories with
families, split type-categories, and representable maps of presheaves. We study
these in univalent type theory, where the comparisons between them can be given
more elementarily than in set-theoretic foundations. Specifically, we construct
maps between the various types of structures, and show that assuming the
Univalence axiom, some of the comparisons are equivalences.
  We then analyze how these structures transfer along (weak and strong)
equivalences of categories, and, in particular, show how they descend from a
category (not assumed univalent/saturated) to its Rezk completion. To this end,
we introduce relative universes, generalizing the preceding notions, and study
the transfer of such relative universes along suitable structure.
  We work throughout in (intensional) dependent type theory; some results, but
not all, assume the univalence axiom. All the material of this paper has been
formalized in Coq, over the UniMath library.
