# Decidability in Extensional Type Theory

What are the ways in which one can add a decidable equivalence relation in a type system with undecidable type checking/extensional equality?

• Some motivation and background for the question would be helpful. Please see the tips about how to write a better question section of our FAQ. – Kaveh Apr 14 '13 at 17:48

Structure DecidableEquivalenceRelation :=