proposition: Lemma isepi_isequiv X Y (f : X -> Y) `{IsEquiv _ _ f} : isepi f.
proof: Proof. intros ? g h H'. apply ap10 in H'. apply path_forall. intro x. transitivity (g (f (f^-1 x))). - by rewrite eisretr. - transitivity (h (f (f^-1 x))). * apply H'. * by rewrite eisretr. Qed.
imports: Basics Types TruncType ReflectiveSubuniverse Colimits.Pushout Truncations.Core HIT.SetCone