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

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?

Solution

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





References