Post #2775976
2026-05-12 21:05 UTC
@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?
Replies (2)
-
@AndrasKovacs@mathstodon.xyz 2026-05-12 21:07
@ncf@types.pl @jonmsterling@mathstodon.xyz @totbwf@types.pl @jeanas@mathstodon.xyz All of IR, II and HII types can be specified in terms of eliminators. The only relevant thing that's missing from literature is HII eliminators in cubical TTs.
-
@jonmsterling@mathstodon.xyz 2026-05-13 05:12
@ncf@types.pl @totbwf@types.pl @jeanas@mathstodon.xyz Yeah, of course.