Toot

Written by Andrej Bauer on 2024-10-12 at 17:49

After a bit more thinking, the following should be a better version. Suppose 𝐿 is a set of levels and 𝗌𝗎𝖼𝖼 : 𝐿 → 𝐿 an endomap without cycles. Is there a type theory with universes indexed by 𝐿, such that (U_i : U_{\mathsf{succ}(i)}) for all (i \in L)? Once again, each universe should be non-trivial, as described above.

=> More informations about this toot | View the thread | More toots from andrejbauer@mathstodon.xyz

Mentions

Tags