proposition: Lemma inj_sigma_r_refl@{i} (A : Type@{i}) (H : IsHSet A) (P : A -> Type@{i}) x (y : P x) : inj_sigma_r (y:=y) (y':=y) 1 = 1%path.
proof: Proof. unfold inj_sigma_r. intros. simpl. now rewrite is_hset_refl. Defined.
imports: Equations.Init Equations.HoTT.Logic Equations.HoTT.Classes HoTT.Basics.Trunc