{PR : PropResizing} {FE : Funext} X : ~ Injection (X -> HProp) X. Proof. intros [i HI]. pose (p n := Build_HProp (smalltype (forall q, i q = n -> ~ q n))). enough (Hp : p (i p) <-> ~ p (i p)). { apply Hp; apply Hp; intros H; by apply Hp. } unfold p at 1. split. - intros H. apply equiv_smalltype in H. apply H. reflexivity. - intros H. apply equiv_smalltype. intros q -> % HI. apply H. Qed.
From HoTT Require Import TruncType abstract_algebra. From HoTT Require Import Universes.Smallness. From HoTT Require Import Spaces.Nat.Core Spaces.Card.