Cantor.lean

def cantor_sur (f : α → (α → Prop)) : { g // ∀ x, g ≠ f x } :=
  ⟨fun x => ¬f x x, fun x h => not_iff_self <| iff_of_eq <| congrFun h x⟩

def cantor_inj (f : (α → Prop) → α) : { g // ¬(∀ {h}, f g = f h → g = h) } :=
  let g x := ∀ h, x = f h → ¬h x
  ⟨g, fun inj => @not_iff_self (g (f g)) ⟨fun p _ q => inj q ▸ p, fun p => p g rfl⟩⟩

namespace NonStrictlyPositiveInductive

unsafe inductive T
  | mk (f : (T → Prop) → Prop)

unsafe def T.mk.inj : mk f = mk g → f = g :=
  Eq.rec (motive := rec fun g _ => f = g) rfl

unsafe def inject (f : T → Prop) : T :=
  .mk (Eq f)

unsafe def inject.inj (p : inject f = inject g) : f = g :=
  (congrFun (T.mk.inj p) g).mpr rfl

unsafe def bad : False :=
  (cantor_inj inject).property inject.inj

end NonStrictlyPositiveInductive

namespace TypeConstructorInjectivity

inductive T (F : Type → Prop)

axiom T.inj {F G} : T F = T G → F = G

theorem bad : False :=
  (cantor_inj T).property T.inj

end TypeConstructorInjectivity