Definition op1_prebicat_data (C : prebicat_data) : prebicat_data. Proof. exists (op1_prebicat_1_id_comp_cells C). red. cbn. unfold op1_2cell_struct. repeat use make_dirprod; intros *. - apply id2. - apply runitor. - apply lunitor. - apply rinvunitor. - apply linvunitor. - apply lassociator. - apply rassociator. - intros α β. exact ( α • β ). - intros α. exact (α ▹ f). - intros α. exact (g ◃ α). 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.opp_precat. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Morphisms.Adjunctions.