We report our work on a new treatment of equality in dependent type theory.

Large-scale formalization of mathematics in type theory is greatly impededed by the intensional character of type-theoretic equality. For a variable n:Nat, the terms n+1 and 1+n are equal but not convertible. Consequently, if B(n) is a dependent type over N (eg. R^n), then B(n+1) and B(1+n) are isomorphic but not equal; thus there is no automatic way to transfer properties from one type to another. The terms S=(\n.n+1) and S'=(\n.1+n) of type Nat->Nat are not even equal propositionally, thus there is no explicit isomorphism between types B(S) and B(S') when B(f) is a type dependent over Nat->Nat. Martin-Lof defined extensional type theory by reflecting the equality proofs (terms of the identity type) into the conversion relation. Unfortunately, this renders type-checking and proof-checking undecidable, undermining a major motivation for working in type theory.

Voevodsky recently proposed the Univalence Axiom which solves the problem of extensionality, but, without a computational justification, leads to the failure of canonicity, another crucial metatheoretic property. Coquand et al have recently provided this missing piece by building a model of univalence in constructive metatheory.

We propose an alternative, syntax-based approach to extensionality. In this approach, the equality type is initially defined externally, as a logical relation on the term model of type theory, which in turn is defined by induction on type structure. The relation is then reflected into the language by extending the syntax. This results in a 1-dimensional theory; in order to have equality as a type constructor that can be iterated (so that we can write p,q : Eq(A,a,b), pi : Eq(Eq(A,a,b),p,q), etc.), the reflection operation must itself be internalized. We show how this can be done in a consistent way, and verify some basic properties of the resulting system.