Post #2775974
2026-05-12 20:51 UTC
@jonmsterling@mathstodon.xyz @ncf@types.pl @jeanas@mathstodon.xyz There are some things I'd like to keep that don't admit an eliminator translation: Higher inductive-inductives and single (higher?) IR
Replies (1)
-
@jonmsterling@mathstodon.xyz 2026-05-12 20:53
@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?