摘要：We prove an extensionality theorem for the "type-in-type" dependent type theory with Sigma-types. We suggest that in type theory the notion of extensional equality be identified with the logical equivalence relation defined by induction on type structure.
关键词：Extensionality; logical relations; type theory; lambda calculus; reflection
