Lemma strict_cat_prebicat_laws : prebicat_laws strict_cat_prebicat_data. Proof. repeat split; cbn. - intros C D F G η. apply nat_trans_eq; try apply D. intros ; cbn. apply id_left. - intros C D F G η. apply nat_trans_eq; try apply D. intros ; cbn. apply id_right. - intros C D F₁ F₂ F₃ F₄ α β γ. apply nat_trans_eq; try apply D. intros ; cbn. apply assoc. - intros C₁ C₂ C₃ F G. apply nat_trans_eq; try apply C₃. intros; apply idpath. - intros C₁ C₂ C₃ F G. apply nat_trans_eq; try apply C₃. intros ; cbn. apply functor_id. - intros C₁ C₂ C₃ F G₁ G₂ G₃ α β. apply nat_trans_eq; try apply C₃. intros; apply idpath. - intros C₁ C₂ C₃ F₁ F₂ F₃ G α β. apply nat_trans_eq; try apply C₃. intros ; cbn. exact (!(functor_comp G _ _)). - intros C D F G α. apply nat_trans_eq; try apply D. intros ; cbn. rewrite id_left, id_right. apply idpath. - intros C D F G α. apply nat_trans_eq; try apply D. intros ; cbn. rewrite id_left, id_right. apply idpath. - intros C₁ C₂ C₃ C₄ F G H₁ H₂ α. apply nat_trans_eq; try apply C₄. intros ; cbn. rewrite id_left, id_right. apply idpath. - intros C₁ C₂ C₃ C₄ F G₁ G₂ H α. apply nat_trans_eq; try apply C₄. intros ; cbn. rewrite id_left, id_right. apply idpath. - intros C₁ C₂ C₃ C₄ F₁ F₂ G H α. apply nat_trans_eq; try apply C₄. intros ; cbn. rewrite id_left, id_right. apply idpath. - intros C₁ C₂ C₃ F₁ F₂ G₁ H₂ α β. apply nat_trans_eq; try apply C₃. intros ; cbn. exact ((nat_trans_ax β _ _ _)). - intros C D F. apply nat_trans_eq; try apply D. intros ; cbn. apply id_left. - intros C D F. apply nat_trans_eq; try apply D. intros ; cbn. apply id_left. - intros C D F. apply nat_trans_eq; try apply D. intros ; cbn. apply id_left. - intros C D F. apply nat_trans_eq; try apply D. intros ; cbn. apply id_left. - intros C₁ C₂ C₃ C₄ F₁ F₂ F₃. apply nat_trans_eq; try apply C₄. intros ; cbn. apply id_left. - intros C₁ C₂ C₃ C₄ F₁ F₂ F₃. apply nat_trans_eq; try apply C₄. intros ; cbn. apply id_left. - intros C₁ C₂ C₃ F G. apply nat_trans_eq; try apply C₃. intros ; cbn. exact (id_left _ @ functor_id G _). - intros C₁ C₂ C₃ C₄ C₅ F₁ F₂ F₃ F₄. apply nat_trans_eq; try apply C₅. 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.Setcategories. 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.EquivToAdjequiv. Require Import UniMath.Bicategories.Core.AdjointUnique. Require Import UniMath.Bicategories.Core.Strictness. Require Import UniMath.Bicategories.Core.Univalence.