Use for proof assistants or type theories featuring an equality type that has a reflection rule creating judgemental equalities out of them. See also [reflection].
Use for proof assistants or type theories featuring an equality type that has a reflection rule creating judgemental equalities out of them. See also reflection.
Equality reflection typically refers to the rule
$$\frac{\Gamma \vdash \text{Id}(s,t)}{\Gamma\vdash s \equiv t}$$
which typically renders type-checking undecidable.
