{X Y : Type} (f : X -> Y) {I : IsEmbedding f} {x0 x1 : X} : forall (p : f x0 = f x1), ap f (isinj_embedding f I x0 x1 p) = p. Proof. equiv_intro (equiv_ap_isembedding f x0 x1) q. induction q. cbn. exact (ap _ (isinj_embedding_beta f)). Defined.
Require Import Basics Types Diagrams.CommutativeSquares HSet.