ホモトピー型理論
[004G]

\(\mathbf {0}\)は命題である。実際、帰納法で直ちに示せる。