Definition cod_id_comp : disp_cat_id_comp _ cod_disp_ob_mor. Proof. split. - simpl; intros. exists (identity _ ). abstract ( etrans; [apply id_left |]; apply pathsinv0, id_right ). - simpl; intros x y z f g xx yy zz ff gg. exists (pr1 ff · pr1 gg). abstract ( apply pathsinv0; etrans; [apply assoc |]; etrans; [apply maponpaths_2, (! (pr2 ff)) |]; etrans; [eapply pathsinv0, assoc |]; etrans; [apply maponpaths, (! (pr2 gg))|]; apply assoc). 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.