Skip to content

Instantly share code, notes, and snippets.

@andrejbauer
Created May 25, 2022 22:08
Show Gist options
  • Save andrejbauer/4623bba71854332cc9f396cdd22524fb to your computer and use it in GitHub Desktop.
Save andrejbauer/4623bba71854332cc9f396cdd22524fb to your computer and use it in GitHub Desktop.
A proof in Coq that `Set -> bool` is not equal to `Set`.
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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment