proposition: Lemma section_disp_on_eq_morphisms' {C : category} (F : section_disp (three_disp C)) {f f' : arrow C} {γ : f --> f'} (H : arrow_mor00 γ · f' = f · arrow_mor11 γ) : let alternate := ((arrow_mor00 γ,, arrow_mor11 γ),, H) : f --> f' in pr1 (section_disp_on_morphisms F alternate) = pr1 (section_disp_on_morphisms F γ).
proof: Proof. use section_disp_on_eq_morphisms; reflexivity. Qed.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Constructions UniMath.CategoryTheory.DisplayedCats.Examples.Arrow UniMath.CategoryTheory.DisplayedCats.Examples.Three