X Y (f : X -> Y) `{IsEquiv _ _ f} : isepi f. 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.
Require Import Basics. Require Import Types. Require Import TruncType. Require Import ReflectiveSubuniverse. Require Import Colimits.Pushout Truncations.Core HIT.SetCone.