記事タイトルの「最近の」は、「理論的には古くから知られていても、実用的利用は最近になって出てきた」といった意味です。さらに具体的な特徴として、「階層化された宇宙達を備えた型理論」のことです。そのような型理論は、Lean, Agda, Coq などの型システムの背景理論になっています。この記事では、「階層化された宇宙達を備えた型理論」における構文論と意味論のおおよその枠組みを述べます。以下の過去記事で述べたことを利用します。$`\newcommand{\cat}[1]{\mathcal{#1}} \newcommand{\mrm}[1]{\mathrm{#1}} \newcommand{\In}…