Try out Homotopy Type Theory

[awalterschulze]

No description provided.

[awalterschulze]

-- UIP => unique identity => (a = b) = (a = b)
example {α : Type u} {a b : α} (p q : a = b) : p = q := by
  cases p
  cases q
  reflexivity

-- HoTT => !UIP => don't have unique identity => (a = b) = (a = b) ⋃ (a = b) != (a = b)
-- !UIP !=> HoTT
-- !large elimination in Lean => !UIP
-- hott example {α : Type u} {a b : α} (p q : a = b) : p = q := by
--   cases p
--   cases q
--   reflexivity

-- Agda K rule => allows pattern matching on refl => UIP
-- K : {A : Set} {x : A} (P : x ≡ x → Set) →
--     P refl → (x≡x : x ≡ x) → P x≡x
-- K P p refl = p

-- K rule is only used by Agda
-- without K => !UIP
-- without K => can use J rule
-- J rule is used by Coq, Lean, etc.
-- Coq has proof relevance
-- Lean has proof irrelevance and large elimination
-- !large elimination => proof relevance

-- "If you do need specifically proof-relevant equality, I would switch to Coq or Agda. Lean actively works against you in that case." - Jannis Limperg

-- K rule is better at infering types than the J rule, especially for False proofs, in our experience