Definition op2_prebicat_data : prebicat_data. Proof. use build_prebicat_data. - exact B. - exact (λ x y, x --> y). - exact (λ x y f g, g ==> f). - exact (λ x, id₁ _). - exact (λ x y z f g, f · g). - exact (λ x y f, id₂ _). - exact (λ x y f g h α β, β • α). - exact (λ x y z f g h α, f ◃ α). - exact (λ x y z g h f α, α ▹ f). - exact (λ x y f, linvunitor f). - exact (λ x y f, lunitor f). - exact (λ x y f, rinvunitor f). - exact (λ x y f, runitor f). - exact (λ w x y z f g h, rassociator f g h). - exact (λ w x y z f g h, lassociator f g h). 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.