Lemma pathsinv0_weqtopaths {A B : UU} (eq : A ≃ B) : ! (weqtopaths eq) = weqtopaths (invweq eq). Proof. type_induction eq e. symmetry. refine (maponpaths _ (! univalence_pathsinv0 e) @ _). refine (homotinvweqweq _ _ @ _). refine (maponpaths _ (! homotinvweqweq _ _)). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Univalence.