proposition: Lemma pr1_section_disp_on_morphisms_comp {C : category} (F : section_disp (three_disp C)) {f f' f'' : arrow C} (γ : f --> f') (γ' : f' --> f'') : pr1 (section_disp_on_morphisms F γ) · pr1 (section_disp_on_morphisms F γ') = pr1 (section_disp_on_morphisms F (γ · γ')).
proof: Proof. apply pathsinv0. etrans. apply maponpaths. apply (section_disp_comp F). 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