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. intro k0. induction k0. intro pfset. apply maponpaths. apply pfset. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions. Require Import UniMath.Bicategories.Core.Bicat. Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Require Import UniMath.Bicategories.DisplayedBicats.DispUnivalence. Require Import UniMath.Bicategories.DisplayedBicats.DispInvertibles. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.MonoidalCategories.UnivalenceMonCat.CurriedMonoidalCategories. Import TensorNotation. Import TensorNotation.