Lemma ishomotinclrecomplf {X Y : UU} (x : X) (y : Y) (isx : isisolated X x) (f : compl X x -> compl Y y) (x'n : compl X x) (y'n : compl Y y) (e : paths (recomplf x y isx f (pr1 x'n)) (pr1 y'n)) : (f x'n) = y'n. Proof. intros. induction x'n as [ x' nexx' ]. induction y'n as [ y' neyy' ]. simpl in e . apply (invmaponpathsincl _ (isinclpr1compl _ _)). simpl. rewrite (pathsinv0 e). unfold recomplf. unfold invmap. unfold coprodf. simpl. unfold invrecompl. induction (isx x') as [ exx' | nexx'' ]. - induction (nexx' exx'). - simpl. assert (ee : nexx' = nexx''). apply (proofirrelevance _ (isapropneg _)). rewrite ee. apply idpath. Defined.