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. 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.
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.