proposition: Lemma pr2_transportf_sigma_disp {x y : C} {f f' : x --> y} (e : f = f') {xxx : sigma_disp_cat x} {yyy} (fff : xxx -->[f] yyy) : pr2 (transportf _ e fff) = transportf (λ ff, pr2 xxx -->[ff] _ ) (two_arg_paths_f e (! pr1_transportf_sigma_disp e fff)) (pr2 fff).
proof: Proof. destruct e. apply pathsinv0. etrans. apply maponpaths_2, maponpaths, maponpaths. apply (homsets_disp _ _ _ _ _ _ (idpath _)). apply idpath. 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