proposition: Lemma Cantor_sing (i : (X -> HProp) -> (X -> HProp)) : IsInjective i -> exists p, ~ sing (i p).
proof: Proof. intros HI. pose (p n := Build_HProp (resize_hprop (forall q, i q = hpaths n -> ~ q n))). exists p. intros [n HN]. enough (Hp : p n <-> ~ p n). { apply Hp; apply Hp; intros H; now apply Hp. } unfold p at 1. split. - intros H. apply equiv_resize_hprop in H. apply H, HN. - intros H. apply equiv_resize_hprop. intros q HQ. rewrite <- HN in HQ. now apply HI in HQ as ->. Qed.
imports: HoTT(TruncType abstract_algebra) HoTT(PropResizing.PropResizing) HoTT(Spaces.Nat.Core Spaces.Card)