/Paradox.lean at main - miscelleaneous

-- https://leanprover.zulipchat.com/#narrow/channel/236446-Type-theory/topic/Paradoxes.20and.20Type.20Universes/with/538016579

import Mathlib

axiom Bad : Type

axiom bad : (α : Type) × α ↪ Bad

noncomputable section

def k (P : Bad → Prop) : Bad :=
  bad ⟨Bad → Prop, P⟩

def Q (b : Bad) : Prop :=
  ∃ P, k P = b ∧ ¬P b

theorem k_injective : k.Injective :=
  fun _ _ hab => eq_of_heq
    (Sigma.mk.inj (bad.injective hab)).2

theorem down (h : Q (k Q)) : ¬Q (k Q) :=
  h.elim fun _ hP =>
    (congrArg Not (congrFun (k_injective hP.1) (k Q))).mp hP.2

theorem up (h : ¬Q (k Q)) : Q (k Q) :=
  ⟨Q, rfl, h⟩

theorem false : False :=
  down (up fun h => down h h) (up fun h => down h h)

-- 'false' depends on axioms: [Bad, bad]
#print axioms _root_.false




def girard' (α : Type) (bad : (β : Type) × β ↪ α) : False :=
  and_not_self ⟨fun _ _ hab ↦ eq_of_heq (Sigma.mk.inj (bad.injective hab)).2, (bad ⟨Set α, ·⟩).cantor_injective⟩


lemma blah (p : α → Prop) (x : α) (h : p x) : (Subtype.mk x h).val = x := by
  grind

