proposition: Lemma section_disp_on_eq_morphisms {C : category} (F : section_disp (three_disp C)) {f f' : arrow C} {γ γ': f --> f'} (H00 : arrow_mor00 γ = arrow_mor00 γ') (H11 : arrow_mor11 γ = arrow_mor11 γ') : pr1 (section_disp_on_morphisms F γ) = pr1 (section_disp_on_morphisms F γ').
proof: Proof. assert (Heq : γ = γ'). { use arrow_mor_eq; assumption. } induction Heq. 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