「贅沢なグロタンディーク宇宙とPropositions-As-Types」に対して、老婆心的な補足をします。$`\newcommand{\mrm}[1]{\mathrm{#1} } \newcommand{\mbf}[1]{\mathbf{#1} } \newcommand{\In}{\text{ in }} `$内容： 「命題」を排除したい！ ベリティ型とその型…