Proposition underlying_vert_two_cat_laws : two_cat_laws underlying_vert_two_cat_category. Proof. repeat split ; cbn. - intros x y v₁ v₂ s. rewrite <- square_assoc_v'. rewrite transportf_f_square. rewrite lunitor_square. unfold transportb_square. rewrite transportf_square_postwhisker. rewrite transportf_f_square. etrans. { apply maponpaths. apply square_assoc_v. } unfold transportb_square. rewrite transportf_f_square. rewrite linvunitor_lunitor_h. unfold transportb_square. rewrite transportf_square_prewhisker. rewrite transportf_f_square. rewrite square_id_left_v. unfold transportb_square. rewrite transportf_f_square. apply transportf_square_id. - intros x y v₁ v₂ s. rewrite <- square_assoc_v'. rewrite transportf_f_square. rewrite lunitor_h_runitor_h. rewrite runitor_square. unfold transportb_square. rewrite transportf_square_postwhisker. rewrite transportf_f_square. etrans. { apply maponpaths. apply square_assoc_v. } unfold transportb_square. rewrite transportf_f_square. rewrite runitor_h_lunitor_h. rewrite linvunitor_lunitor_h. unfold transportb_square. rewrite transportf_square_prewhisker. rewrite transportf_f_square. rewrite square_id_left_v. unfold transportb_square. rewrite transportf_f_square. apply transportf_square_id. - intros x y v₁ v₂ v₃ v₄ s₁ s₂ s₃. apply maponpaths. apply maponpaths_2. apply maponpaths. apply underlying_vert_two_cat_assoc. - intros x y z v₁ v₂. rewrite id_h_square_comp. apply idpath. - intros x y z v₁ v₂. rewrite id_h_square_comp. apply idpath. - intros x y z v w₁ w₂ w₃ s₁ s₂. rewrite transportf_square_postwhisker. rewrite comp_h_square_comp. etrans. { rewrite square_assoc_v. unfold transportb_square. rewrite !transportf_square_prewhisker. rewrite transportf_f_square. rewrite linvunitor_square. rewrite !transportf_square_prewhisker. rewrite transportf_f_square. rewrite <- square_assoc_v'. rewrite transportf_f_square. rewrite <- square_assoc_v'. rewrite transportf_f_square. apply idpath. } rewrite <- square_assoc_v'. rewrite transportf_square_postwhisker. rewrite transportf_f_square. use transportf_square_eq. apply idpath. - intros x y z v w₁ w₂ w₃ s₁ s₂. rewrite transportf_square_prewhisker. rewrite comp_h_square_comp. rewrite <- square_assoc_v'. rewrite transportf_f_square. rewrite <- square_assoc_v'. rewrite transportf_square_postwhisker. rewrite transportf_f_square. rewrite lunitor_square. unfold transportb_square. rewrite !transportf_square_postwhisker. rewrite transportf_f_square. rewrite <- square_assoc_v'. rewrite transportf_f_square. refine (!_). etrans. { apply maponpaths. refine (!_). apply square_assoc_v'. } rewrite transportf_f_square. use transportf_square_eq. apply idpath. - intros x y z v w₁ w₂ w₃ s₁ s₂. rewrite !comp_h_square_comp. etrans. { rewrite <- square_assoc_v'. rewrite transportf_f_square. rewrite <- square_assoc_v'. rewrite transportf_square_postwhisker. rewrite transportf_f_square. rewrite lunitor_square. unfold transportb_square. rewrite !transportf_square_postwhisker. rewrite transportf_f_square. etrans. { do 2 apply maponpaths. apply square_assoc_v. } unfold transportb_square. rewrite !transportf_square_postwhisker. rewrite transportf_f_square. rewrite lunitor_h_runitor_h. rewrite runitor_square. unfold transportb_square. rewrite transportf_square_prewhisker. rewrite transportf_square_postwhisker. rewrite transportf_f_square. rewrite square_assoc_v. unfold transportb_square. rewrite transportf_f_square. etrans. { apply maponpaths. apply maponpaths_2. apply square_assoc_v. } unfold transportb_square. rewrite transportf_square_prewhisker. rewrite transportf_f_square. rewrite runitor_h_lunitor_h. rewrite linvunitor_lunitor_h. unfold transportb_square. rewrite !transportf_square_prewhisker. rewrite transportf_f_square. rewrite square_id_left_v. unfold transportb_square. rewrite !transportf_square_prewhisker. rewrite transportf_f_square. apply idpath. } refine (!_). etrans. { rewrite <- square_assoc_v'. rewrite transportf_f_square. rewrite <- square_assoc_v'. rewrite transportf_square_postwhisker. rewrite transportf_f_square. rewrite lunitor_h_runitor_h. rewrite runitor_square. unfold transportb_square. rewrite !transportf_square_postwhisker. rewrite transportf_f_square. etrans. { do 2 apply maponpaths. apply square_assoc_v. } unfold transportb_square. rewrite !transportf_square_postwhisker. rewrite transportf_f_square. rewrite runitor_h_lunitor_h. rewrite lunitor_square. unfold transportb_square. rewrite transportf_square_prewhisker. rewrite transportf_square_postwhisker. rewrite transportf_f_square. rewrite square_assoc_v. unfold transportb_square. rewrite transportf_f_square. etrans. { apply maponpaths. apply maponpaths_2. apply square_assoc_v. } unfold transportb_square. rewrite transportf_square_prewhisker. rewrite transportf_f_square. rewrite linvunitor_lunitor_h. unfold transportb_square. rewrite !transportf_square_prewhisker. rewrite transportf_f_square. rewrite square_id_left_v. unfold transportb_square. rewrite !transportf_square_prewhisker. rewrite transportf_f_square. apply idpath. } use transportf_square_eq. apply idpath. - intros x y v₁ v₂ s. rewrite !idto2mor_underlying_vert_two_cat. etrans. { rewrite <- square_assoc_v'. rewrite transportf_f_square. rewrite transportf_hcomp_r. rewrite transportf_square_prewhisker. rewrite transportf_square_postwhisker. rewrite !transportf_f_square. rewrite lunitor_h_runitor_h. rewrite runitor_square. unfold transportb_square. rewrite !transportf_square_postwhisker. rewrite !transportf_f_square. rewrite square_assoc_v. unfold transportb_square. rewrite !transportf_f_square. rewrite runitor_h_lunitor_h. rewrite linvunitor_lunitor_h. unfold transportb_square. rewrite !transportf_square_prewhisker. rewrite transportf_f_square. rewrite square_id_left_v. unfold transportb_square. rewrite transportf_f_square. rewrite id_h_square_id. rewrite square_id_left_v. unfold transportb_square. rewrite transportf_f_square. apply idpath. } refine (!_). etrans. { rewrite <- square_assoc_v'. rewrite transportf_f_square. rewrite transportf_hcomp_l. rewrite transportf_square_prewhisker. rewrite transportf_square_postwhisker. rewrite !transportf_f_square. rewrite lunitor_square. unfold transportb_square. rewrite !transportf_square_postwhisker. rewrite !transportf_f_square. rewrite square_assoc_v. unfold transportb_square. rewrite !transportf_f_square. rewrite linvunitor_lunitor_h. unfold transportb_square. rewrite !transportf_square_prewhisker. rewrite transportf_f_square. rewrite square_id_left_v. unfold transportb_square. rewrite transportf_f_square. apply idpath. } use transportf_square_eq. apply idpath. - intros x y v₁ v₂ s. rewrite !idto2mor_underlying_vert_two_cat. etrans. { rewrite <- square_assoc_v'. rewrite transportf_f_square. rewrite transportf_hcomp_r. rewrite transportf_square_prewhisker. rewrite transportf_square_postwhisker. rewrite !transportf_f_square. rewrite lunitor_h_runitor_h. rewrite runitor_square. unfold transportb_square. rewrite !transportf_square_postwhisker. rewrite !transportf_f_square. rewrite square_assoc_v. unfold transportb_square. rewrite !transportf_f_square. rewrite runitor_h_lunitor_h. rewrite linvunitor_lunitor_h. unfold transportb_square. rewrite !transportf_square_prewhisker. rewrite transportf_f_square. rewrite square_id_left_v. unfold transportb_square. rewrite transportf_f_square. rewrite id_h_square_id. rewrite square_id_right_v. unfold transportb_square. rewrite transportf_f_square. apply idpath. } refine (!_). etrans. { rewrite <- square_assoc_v'. rewrite transportf_f_square. rewrite transportf_hcomp_l. rewrite transportf_square_prewhisker. rewrite transportf_square_postwhisker. rewrite !transportf_f_square. rewrite lunitor_square. unfold transportb_square. rewrite !transportf_square_postwhisker. rewrite !transportf_f_square. rewrite square_assoc_v. unfold transportb_square. rewrite !transportf_f_square. rewrite linvunitor_lunitor_h. unfold transportb_square. rewrite !transportf_square_prewhisker. rewrite transportf_f_square. rewrite square_id_left_v. unfold transportb_square. rewrite transportf_f_square. apply idpath. } use transportf_square_eq. apply idpath. - intros x₁ x₂ x₃ x₄ u v w₁ w₂ s. rewrite !idto2mor_underlying_vert_two_cat. etrans. { rewrite <- square_assoc_v'. rewrite transportf_f_square. rewrite transportf_hcomp_r. rewrite transportf_square_prewhisker. rewrite transportf_square_postwhisker. rewrite !transportf_f_square. rewrite lunitor_h_runitor_h. rewrite runitor_square. unfold transportb_square. rewrite !transportf_square_postwhisker. rewrite !transportf_f_square. rewrite square_assoc_v. unfold transportb_square. rewrite !transportf_f_square. rewrite runitor_h_lunitor_h. rewrite linvunitor_lunitor_h. unfold transportb_square. rewrite !transportf_square_prewhisker. rewrite transportf_f_square. rewrite square_id_left_v. unfold transportb_square. rewrite transportf_f_square. apply idpath. } refine (!_). etrans. { rewrite <- square_assoc_v'. rewrite transportf_f_square. rewrite transportf_hcomp_l. rewrite transportf_square_prewhisker. rewrite transportf_square_postwhisker. rewrite !transportf_f_square. rewrite lunitor_square. unfold transportb_square. rewrite !transportf_square_postwhisker. rewrite !transportf_f_square. rewrite square_assoc_v. unfold transportb_square. rewrite !transportf_f_square. rewrite linvunitor_lunitor_h. unfold transportb_square. rewrite !transportf_square_prewhisker. rewrite transportf_f_square. rewrite square_id_left_v. unfold transportb_square. rewrite transportf_f_square. rewrite id_h_square_comp. rewrite <- square_assoc_v'. rewrite transportf_f_square. apply idpath. } use transportf_square_eq. apply idpath. - intros x₁ x₂ x₃ x₄ u v₁ v₂ w s. rewrite !idto2mor_underlying_vert_two_cat. etrans. { rewrite <- square_assoc_v'. rewrite transportf_f_square. rewrite transportf_hcomp_r. rewrite transportf_square_prewhisker. rewrite transportf_square_postwhisker. rewrite !transportf_f_square. rewrite lunitor_h_runitor_h. rewrite runitor_square. unfold transportb_square. rewrite !transportf_square_postwhisker. rewrite !transportf_f_square. rewrite square_assoc_v. unfold transportb_square. rewrite !transportf_f_square. rewrite runitor_h_lunitor_h. rewrite linvunitor_lunitor_h. unfold transportb_square. rewrite !transportf_square_prewhisker. rewrite transportf_f_square. rewrite square_id_left_v. unfold transportb_square. rewrite transportf_f_square. apply idpath. } refine (!_). etrans. { rewrite <- square_assoc_v'. rewrite transportf_f_square. rewrite transportf_hcomp_l. rewrite transportf_square_prewhisker. rewrite transportf_square_postwhisker. rewrite !transportf_f_square. rewrite lunitor_square. unfold transportb_square. rewrite !transportf_square_postwhisker. rewrite !transportf_f_square. rewrite square_assoc_v. unfold transportb_square. rewrite !transportf_f_square. rewrite linvunitor_lunitor_h. unfold transportb_square. rewrite !transportf_square_prewhisker. rewrite transportf_f_square. rewrite square_id_left_v. unfold transportb_square. rewrite transportf_f_square. rewrite <- square_assoc_v'. rewrite transportf_f_square. apply idpath. } use transportf_square_eq. apply idpath. - intros x₁ x₂ x₃ x₄ u₁ u₂ v w s. rewrite !idto2mor_underlying_vert_two_cat. etrans. { rewrite <- square_assoc_v'. rewrite transportf_f_square. rewrite transportf_hcomp_l. rewrite transportf_square_prewhisker. rewrite transportf_square_postwhisker. rewrite !transportf_f_square. rewrite lunitor_square. unfold transportb_square. rewrite !transportf_square_postwhisker. rewrite !transportf_f_square. rewrite square_assoc_v. unfold transportb_square. rewrite !transportf_f_square. rewrite linvunitor_lunitor_h. unfold transportb_square. rewrite !transportf_square_prewhisker. rewrite transportf_f_square. rewrite square_id_left_v. unfold transportb_square. rewrite transportf_f_square. apply idpath. } refine (!_). etrans. { rewrite <- square_assoc_v'. rewrite transportf_f_square. rewrite transportf_hcomp_r. rewrite transportf_square_prewhisker. rewrite transportf_square_postwhisker. rewrite !transportf_f_square. rewrite lunitor_h_runitor_h. rewrite runitor_square. unfold transportb_square. rewrite !transportf_square_postwhisker. rewrite !transportf_f_square. rewrite square_assoc_v. unfold transportb_square. rewrite !transportf_f_square. rewrite runitor_h_lunitor_h. rewrite linvunitor_lunitor_h. unfold transportb_square. rewrite !transportf_square_prewhisker. rewrite transportf_f_square. rewrite square_id_left_v. unfold transportb_square. rewrite transportf_f_square. rewrite id_h_square_comp. rewrite square_assoc_v. unfold transportb_square. rewrite transportf_f_square. apply idpath. } use transportf_square_eq. apply idpath. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Core.Setcategories. Require Import UniMath.CategoryTheory.Core.TwoCategories. Require Import UniMath.CategoryTheory.Monads.Monads. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Strictness. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Examples.Comma. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. Require Import UniMath.Bicategories.DoubleCategories.Basics.DoubleCategoryBasics. Require Import UniMath.Bicategories.DoubleCategories.Core.DoubleCats. Require Import UniMath.Bicategories.DoubleCategories.Core.UnivalentDoubleCats. Require Import UniMath.Bicategories.DoubleCategories.Core.PseudoDoubleSetCats. Require Import UniMath.Bicategories.DoubleCategories.DerivedLaws. Import TransportSquare.