  Category theory in homotopy type theory is intricate as categorical laws can
only be stated "up to homotopy", and thus require coherences. The established
notion of a univalent category (Ahrens, Kapulkin, Shulman) solves this by
considering only truncated types, roughly corresponding to an ordinary
category. This fails to capture many naturally occurring structures, stemming
from the fact that the naturally occurring structures in homotopy type theory
are not ordinary, but rather higher categories.
  Out of the large variety of approaches to higher category theory that
mathematicians have proposed, we believe that, for type theory, the simplicial
strategy is best suited. Work by Lurie and Harpaz motivates the following
definition. Given the first (n+3) levels of a semisimplicial type S, we can
equip S with three properties: first, contractibility of the types of certain
horn fillers; second, a completeness property; and third, a truncation
condition. We call this a complete semi-Segal n-type. This is very similar to
an earlier suggestion by Schreiber.
  The definition of a univalent (1-) category can easily be extended or
restricted to the definition of a univalent n-category (more precisely,
(n,1)-category) for n in {0,1,2}, and we show that the type of complete
semi-Segal n-types is equivalent to the type of univalent $n$-categories in
these cases. Thus, we believe that the notion of a complete semi-Segal n-type
can be taken as the definition of a univalent n-category.
  We provide a formalisation in the proof assistant Agda using a completely
explicit representation of semi-simplicial types for levels up to 4.
