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