Type : Type is good enough to get started!

Girard's paradox hurts less than trying to avoid Girard's paradox 2026-03-25

by Luna Nova

---

Working on a new dependently typed language that isn't also doing proofs?

Type : Type is good enough! Don't bother implementing a universe hierarchy. It's fine.
You can fix it in V2, or once you're self-hosting.

If you try to do it right from the start you'll spend a lot of time handling it, and almost inevitably your V1 will be unsound anyway, whether from your universe hierarchy being flawed or from unrelated mistakes.

We can learn from the mistakes of the past to avoid repeating the probable mistakes of the future for the first time. Idris 2 is still Type-in-Type.

If you're writing the a proof system, please disregard.

@online{type-in-type-is-good-enough,
    author = {Luna Nova},
    title = {Type : Type is good enough to get started!},
    date = {2026-03-25},
    year = {2026},
    url = {https://lunnova.dev/articles/type-in-type-is-good-enough/},
}

tagged type-theory