Definition one_type_bicat_data : prebicat_data. Proof. use build_prebicat_data. - exact one_type. - exact (λ X Y, X → Y). - exact (λ _ _ f g, f ~ g). - exact (λ _ x, x). - exact (λ _ _ _ f g x, g(f x)). - intros. exact (homotrefl _). - cbn ; intros X Y f g h p q. exact (homotcomp p q). - cbn ; intros X Y Z f g h p. exact (funhomotsec f p). - cbn ; intros X Y Z f g h p. exact (homotfun p h). - intros ; intro. apply idpath. - intros ; intro. apply idpath. - intros ; intro. apply idpath. - intros ; intro. apply idpath. - intros ; intro. apply idpath. - intros ; intro. apply idpath. 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.