proposition: Lemma injective_proj1 {Z} (r : Z -> HProp) : IsInjective (@proj1 Z r).
proof: Proof. intros [p Hp] [q Hq]; cbn. intros ->. unshelve eapply path_sigma; cbn. - reflexivity. - cbn. apply path_ishprop. Qed.
imports: HoTT(TruncType abstract_algebra) HoTT(PropResizing.PropResizing) HoTT(Spaces.Nat.Core Spaces.Card)