Definition weqcomp_assoc {W X Y Z : UU} (f : W ≃ X) (g: X ≃ Y) (h : Y ≃ Z) : (h ∘ (g ∘ f) = (h ∘ g) ∘ f)%weq. Proof. intros. apply subtypePath. - intros p. apply isapropisweq. - simpl. apply idpath. Defined.