Definition strict_identitor_disp_cat_data : disp_cat_ob_mor (map1cells C D). Proof. use tpair. - exact (λ F, ∏ (X : C), id₁ (Fobj F X) = Fmor F (id₁ X)). - exact (λ F G Fid Gid η, ∏ (X : C), (ηobj η X ◃ idtoiso_2_1 _ _ (Gid X)) • ηmor η (id₁ X) = (runitor (ηobj η X)) • linvunitor (ηobj η X) • (idtoiso_2_1 _ _ (Fid X) ▹ ηobj η X)). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.PseudoFunctors.Display.Base. Require Import UniMath.Bicategories.PseudoFunctors.Display.Map1Cells. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.DisplayedBicats.Examples.DisplayedCatToBicat. Require Import UniMath.Bicategories.DisplayedBicats.DispUnivalence.