Lemma one_type_bicat_laws : prebicat_laws one_type_bicat_data. Proof. repeat (use tpair). - intros X Y f g p ; cbn in *. apply idpath. - intros X Y f g p ; cbn in *. unfold homotcomp, homotrefl. apply funextsec. intro x. apply pathscomp0rid. - intros X Y f g h k p q r. apply funextsec. intro x. apply path_assoc. - intros; apply idpath. - intros; apply idpath. - intros X Y Z f g h i p q ; cbn in *. apply funextsec. intro x. apply idpath. - intros X Y Z f g h i p q ; cbn in *. apply funextsec. intro x. unfold homotcomp, homotfun. simpl. apply (! maponpathscomp0 _ _ _). - intros X Y f g p ; cbn in *. apply funextsec. intro x. unfold homotcomp, homotfun. simpl. apply pathscomp0rid. - intros X Y f g p ; cbn in *. apply funextsec. intro x. unfold homotcomp, homotfun. simpl. etrans. { apply pathscomp0rid. } apply maponpathsidfun. - intros W X Y Z f g h i p ; cbn in *. apply funextsec. intro x. unfold homotcomp, funhomotsec. simpl. apply pathscomp0rid. - intros W X Y Z f g h i p ; cbn in *. apply funextsec. intro x. apply pathscomp0rid. - intros W X Y Z f g h i p ; cbn in *. apply funextsec. intro x. unfold homotcomp, homotfun. simpl. etrans. { apply maponpathscomp. } apply (! pathscomp0rid _). - intros X Y Z f g h i p q ; cbn in *. apply funextsec. intro x. unfold homotcomp, homotfun, funhomotsec. induction (p x). apply (! pathscomp0rid _). - intros; apply idpath. - intros; apply idpath. - intros; apply idpath. - intros; apply idpath. - intros; apply idpath. - intros; apply idpath. - intros; apply idpath. - intros V W X Y Z f g h i ; cbn in *. apply idpath. Qed.
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.