{X Y : Type} (f : X -> Y) : isepi f <~> isepi_funext f. Proof. apply equiv_iff_hprop. - intros e ? g0 g1 h. apply equiv_path_arrow. apply e. by apply path_arrow. - intros e ? g0 g1 p. apply path_arrow. apply e. by apply equiv_path_arrow. Defined.
Require Import Basics. Require Import Types. Require Import TruncType. Require Import ReflectiveSubuniverse. Require Import Colimits.Pushout Truncations.Core HIT.SetCone.