  This paper continues the series of papers that develop a new approach to
syntax and semantics of dependent type theories. Here we study the
interpretation of the rules of the identity types in the intensional Martin-Lof
type theories on the C-systems that arise from universe categories. In the
first part of the paper we develop constructions that produce interpretations
of these rules from certain structures on universe categories while in the
second we study the functoriality of these constructions with respect to
functors of universe categories. The results of the first part of the paper
play a crucial role in the construction of the univalent model of type theory
in simplicial sets.
