proposition: Theorem inj_sigma_r@{i} {A : Type@{i}} `{H : HSet 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 (is_hset H' id_refl). apply (transport (P:=fun h => transport h y = y') i H''). Defined.
imports: Equations.Init Equations.Type.Logic Equations.Type.Classes