(i : (X -> HProp) -> (X -> HProp)) : IsInjective i -> exists p, ~ sing (i p). Proof. intros HI. pose (p n := Build_HProp (smalltype (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; by apply Hp. } unfold p at 1. split. - intros H. apply equiv_smalltype in H. apply H, HN. - intros H. apply equiv_smalltype. intros q HQ. rewrite <- HN in HQ. by apply HI in HQ as ->. Qed.
From HoTT Require Import TruncType abstract_algebra. From HoTT Require Import Universes.Smallness. From HoTT Require Import Spaces.Nat.Core Spaces.Card.