Homotopy type theory（ホモトピー・型理論）は、集合論の代替になりうる。 集合論は第一階述語論理の証明システム→ZFC集合論の二層から成り立っているが、型理論は第一階述語論理といった上位層の内部として理論を位置付ける必要がない。なぜなら命題は特定…