A proof in Coq that `Set -> bool` is not equal to `Set`.

Set2Bool.v

Require Import Setoid.

Definition coerce {A B : Type} : A = B -> A -> B.
Proof.
  intros [] a.
  exact a.
Defined.

Lemma coerce_coerce {A B : Type} (e : A = B) (b : B) :
  coerce e (coerce (eq_sym e) b) = b.
Proof.
  now destruct e.
Defined.

Lemma eq_arg (A B : Type) (f g : A -> B) (a : A) :
  f = g -> f a = g a.
Proof.
  now intros [].
Defined.

Theorem Lawvere {A B : Type} : (A = (A -> B)) -> forall (f : B -> B), { x : B | x = f x }.
Proof.
  intros E f.
  pose (g := fun (a : A) => f (coerce E a a)).
  pose (x := coerce (eq_sym E) g).
  exists (g x).
  unfold g at 1.
  f_equal.
  apply eq_arg.
  unfold x.
  apply coerce_coerce.
Qed.

Lemma KyleStemen : Set = (Set -> bool) -> False.
Proof.
  intro e.
  absurd (true = false).
  - discriminate.
  - destruct (Lawvere e negb) as [[|] eq].
    + assumption.
    + now symmetry.
Qed.