{X Y : Type} (f : X -> Y) {I : IsEmbedding f} {x : X} : (isinj_embedding f I x x idpath) = idpath. Proof. exact (ap (ap pr1) (contr (idpath : (x;idpath) = (x;idpath)))). Defined.
Require Import Basics. Require Import Types.Sigma Types.Paths Types.Unit Types.Arrow.