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?
Your question is very brief, so my answer will be as well:

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