Lemma cat_prebicat_laws : prebicat_laws cat_prebicat_data. Proof. repeat split; cbn. - intros C D F G η. apply nat_trans_eq; try apply homset_property. intros ; cbn. apply id_left. - intros C D F G η. apply nat_trans_eq; try apply homset_property. intros ; cbn. apply id_right. - intros C D F₁ F₂ F₃ F₄ α β γ. apply nat_trans_eq; try apply homset_property. intros ; cbn. apply assoc. - intros C₁ C₂ C₃ F G. apply nat_trans_eq; try apply homset_property. intro; apply idpath. - intros C₁ C₂ C₃ F G. apply nat_trans_eq; try apply homset_property. intros ; cbn. apply functor_id. - intros C₁ C₂ C₃ F G₁ G₂ G₃ α β. apply nat_trans_eq; try apply homset_property. intros; apply idpath. - intros C₁ C₂ C₃ F₁ F₂ F₃ G α β. apply nat_trans_eq; try apply homset_property. intros ; cbn. exact (!(functor_comp G _ _)). - intros C D F G α. apply nat_trans_eq; try apply homset_property. intros ; cbn. rewrite id_left, id_right. apply idpath. - intros C D F G α. apply nat_trans_eq; try apply homset_property. intros ; cbn. rewrite id_left, id_right. apply idpath. - intros C₁ C₂ C₃ C₄ F G H₁ H₂ α. apply nat_trans_eq; try apply homset_property. intros ; cbn. rewrite id_left, id_right. apply idpath. - intros C₁ C₂ C₃ C₄ F G₁ G₂ H α. apply nat_trans_eq; try apply homset_property. intros ; cbn. rewrite id_left, id_right. apply idpath. - intros C₁ C₂ C₃ C₄ F₁ F₂ G H α. apply nat_trans_eq; try apply homset_property. intros ; cbn. rewrite id_left, id_right. apply idpath. - intros C₁ C₂ C₃ F₁ F₂ G₁ H₂ α β. apply nat_trans_eq; try apply homset_property. intros ; cbn. exact ((nat_trans_ax β _ _ _)). - intros C D F. apply nat_trans_eq; try apply homset_property. intros ; cbn. apply id_left. - intros C D F. apply nat_trans_eq; try apply homset_property. intros ; cbn. apply id_left. - intros C D F. apply nat_trans_eq; try apply homset_property. intros ; cbn. apply id_left. - intros C D F. apply nat_trans_eq; try apply homset_property. intros ; cbn. apply id_left. - intros C₁ C₂ C₃ C₄ F₁ F₂ F₃. apply nat_trans_eq; try apply homset_property. intros ; cbn. apply id_left. - intros C₁ C₂ C₃ C₄ F₁ F₂ F₃. apply nat_trans_eq; try apply homset_property. intros ; cbn. apply id_left. - intros C₁ C₂ C₃ F G. apply nat_trans_eq; try apply homset_property. intros ; cbn. exact (id_left _ @ functor_id G _). - intros C₁ C₂ C₃ C₄ C₅ F₁ F₂ F₃ F₄. apply nat_trans_eq; try apply homset_property. intros ; cbn. rewrite !id_left. exact (functor_id F₄ _). Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.catiso. Require Import UniMath.CategoryTheory.CategoryEquality. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.EquivToAdjequiv. Require Import UniMath.Bicategories.Core.AdjointUnique. Require Import UniMath.Bicategories.Core.Univalence.