proposition: Lemma maponpaths_total {A : UU} {B : A -> UU} (x : ∑ y : A, B y) (p0 : pr1 x = pr1 x) (p1 : transportf B p0 (pr2 x) = pr2 x) (q0 : pr1 x = pr1 x) (q1 : transportf B q0 (pr2 x) = pr2 x) : p0=q0 -> (∏ a : A, isaset (B a)) -> total2_paths_f p0 p1 = total2_paths_f q0 q1.
proof: Proof. intro k0. induction k0. intro pfset. apply maponpaths. apply pfset. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.Constructions UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Examples.BicatOfUnivCats UniMath.Bicategories.Core.Invertible_2cells UniMath.Bicategories.DisplayedBicats.DispBicat UniMath.Bicategories.DisplayedBicats.DispUnivalence UniMath.Bicategories.DisplayedBicats.DispInvertibles UniMath.Bicategories.Core.Univalence UniMath.Bicategories.MonoidalCategories.UnivalenceMonCat.CurriedMonoidalCategories