Lemma E_mor_eq {x y xx yy} {xxx : E (x ,, xx)} {yyy : E (y ,, yy)} (xxx' := (xx ,, xxx) : sigma_disp_cat _) (yyy' := (yy ,, yyy) : sigma_disp_cat _) (f : z_iso x y) (g := inv_from_z_iso f) {ff gg fff ggg} {H1 : compose (C := total_category D) (a := (_ ,, _)) (b := (_ ,, _)) (c := (_ ,, _)) (z_iso_mor f ,, ff) (g ,, gg) = identity _} (H2 : comp_disp (D := sigma_disp_cat) (xx := (xx ,, xxx)) (yy := (yy ,, yyy)) (zz := (xx ,, xxx)) (ff ,, fff) (gg ,, ggg) = transportb _ (z_iso_inv_after_z_iso f) (id_disp _)) : fff ;; ggg = transportb _ H1 (id_disp _). Proof. induction (total2_paths_equiv _ _ _ H2) as [H3 H4]. refine (transportb_transpose_right (e := H3) H4 @ _). unfold transportb. simpl. apply transportf_transpose_right. rewrite pr2_transportf_sigma_disp, (functtransportf _ _ (two_arg_paths_f _ _)), (functtransportf _ _ (!H3)), transport_b_f, transport_f_f. apply transportf_set. apply (homset_property (total_category _)). Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Limits.