Definition disp_cat_id_comp_eq (pob : ∏ (x : C), D₁ x = D₂ x) (pmor : ∏ (x y : C) (xx : D₁ x) (yy : D₁ y) (f : x --> y), xx -->[ f ] yy = eqweqmap (pob x) xx -->[ f ] eqweqmap (pob y) yy) : UU := (∏ (x : C) (xx : D₁ x), eqweqmap (pmor x x xx xx (identity x)) (id_disp xx) = id_disp (eqweqmap (pob x) xx)) × (∏ (x y z : C) (f : x --> y) (g : y --> z) (xx : D₁ x) (yy : D₁ y) (zz : D₁ z) (ff : xx -->[ f ] yy) (gg : yy -->[ g ] zz), eqweqmap (pmor _ _ _ _ _) (ff ;; gg) = eqweqmap (pmor _ _ _ _ f) ff ;; eqweqmap (pmor _ _ _ _ g) gg).
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.NaturalTransformations. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Equivalences. Require Import UniMath.CategoryTheory.DisplayedCats.DisplayedFunctorEq. Require Import UniMath.CategoryTheory.DisplayedCats.EquivalenceOverId.