Skip to main content

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 .

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.