Definition section_disp_on_morphisms (F : section_disp_data) {x y : C} (f : x --> y) := pr2 F _ _ f : F x -->[f] F y.
Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.DisplayedCats.Core.