  It is well known that univalence is incompatible with uniqueness of identity
proofs (UIP), the axiom that all types are h-sets. This is due to finite h-sets
having non-trivial automorphisms as soon as they are not h-propositions.
  A natural question is then whether univalence restricted to h-propositions is
compatible with UIP. We answer this affirmatively by constructing a model where
types are elements of a closed universe defined as a higher inductive type in
homotopy type theory. This universe has a path constructor for simultaneous
"partial" univalent completion, i.e., restricted to h-propositions.
  More generally, we show that univalence restricted to $(n-1)$-types is
consistent with the assumption that all types are $n$-truncated. Moreover we
parametrize our construction by a suitably well-behaved container, to abstract
from a concrete choice of type formers for the universe.
