← Feed @carloangiuli@mathstodon.xyz Post #2062620 2026-05-06 01:47 UTC @totbwf > In particular, we put some indexed inductives in Typeω to avoid generating the extra cubical code. lmao. @stschaef @amy @ncf Replies (0) No replies.