  Type theory plays an important role in foundations of mathematics as a
framework for formalizing mathematics and a base for proof assistants providing
semi-automatic proof checking and construction. Derivation of each theorem in
type theory results in a formal term encapsulating the whole proof process. In
this paper we use a variant of type theory, namely the Calculus of
Constructions with Definitions, to formalize the standard theory of binary
relations. This includes basic operations on relations, criteria for special
properties of relations, invariance of these properties under the basic
operations, equivalence relation, well-ordering, and transfinite induction.
Definitions and proofs are presented as flag-style derivations.
