Lemma univalence_pathsinv0 {A B : UU} (p : A = B) : univalence _ _ (!p) = invweq (univalence _ _ p). Proof. apply eqweqmap_pathsinv0. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Univalence.