Questions tagged [eliminator]

eliminators are proof relevant eliminations.

1 question with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
3 votes
0 answers
122 views

Uniform notions of pattern matching at dependent types with impredicative proof strength

I am looking for axioms/inference rules that satisfy the following 3 conditions: can be added to predicative intensional Martin-Löf type theory, so $\Pi$, $\Sigma$, equality type, with W-types, ...
Ilk's user avatar
  • 547