Definition two_type_bicat_data : prebicat_data. Proof. use build_prebicat_data. - exact X. - exact (λ x y, x = y). - exact (λ _ _ p q, p = q). - exact (fun _ => idpath _). - exact (λ _ _ _ p q, p @ q). - exact (λ _ _ p, idpath p). - exact (λ _ _ _ _ _ q₁ q₂, q₁ @ q₂). - exact (λ _ _ _ p _ _ r, maponpaths (λ s, p @ s) r). - exact (λ _ _ _ _ _ q r, maponpaths (λ s, s @ q) r). - exact (λ _ _ p, idpath p). - exact (λ _ _ p, idpath p). - exact (λ _ _ p, pathscomp0rid p). - exact (λ _ _ p, !(pathscomp0rid p)). - exact (λ _ _ _ _ p q r, path_assoc p q r). - exact (λ _ _ _ _ p q r, !(path_assoc p q r)). Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Core.EquivToAdjequiv. Require Import UniMath.Bicategories.Core.AdjointUnique.