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.