Definition homotrecomplfcomp {X Y Z : UU} (x : X) (y : Y) (z : Z) (isx : isisolated X x) (isy : isisolated Y y) (f : compl X x -> compl Y y) (g : compl Y y -> compl Z z) : homot (funcomp (recomplf x y isx f) (recomplf y z isy g)) (recomplf x z isx (funcomp f g)). Proof. intros. intro x'. unfold recomplf. set (e := homotinvweqweq (weqrecompl Y y isy) (coprodf f (idfun unit) (invmap (weqrecompl X x isx) x'))). simpl in e. simpl. rewrite e. set (e' := homotcoprodfcomp f (idfun unit) g (idfun unit) (invmap (weqrecompl X x isx) x')). simpl in e'. rewrite e'. apply idpath. Defined.