The definition of type equivalence plays a crucial role in any statically typed language. In dependent type theories, there is no syntactic distinction between terms and types, and this notion of equivalence, generally referred to as conversion, is fundamental for typechecking.

Dependent type theories are classified in two categories according to the way in which conversion is handled:

extensional type theories (as implemented in NuPRL) identify conversion with propositional equality (expressed as a type and used for reasoning) resulting in powerful systems with undecidable typechecking;

intensional type theories (as implemented in Coq, Agda and Epigram) use a decidable notion of conversion, typically β-equivalence, and rely on strong normalisation to guarantee decidable typechecking. In the talk we will focus on this class.

The talk will consist of two parts: first I will show that in some cases the notion of conversion present in intesional type theories can be too weak. I will do so through a set of simple practical examples developed in Agda2. In the second part I will informally review some research aimed at extending conversion without compromising decidability of typechecking.