(* Proof showing that the universe is not a set *)
Require Import HoTT.
Section UniverseNotSet.
(* Want to assume the univalence axiom and function extensionality (the former implying the latter) *)
Context `{Univalence} `{Funext}.
(* It's useful to make the homotopy asserted by univalence explicit
We can think of it as a propositional computation rule for path_universe_uncurried *)
Definition beta_path_universe_uncurried {A B : Type} (f : A <~> B)
: equiv_path A B (path_universe_uncurried f) = f
:= eisretr (equiv_path A B) f.
(* Same for the underlying function of an equivalence *)
Definition beta_path_universe {A B : Type} (f : A -> B) {feq : IsEquiv f}
: equiv_fun A B (equiv_path A B (path_universe f)) = f
:= ap (equiv_fun A B) (eisretr (equiv_path A B) (BuildEquiv _ _ f feq)).
(* negb is the 'flip' map Bool -> Bool defined in the library. Show that it's not equal to the identity map *)
Lemma negb_ne_idmap : (negb = idmap) -> Empty.
Proof.
(* Introduce a hypothetical equality proof *)
intro negb_eq_idmap.
(* It's already shown in the library that (false = true) -> Empty *)
apply false_ne_true.
(* Now we get false = true by evaluating the equality of functions negb = idmap on true *)
apply (ap10 negb_eq_idmap true).
Defined.
(* This leads us the theorem that the path corresponding to negb uder univalence is not the constant path
negb automatically gets recognized as an equivalence due to isequiv_negb from the library *)
Theorem negb_path_ne_refl : (path_universe negb = idpath) -> Empty.
Proof.
(* Introduce a hypothetical 2-path *)
intro two_path.
(* By the previous lemma, it's enough to derive negb = idmap *)
apply negb_ne_idmap.
(* negb is the underlying equivalence of the path (path_universe negb) *)
rewrite <- (beta_path_universe negb).
(* Now use the assumed 2-path *)
rewrite two_path.
(* The rest is computation *)
unfold equiv_path.
simpl; trivial.
Defined.
(* It easily follows that the universe is not a set *)
Corollary not_set_universe : (IsHSet Type) -> Empty.
Proof.
(* Assume that it is a set *)
intro set_proof.
(* We already have two parallel paths that are not equal *)
apply negb_path_ne_refl.
(* The contradictory 2-path follows from the assumption in the form of Axiom K *)
apply axiomK_hset.
assumption.
Defined.
End UniverseNotSet.