Lemma weqhomot {A B : UU} (f : A -> B) (w : A ≃ B) (H : w ~ f) : isweq f. Proof. apply isweqhomot with w. apply H. apply weqproperty. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.