一連のシリーズ記事（最初の記事は「最近の型理論： 宇宙と世界、そして銀河」）を始めた目的は、最近のプログラミング言語・証明支援系 Lean、Agda、Coq などが備えている型システムの背景となっている「階層化された宇宙達を備えた型理論」を調べて紹介す…