HEq and K

K.lean

universe u v

inductive Eq' {α : Sort u} : α → α → Sort (max u 1) where
  | refl (x : α) : Eq' x x

infix:50 " ≡ " => Eq'

def Eq'.rfl {α : Sort u} {x : α} : x ≡ x := refl x

noncomputable def Eq'.subst {α : Sort u}
  {motive : α → Sort v} {x y : α}
  (h₁ : x ≡ y) (h₂ : motive x) : motive y := Eq'.rec h₂ h₁

noncomputable def Eq'.symm {α : Sort u} {x y : α} (h : x ≡ y) : y ≡ x :=
  Eq'.subst (motive := fun z => z ≡ x) h rfl

theorem Eq'.heq {α : Sort u} (x y : α) (h : x ≡ y) : x ≍ y :=
  subst h HEq.rfl

axiom HEq.rec' {α : Sort u} {x : α} {motive : (y : α) → x ≍ y → Sort v}
      (refl : motive x (HEq.refl x)) {y : α} (h : x ≍ y) : motive y h

#check HEq.rec
#check HEq.rec'
#check PProd

def sig' {α : Sort u} (x y : α)
    (h : (⟨α, x⟩ : Σ' α : Sort u, α) ≡ (⟨α, y⟩ : Σ' α : Sort u, α)) : x ≡ y := by
  cases h
  constructor

set_option pp.proofs true
#reduce sig'

#check (α : Sort u) ×' α
#check Σ' α : Sort u, α
#check @PSigma (Sort u) (fun (α : Sort u) => α)

noncomputable def HEq.eq' {α : Sort u} (x y : α) (h : x ≍ y) : x ≡ y :=
  HEq.rec' (motive := fun x' _ => x ≡ x') Eq'.rfl h

def sigma_of_heq {α : Sort u} {x : α}
    {β : Sort u} (y : β)
    (h : x ≍ y) : (⟨α, x⟩ : Σ' α : Sort u, α) ≡ (⟨β, y⟩ : Σ' β : Sort u, β) :=
  HEq.rec
    (motive := fun {γ} y' _ => @Eq' (Σ' α : Sort u, α) ⟨α, x⟩ ⟨γ, y'⟩)
    Eq'.rfl
    h

def heq_of_sigma {α : Sort u} {x : α}
    {β : Sort u} (y : β)
    (h : (⟨α, x⟩ : Σ' α : Sort u, α) ≡ (⟨β, y⟩ : Σ' β : Sort u, β)) : x ≍ y :=
  let S : Σ' α : Sort u, α := ⟨α, x⟩
  let T : Σ' β : Sort u, β := ⟨β, y⟩
  have heq : S.2 ≍ T.2 := Eq'.subst (motive := fun S' => S.2 ≍ S'.2) h HEq.rfl
  heq


def K' {α : Sort u} (x : α)
  {motive : x = x → Sort v}
  (d : motive (Eq.refl x))
  (z : x = x) :
  motive z := d

noncomputable def eq_uip {α : Sort u} (x : α) (z : x ≡ x) : z ≡ (Eq'.refl x) := by
  apply HEq.eq'
  apply heq_of_sigma
  exact Eq'.rec
    (motive := fun x' q =>
      @Eq' (Σ' α : Sort (max 1 u), α) ⟨x ≡ x', q⟩ ⟨x ≡ x, Eq'.refl x⟩)
    Eq'.rfl
    z

noncomputable def eq_uip' {α : Sort u} (x : α) (z : x ≡ x) : z ≡ (Eq'.refl x) := by
  cases z
  exact Eq'.rfl

#print eq_uip'
#print eq_uip'._proof_1
#print eq_uip'._proof_2
#check Eq'.rec

noncomputable def eq_uip'' {α : Sort u} (x : α) (z : x ≡ x) : z ≡ (Eq'.refl x) :=
  Eq'.rec
    (motive := fun y h => x = y → z ≍ h → z ≡ Eq'.refl x)
    (fun _ heq => Eq.rec (motive := fun y _ => z ≡ y) (Eq'.refl z) (eq_of_heq heq))
    z
    rfl
    HEq.rfl

noncomputable def K {α : Sort u} (x : α)
  {motive : x ≡ x → Sort v}
  (d : motive (Eq'.refl x))
  (z : x ≡ x) :
  motive z := Eq'.subst (Eq'.symm <| eq_uip x z) d

example {α : Sort u} {x : α} (h : x = x) : h = rfl := rfl

noncomputable example {α : Sort u} {x : α} (h : x ≡ x) : h ≡ Eq'.rfl :=
  K (motive := fun z => z ≡ Eq'.rfl) x Eq'.rfl h