Definition homotrecomplfidfun {X : UU} (x : X) (isx : isisolated X x) : homot (recomplf x x isx (idfun (compl X x))) (idfun _). Proof. intros. intro x'. unfold recomplf. unfold weqrecompl. unfold invmap. simpl. unfold invrecompl. induction (isx x') as [ e | ne ]. - simpl. apply e. - simpl. apply idpath. Defined.