Post #2775973
2026-05-12 20:36 UTC
@ncf@types.pl @jeanas@mathstodon.xyz @totbwf@types.pl No time like the present ;-)
Replies (1)
-
@totbwf@types.pl 2026-05-12 20:51
@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