proposition: 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: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Equivalences.Core UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Graphs.Limits UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.Isos UniMath.CategoryTheory.DisplayedCats.Univalence UniMath.CategoryTheory.DisplayedCats.Limits