- type-theory undecidability
- Updated Tue, 07 Jun 2022 11:55:13 GMT

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