1. 1
2. 2
3. 3
4. 4
5. 5
6. 6
7. 7
8. 8
9. 9
10. 10
11. 11
12. 12
13. 13
14. 14
15. 15
16. 16
17. 17
18. 18
19. 19
20. 20
21. 21
22. 22
23. 23
24. 24
25. 25
26. 26
27. 27
28. 28
29. 29
30. 30
31. 31
32. 32

-- 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