為什麼UIP跟univalence不能並存

{-# OPTIONS --without-K #-}
open import MLTT.Spartan
open import MLTT.Bool
open import UF.Base
open import UF.Equiv
open import UF.Retracts
open import UF.Univalence

module ag-WN45 (ua : is-univalent 𝓤₀) where

首先，我們知道 not 是自己的反函數，也就是說 not 有 section 也有 retraction，這導致 not 是一個 Bool 的 equivalence

equiv-not : Bool ≃ Bool
equiv-not = not , sec , ret
  where
  I : (x : Bool) → not (not x) ＝ x
  I true = refl
  I false = refl

  sec : has-section not
  sec = not , I
  ret : is-section not
  ret = not , I

對於 equivalence e，我們知道取其路徑函數會等於 ⌜ e ⌝，因此我們反過來從函數去取其路徑。藉由 UIP，我們迫使所有路徑都等於 refl，又從 Idtofun refl 得出 id，因此證明了 not ＝ id

postulate UIP : {X : 𝓤 ̇ } → (x y : X) → (p q : x ＝ y) → p ＝ q

equiv-id : Bool ≃ Bool
equiv-id = id , (id , λ x → refl) , id , λ x → refl

not-＝-id : not ＝ id
not-＝-id =
  not                                     ＝⟨by-definition⟩
  ⌜ equiv-not ⌝                           ＝⟨ (Idtofun-eqtoid ua equiv-not) ⁻¹ ⟩
  Idtofun (eqtoid ua Bool Bool equiv-not) ＝⟨ ap Idtofun uip-claim ⟩
  Idtofun refl                            ＝⟨by-definition⟩
  id ∎
  where
  not-path : Bool ＝ Bool
  not-path = eqtoid ua Bool Bool equiv-not

  uip-claim : not-path ＝ refl
  uip-claim = UIP Bool Bool not-path refl

到這邊就已經歸結出一個荒謬的結果，我們接著看怎麼把這個結果用來導出 𝟘 證明這樣會導致系統不一致。

根據定義 false ＝ id false
藉由 not ＝ id 把 id false 改成 not false
根據定義 not false ＝ true

得出了 false ＝ true，然而我們知道 true ≠ false

false-is-true : false ＝ true
false-is-true =
  false     ＝⟨by-definition⟩
  id false  ＝⟨ happly not-＝-id true ⟩
  not false ＝⟨by-definition⟩
  true ∎

ua-negates-UIP : 𝟘
ua-negates-UIP = true-is-not-false (false-is-true ⁻¹)

為什麼UIP跟univalence不能並存 [ag-WN45]