Lemma isweql3 {X Y : UU} (f : X -> Y) (g : Y -> X) (egf : ∏ x : X, g (f x) = x) : isweq f -> isweq g. Proof. intros w. assert (int1 : isweq (g ∘ f)). { apply (isweqhomot (idfun X) (g ∘ f) (λ (x : X), ! (egf x))). apply idisweq. } apply (twooutof3b f g w int1). Defined.