Definition homotrecomplfhomot {X Y : UU} (x : X) (y : Y) (isx : isisolated X x) (f f' : compl X x -> compl Y y) (h : homot f f') : homot (recomplf x y isx f) (recomplf x y isx f'). Proof. intros. intro a. unfold recomplf. apply (maponpaths (recompl Y y) (homotcoprodfhomot _ _ _ _ h (λ t : unit, idpath t) (invmap (weqrecompl X x isx) a))). Defined.