Definition weqcompweql {X Y Z} (f:X ≃ Y) : isweq (λ g:Y ≃ Z, weqcomp f g). Proof. intros. simple refine (isweq_iso _ _ _ _). { intro h. exact (weqcomp (invweq f) h). } { intro g. simpl. rewrite <- weqcompassoc. rewrite weqcompinvl. apply weqcompidl. } { intro h. simpl. rewrite <- weqcompassoc. rewrite weqcompinvr. apply weqcompidl. } Defined.