proposition: Theorem inj_sigma_r@{i} {A : Type@{i}} `{H : IsHSet A} {P : A -> Type@{i}} {x} {y y':P x} : sigmaI P x y = sigmaI P x y' -> y = y'.
proof: Proof. intros [H' H'']%sigma_eq. cbn in *. pose (i := is_hset H' 1). apply (transport (fun h => transport _ h y = y') i H''). Defined.
imports: Equations.Init Equations.HoTT.Logic Equations.HoTT.Classes