Post #2775975
2026-05-12 20:53 UTC
@totbwf@types.pl @ncf@types.pl @jeanas@mathstodon.xyz I’m just not sure how we can believe that stuff is valid if you don’t know how to turn it to eliminators. Doesn’t this worry you?
Replies (1)
-
@ncf@types.pl 2026-05-12 21:05
@jonmsterling@mathstodon.xyz @totbwf@types.pl @jeanas@mathstodon.xyz I think we need to be more precise about "translation to eliminators" here: of course IR doesn't admit a translation to eliminators relative to a type theory without IR (unless you restrict to small IR), but inductive-recursive types themselves can be specified in terms of eliminators, I think?