proposition: Lemma Cantor_inj {PR : PropResizing} {FE : Funext} X : ~ Injection (X -> HProp) X.
proof: Proof. intros [i HI]. pose (p n := Build_HProp (resize_hprop (forall q, i q = n -> ~ q n))). enough (Hp : p (i p) <-> ~ p (i p)). { apply Hp; apply Hp; intros H; now apply Hp. } unfold p at 1. split. - intros H. apply equiv_resize_hprop in H. apply H. reflexivity. - intros H. apply equiv_resize_hprop. intros q -> % HI. apply H. Qed.
imports: HoTT(TruncType abstract_algebra) HoTT(PropResizing.PropResizing) HoTT(Spaces.Nat.Core Spaces.Card)