  This paper introduces Relational Type Theory (RelTT), a new approach to type
theory with extensionality principles, based on a relational semantics for
types. The type constructs of the theory are those of System F plus relational
composition, converse, and promotion of application of a term to a relation. A
concise realizability semantics is presented for these types. The paper shows
how a number of constructions of traditional interest in type theory are
possible in RelTT, including eta-laws for basic types, inductive types with
their induction principles, and positive-recursive types. A crucial role is
played by a lemma called Identity Inclusion, which refines the Identity
Extension property familiar from the semantics of parametric polymorphism. The
paper concludes with a type system for RelTT, paving the way for
implementation.
