Definition homotweqoncomplcomp {X Y Z : UU} (f : X ≃ Y) (g : Y ≃ Z) (x : X) : homot (weqcomp (weqoncompl f x) (weqoncompl g (f x))) (weqoncompl (weqcomp f g) x). Proof. intros. intro x'. induction x' as [ x' nexx' ]. apply (invmaponpathsincl _ (isinclpr1compl Z _) _ _). simpl. apply idpath. Defined.