Definition weqcompassoc {X Y Z W} (f:X ≃ Y) (g:Y ≃ Z) (h:Z ≃ W) : weqcomp (weqcomp f g) h = weqcomp f (weqcomp g h). Proof. intros. apply (invmaponpathsincl _ (isinclpr1weq _ _)). apply funextsec; intro x; simpl. apply idpath. Defined.