{Z} (r : Z -> HProp) : IsInjective (@proj1 Z r). Proof. intros [p Hp] [q Hq]; cbn. intros ->. unshelve eapply path_sigma; cbn. - reflexivity. - cbn. apply path_ishprop. Qed.
From HoTT Require Import TruncType abstract_algebra. From HoTT Require Import Universes.Smallness. From HoTT Require Import Spaces.Nat.Core Spaces.Card.