Definition transportb_total2 {X Y : UU} (Z : X → Y → UU) {x₁ x₂ : X} (p : x₁ = x₂) (yz : ∑ (y : Y), Z x₂ y) : transportb (λ (x : X), ∑ (y : Y), Z x y) p yz = pr1 yz ,, transportb (λ x, Z x (pr1 yz)) p (pr2 yz). Proof. induction p ; cbn. apply idpath. Defined.
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.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence. Section FromIsoTotal. End FromIsoTotal.