# 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

Your question is very brief, so my answer will be as well:

Structure DecidableEquivalenceRelation :=
{
carrier :> Type ;
rel :> carrier -> carrier -> Prop ;
reflexive : forall x, rel x x ;
symmetric : forall x y, rel x y -> rel y x ;
transitive : forall x y z, rel x y -> rel y z -> rel x y ;
decidable : forall x y, (rel x y) + ~ (rel x y)
}.