【Arend Theorem Prover 連載（初回）】「同型なものは等しい」を機械に検査させる ── 定理証明支援系 Arend がHoTTを公理としなかった理由 - Qiitaどちらも「Bool と Bool は等しい」ことの根拠です。 対応のつけ方が、２通りあります。 true と false を、元の値のまま比べる対応づけ と、 両者を論理反転した結果どうしを比べる対応づけ の ２つの対応付け です。 どちらも、Bool の要素と Bool の要素を過不足なく一対一に対応づけていますので、 いずれも「Bool と Bool は等しい」ことの根拠となります。 しかし、対応のつけ方そのものは別物 です。 等しさの根拠が、２つ存在する ことになります。 従来の型理論では、この区別ができませんでした。 等しいなら等しい。根拠は１通りに潰れていた のです。 ここまでの議論を数学的により厳密に述べてみましょう。 ここでいう「対応づけ」は、単なる全単射ではなく、型の 同値（equivalence）を指します。 Bool には、自分自身への同値が少なくとも２つあります。 １
