UIP と関数外延性の独立性

定理 5.3（「依存型理論」§5）・ ※主張のみ

MLTT（Π・Σ・Id・ℕ・宇宙をもつ内包的型理論）では、次の二つはどちらも証明も反証もできない。

（UIP：等号の証明の一意性） $\Pi_{(a,b:A)}\Pi_{(p,q:\mathrm{Id}_A(a,b))}\mathrm{Id}(p,q)$ 。
（関数外延性） $f,g:\Pi_{(x:A)}B(x)$ について $\bigl(\Pi_{(x:A)}\mathrm{Id}(f\,x,g\,x)\bigr)\to\mathrm{Id}(f,g)$ 。

閉包の状態

※ 主張のみ

証明を Rikai に書かない定理です（研究最前線の結果や、証明が本 1 冊分になるもの）。主張のみの台帳に理由つきで登録されています。理由と出典は本文の注意にあります。

印の意味: ✓公理まで証明済み・ △証明あり（閉包未完）・ ※主張のみ。テーマごとの集計は閉包の状況。

主張のみなので、Rikai の中で証明が使う前提はありません。

証明で明示的に参照している定理は、まだありません。