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