Proposition two_cat_laws_strict_underlying_vertical_two_cat_category : two_cat_laws strict_underlying_vertical_two_cat_category. Proof. repeat split ; cbn -[transportf_s_square]. - intros x y v₁ v₂ s. rewrite strict_square_id_left. rewrite transportfb_s_square. apply idpath. - intros x y v₁ v₂ s. rewrite strict_square_id_right. rewrite transportfb_s_square. apply idpath. - intros x y v₁ v₂ v₃ v₄ s₁ s₂ s₃. rewrite transportf_s_square_post_whisker_h. rewrite transportf_s_square_pre_whisker_h. rewrite !transportf_f_s_square. rewrite strict_square_assoc. unfold transportb_s_square. rewrite transportf_f_s_square. use transportf_s_square_eq. apply idpath. - intros x y z v₁ v₂. rewrite s_id_h_square_comp. apply idpath. - intros x y z v₁ v₂. rewrite s_id_h_square_comp. apply idpath. - intros x y z v w₁ w₂ w₄ s₁ s₂. rewrite comp_h_square_comp. rewrite strict_square_id_left. unfold transportb_s_square. refine (!_). exact (transportf_s_square_post_whisker_v' _ _ _ _ _ _ _). - intros x y z v₁ v₂ v₃ w s₁ s₂. rewrite comp_h_square_comp. rewrite strict_square_id_left. unfold transportb_s_square. rewrite (transportf_s_square_pre_whisker_v' _ _ _ _ (s_id_h_left (s_identity_h z))). apply idpath. - intros x y z v₁ v₂ w₁ w₂ s₁ s₂. rewrite !comp_h_square_comp. rewrite !strict_square_id_left. rewrite !strict_square_id_right. use transportf_s_square_eq. assert (s_id_h_left (s_identity_h x) = s_id_h_right (s_identity_h x)) as r. { apply isaset_hor_mor_strict_double_cat. } rewrite r ; clear r. assert (s_id_h_left (s_identity_h y) = s_id_h_right (s_identity_h y)) as r. { apply isaset_hor_mor_strict_double_cat. } rewrite r ; clear r. apply maponpaths. use transportf_s_square_eq. apply idpath. - intros x y v₁ v₂ s. rewrite !vertical_two_cat_category_idto2mor. etrans. { apply maponpaths. exact (transportf_s_square_post_whisker_h' _ _ _ _ _ _ (s_id_v_left _) _ _). } rewrite strict_square_id_right. rewrite s_id_h_square_id. rewrite s_square_id_left_v. refine (!_). etrans. { apply maponpaths. exact (transportf_s_square_pre_whisker_h' _ _ _ _ (idpath _) _ _ _ _). } rewrite strict_square_id_left. unfold transportb_s_square. rewrite !transportf_f_s_square. use transportf_s_square_eq. apply idpath. - intros x y v₁ v₂ s. rewrite !vertical_two_cat_category_idto2mor. etrans. { apply maponpaths. exact (transportf_s_square_post_whisker_h' _ _ _ _ _ _ (s_id_v_right _) _ _). } rewrite strict_square_id_right. rewrite s_id_h_square_id. rewrite s_square_id_right_v. refine (!_). etrans. { apply maponpaths. exact (transportf_s_square_pre_whisker_h' _ _ _ _ (idpath _) _ _ _ _). } rewrite strict_square_id_left. unfold transportb_s_square. rewrite !transportf_f_s_square. use transportf_s_square_eq. apply idpath. - intros x₁ x₂ x₃ x₄ u v w₁ w₂ s. rewrite !vertical_two_cat_category_idto2mor. etrans. { apply maponpaths. exact (transportf_s_square_post_whisker_h' _ _ _ _ _ _ (s_assocl_v _ _ _) _ _). } rewrite strict_square_id_right. rewrite s_square_assoc_v. refine (!_). etrans. { apply maponpaths. exact (transportf_s_square_pre_whisker_h' _ _ _ _ (idpath _) _ _ _ _). } rewrite strict_square_id_left. rewrite s_id_h_square_comp. unfold transportb_s_square. rewrite !transportf_f_s_square. use transportf_s_square_eq. apply idpath. - intros x₁ x₂ x₃ x₄ u v₁ v₂ w s. rewrite !vertical_two_cat_category_idto2mor. etrans. { apply maponpaths. exact (transportf_s_square_post_whisker_h' _ _ _ _ _ _ (s_assocl_v _ _ _) _ _). } rewrite strict_square_id_right. rewrite s_square_assoc_v. refine (!_). etrans. { apply maponpaths. exact (transportf_s_square_pre_whisker_h' _ _ _ _ (idpath _) _ _ _ _). } rewrite strict_square_id_left. unfold transportb_s_square. rewrite !transportf_f_s_square. use transportf_s_square_eq. apply idpath. - intros x₁ x₂ x₃ x₄ u₁ u₂ v w s. rewrite !vertical_two_cat_category_idto2mor. refine (!_). etrans. { apply maponpaths. exact (transportf_s_square_post_whisker_h' _ _ _ _ _ _ (s_assocl_v _ _ _) _ _). } rewrite strict_square_id_right. refine (!_). etrans. { apply maponpaths. exact (transportf_s_square_pre_whisker_h' _ _ _ _ (idpath _) _ _ _ _). } rewrite strict_square_id_left. rewrite s_id_h_square_comp. rewrite s_square_assoc_v. unfold transportb_s_square. rewrite !transportf_f_s_square. use transportf_s_square_eq. apply idpath. 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.TwoCategories. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Strictness. Require Import UniMath.Bicategories.DoubleCategories.Basics.DoubleCategoryBasics. Require Import UniMath.Bicategories.DoubleCategories.Basics.StrictDoubleCatBasics. Require Import UniMath.Bicategories.DoubleCategories.Core.StrictDoubleCats.