theorem subtype_eq_implies_predicate_eq {A : Type 1} {P Q : A → Prop}
    (h : {a : A // P a} = {a : A // Q a}) : ∀ a, P a ↔ Q a := by
  intro a
  constructor
  · intro hpa
    let a' : {x : A // P x} := ⟨a, hpa⟩
    have : a'.val = a := by
      grind
    rw [h] at a'
    have : a = a'.val := by
      exact blah P a hpa
    exact this ▸ a'.prop
  · intro hqa
    have a' : {x : A // Q x} := ⟨a, hqa⟩
    have : a = a'.val := by
      exact Subtype.mk
    rw [← h] at a'
    have : a = a'.val := by
      sorry
    exact this ▸ a'.prop


#check Function.surjective_iff_hasRightInverse

theorem not_surjective_Type (f : Type → Type 1) : ¬f.Surjective := by
  intro hf
  -- let g := f.surjInv hf
  -- have g.Injective := f.injective_surjInv hf
  let T : Type 1 := Sigma f
  cases hf (Set T) with | intro U hU =>
  let g : Set T → T := fun s ↦ ⟨U, cast hU.symm s⟩
  have hg : g.Injective := by
    intro s t h
    suffices cast hU (g s).2 = cast hU (g t).2 by
      simp only [g, cast_cast, cast_eq] at this
      assumption
    · congr
  exact g.cantor_injective hg



def girard (f : Type (u + 1) ↪ Type u) : False := by
  let g := f.toFun.invFun
  have hg : g.Surjective := by
    intro a
    use f.toFun a
    simp [g, Function.invFun]
  let T := Sigma g
  obtain ⟨U, hU⟩ := hg (Set T)
  let k (s : Set T) : T :=
    ⟨U, cast hU.symm s⟩
  have hk : k.Injective := by
    intro s t _
    have : cast hU (k s).2 = cast hU (k t).2 := by congr
    simpa [k]
  -- Now we have an injective function `k` from `Set α → α` (intuitively this is like a function from the power set to a set) which violates `Function.cantor_injective k`
  -- Here's how to manually finish the proof
  -- This is like the set of sets that don't contain themselves
  let Q := { b : T | ∃ P, k P = b ∧ b ∉ P }
  -- If `k Q ∈ Q`, then there exists `P` with `k P = k Q` and `k Q ∉ P`, but `k` is injective so `P = Q` and `k Q ∉ Q`
  have down (h : k Q ∈ Q) : k Q ∉ Q := by
    obtain ⟨P, hP⟩ := h
    exact (hk hP.1) ▸ hP.2
  -- If `k Q ∉ Q` then choose `P := Q` so `k Q ∈ Q` holds by definition
  have up (h : k Q ∉ Q) : k Q ∈ Q :=
    ⟨Q, rfl, h⟩
  -- Now use a diagonalization argument (alternatively, we can use the law of excluded middle)
  let f := fun h ↦ down h h
  exact f (up f)





  -- let hf := Function.invFun_surjective f.inj'
  -- and_not_self ⟨Function.invFun_surjective f.inj', Function.not_surjective_Type.{1, 1} f.toFun.invFun⟩
  -- let T : Type 2 := Sigma bad
  -- let k (P : Set T) : T := ⟨Set Type, P⟩
  -- have k_injective : k.Injective := by
  --   intro a b hab
    -- exact eq_of_heq (Sigma.mk.inj hab).2
     --eq_of_heq (Sigma.mk.inj (bad.injective hab)).2



  -- let k (P : Set Type) : Type := bad P
  -- have : k.Injective := by
  --   intro a b hab
  --   -- have := bad.injective hab
  --   -- have : { x // a x } = { x // b x } := bad.injective hab
  --   exact Set.ext <| subtype_eq_implies_predicate_eq <| bad.injective hab
  -- exact and_not_self ⟨this, k.cantor_injective⟩




-- The same proof works for any type in `Type`, not just `Unit`
-- Uncomment this line to prove false
axiom bad : Type 1 ↪ Type

/-- An injective function from sets of `Unit` to `Unit` (internally, a `Set α` is an `α → Prop` predicate for set membership) -/
noncomputable def k (P : Set Type) : Type :=
  bad P

/-- `k` is injective because the sigma constructor and `bad` are injective -/
lemma k_injective : k.Injective :=
  fun a b hab ↦ by
    have := bad.injective hab
    have blah : {x // x ∈ a} = {x // x ∈ b} := this
    have : (fun x ↦ x ∈ a) = (fun x ↦ x ∈ b) := by
      ext x
      constructor
      · intro h
        let y : {x // x ∈ a} := ⟨x, h⟩
        have : x = y.val := by grind
        let := cast blah y
        have : x = this.val := by grind


      by_cases h : ∃ y : {x // x ∈ a}, y = x
      · obtain ⟨y, hy⟩ := h
        have := cast blah y
        have z : {x // x ∈ b} := ⟨y.val, by
          have := y.prop

          ⟩
      · sorry
    grind

/-- This is like the set of sets that don't contain themselves -/
def Q : Set Type :=
  { b : Type | ∃ P, k P = b ∧ b ∉ P }

/-- If `k Q ∈ Q`, then there exists `P` with `k P = k Q` and `k Q ∉ P`, but `k` is injective so `P = Q` and `k Q ∉ Q` -/
lemma down (h : k Q ∈ Q) : k Q ∉ Q := by
  obtain ⟨P, hP⟩ := h
  exact (k_injective hP.1) ▸ hP.2

/-- If `k Q ∉ Q` then choose `P := Q` so `k Q ∈ Q` holds by definition -/
lemma up (h : k Q ∉ Q) : k Q ∈ Q :=
  ⟨Q, rfl, h⟩

/-- Now use a diagonalization argument (alternatively, we can use the law of excluded middle) -/
theorem false : False :=
  let f := fun h ↦ down h h
  f (up f)



-- We can't actually assign `Type` a different type, but we can assume there's a bad injective function from a sigma (dependent product) type in `Type 1` to some type in `Type`. Intuitively, this sigma type is "too big" to fit in something in `Type`. (Thanks to Aaron Liu and Paul Reichert on the Lean Zulip for this proof.)

def girard'' (α : Type) (bad : (β : Type) × β ↪ α) : False := by
  -- An injective function from sets of `α` to `α` (internally, a `Set α` is an `α → Prop` predicate for set membership)
  let k (P : Set α) : α := bad ⟨Set α, P⟩
  -- `k` is injective because the sigma constructor and `bad` are injective
  have k_injective : k.Injective :=
    fun _ _ hab ↦ eq_of_heq (Sigma.mk.inj (bad.injective hab)).2
  -- Now we have an injective function `k` from `Set α → α` (intuitively this is like a function from the power set to a set) which violates `Function.cantor_injective k`
  -- Here's how to manually finish the proof
  -- This is like the set of sets that don't contain themselves
  let Q := { b : α | ∃ P, k P = b ∧ b ∉ P }
  -- If `k Q ∈ Q`, then there exists `P` with `k P = k Q` and `k Q ∉ P`, but `k` is injective so `P = Q` and `k Q ∉ Q`
  have down (h : k Q ∈ Q) : k Q ∉ Q := by
    obtain ⟨P, hP⟩ := h
    exact (k_injective hP.1) ▸ hP.2
  -- If `k Q ∉ Q` then choose `P := Q` so `k Q ∈ Q` holds by definition
  have up (h : k Q ∉ Q) : k Q ∈ Q :=
    ⟨Q, rfl, h⟩
  -- Now use a diagonalization argument (alternatively, we can use the law of excluded middle)
  let f := fun h ↦ down h h
  exact f (up f)