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