Definition invweqcomp {X Y Z} (f:X ≃ Y) (g:Y ≃ Z) : invweq (weqcomp f g) = weqcomp (invweq g) (invweq f). Proof. intros. apply (weqcompinjr (weqcomp f g)). rewrite weqcompinvl. rewrite weqcompassoc. rewrite <- (weqcompassoc (invweq f)). rewrite weqcompinvl. rewrite weqcompidl. rewrite weqcompinvl. apply idpath. Defined.