Definition total_prebicat_2_id_comp_struct : prebicat_2_id_comp_struct total_prebicat_1_id_comp_cells. Proof. repeat split; cbn; unfold total_prebicat_cell_struct. - intros. exists (id2 _). exact (disp_id2 _). - intros. exists (lunitor _). exact (disp_lunitor _). - intros. exists (runitor _). exact (disp_runitor _). - intros. exists (linvunitor _). exact (disp_linvunitor _). - intros. exists (rinvunitor _). exact (disp_rinvunitor _). - intros. exists (rassociator _ _ _). exact (disp_rassociator _ _ _). - intros. exists (lassociator _ _ _). exact (disp_lassociator _ _ _). - intros a b f g h r s. exists (pr1 r • pr1 s). exact (pr2 r •• pr2 s). - intros a b d f g1 g2 r. exists (pr1 f ◃ pr1 r). exact (pr2 f ◃◃ pr2 r). - intros a b c f1 f2 g r. exists (pr1 r ▹ pr1 g). exact (pr2 r ▹▹ pr2 g). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Core.Univalence.