Definition disp_struct_ob_mor : disp_cat_ob_mor C. Proof. exists P. intros ? ? f a b; exact (H f a b ). Defined.
Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.DisplayedCats.Core.