proposition: Lemma one_type_bicat_laws : prebicat_laws one_type_bicat_data.
proof: 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.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Univalence UniMath.Bicategories.Morphisms.Adjunctions UniMath.Bicategories.Core.EquivToAdjequiv UniMath.Bicategories.Core.AdjointUnique