Proposition double_coalg_comp_hor_is_sqr {X₁ X₂ Y₁ Y₂ Z₁ Z₂ : double_coalg F} {v₁ : double_coalg_ver X₁ X₂} {v₂ : double_coalg_ver Y₁ Y₂} {v₃ : double_coalg_ver Z₁ Z₂} {h₁ : double_coalg_hor X₁ Y₁} {h₂ : double_coalg_hor Y₁ Z₁} {k₁ : double_coalg_hor X₂ Y₂} {k₂ : double_coalg_hor Y₂ Z₂} (s₁ : double_coalg_sqr v₁ v₂ h₁ k₁) (s₂ : double_coalg_sqr v₂ v₃ h₂ k₂) : is_double_coalg_sqr (double_coalg_comp_hor_struct h₁ h₂) (double_coalg_comp_hor_struct k₁ k₂) _ _ (s₁ ⋆h s₂). Proof. cbn. rewrite transportf_square_prewhisker. rewrite transportf_square_postwhisker. rewrite transportf_f_square. etrans. { apply maponpaths. refine (!_). apply (square_assoc_v' (C := C)). } rewrite transportf_f_square. etrans. { do 2 apply maponpaths. exact (lax_double_functor_comp_h_mor' F s₁ s₂). } 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. rewrite <- comp_h_square_comp. etrans. { apply maponpaths_2. apply eq_of_double_coalg_sqr'. } apply maponpaths. apply eq_of_double_coalg_sqr'. } unfold transportb_square. rewrite transportf_hcomp_l. rewrite transportf_square_prewhisker. rewrite !transportf_f_square. rewrite pathsinv0r. rewrite transportf_hcomp_r. rewrite transportf_square_prewhisker. rewrite transportf_f_square. cbn. refine (!_). etrans. { apply maponpaths. apply (square_assoc_v (C := C)). } unfold transportb_square. rewrite transportf_f_square. rewrite <- comp_h_square_comp. apply transportf_square_eq. apply idpath. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.FunctorCoalgebras. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.DisplayedFunctor. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Total. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Examples.DispCatOnTwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Examples.TwoSidedDispCatOnDispCat. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.DoubleCategories.Basics.DoubleCategoryBasics. Require Import UniMath.Bicategories.DoubleCategories.Core.DoubleFunctor. Require Import UniMath.Bicategories.DoubleCategories.Core.DoubleCats. Require Import UniMath.Bicategories.DoubleCategories.Core.UnivalentDoubleCats. Require Import UniMath.Bicategories.DoubleCategories.DerivedLaws. Import TransportSquare.