proposition: Corollary issurj_isepi_funext {X Y} (f:X->Y) : IsSurjection f -> isepi_funext f.
proof: Proof. intro s. apply equiv_isepi_isepi_funext. by apply issurj_isepi. Defined.
imports: Basics Types TruncType ReflectiveSubuniverse Colimits.Pushout Truncations.Core HIT.SetCone