Definition cod_disp_ob_mor : disp_cat_ob_mor C. Proof. exists (λ x : C, ∑ y, y --> x). simpl; intros x y xx yy f. exact (∑ ff : pr1 xx --> pr1 yy, ff · pr2 yy = pr2 xx · f). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations.