Lemma pathsrecomplfxtoy {X Y : UU} (x : X) (y : Y) (isx : isisolated X x) (f : compl X x -> compl Y y) : (recomplf x y isx f x) = y. Proof. intros. unfold recomplf. unfold weqrecompl. unfold invmap. simpl. unfold invrecompl. induction (isx x) as [ i1 | i2 ]. - simpl. apply idpath. - induction (i2 (idpath _)). Defined.