proposition: Lemma sigma_mor_eq {x y f g} {xxx : sigma_disp_cat x} {yyy : sigma_disp_cat y} {fff : xxx -->[f] yyy} {ggg : xxx -->[g] yyy} {H1 : f = g} {H2} (H3 : pr2 fff = transportb _ (total2_paths_b (s := (_ ,, _)) (s' := (_ ,, _)) H1 H2) (pr2 ggg)) : fff = transportb _ H1 ggg.
proof: Proof. use total2_paths_f. - refine (H2 @ !_). apply pr1_transportf_sigma_disp. - refine (maponpaths _ H3 @ _ @ !(pr2_transportf_sigma_disp _ _)). refine (functtransportf _ _ _ _ @ _). apply transportf_transpose_right. refine (transport_b_f _ _ _ _ @ transport_f_f _ _ _ _ @ _). exact (transportf_set _ _ _ (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