<p>Your question is very brief, so my answer will be as well:</p>

<pre><code>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)
  }.
</code></pre>

CC BY-SA 3.0
2013-04-15T06:20:48.163Z
2013-04-15T06:20:48.163Z
Andrej Bauer
<p>What are the ways in which one can add a decidable equivalence relation in a type system with undecidable type checking/extensional equality?</p>

CC BY-SA 3.0
2013-04-14T17:48:32.860Z
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
<type-theory><undecidability>
Decidability in Extensional Type Theory
AnaK
# Decidability in Extensional Type Theory

(Asked by: username_0 on 2013-04-14)

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

**Tags:** type-theory, undecidability

> **Comments:**
> **username_1**: 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].  

---

## 1 answers

### Answer by username_2 on 2013-04-15. Score: 2 | Accepted answer

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)
  }.


---

