Proposition double_coalg_hor_eq {X Y : double_coalg F} (h k : double_coalg_hor X Y) : h = k ≃ ∑ (s : globular_iso_square h k), is_double_coalg_sqr (sqr_of_double_coalg_hor h) (sqr_of_double_coalg_hor k) (identity _) (identity _) s. Proof. simple refine (weqtotal2 _ _ ∘ total2_paths_equiv _ _ _)%weq. - exact (make_weq _ (is_univalent_twosided_disp_cat_hor_mor C _ _ _ _ (idpath _) (idpath _) h k)). - intro p. induction h as [ h Hh ]. induction k as [ k Hk ]. cbn ; cbn in p. induction p ; cbn. use weqimplimpl. + abstract (intro p ; induction p ; cbn ; etrans ; [ do 2 apply maponpaths ; apply lax_double_functor_id_square | ] ; unfold transportb_square ; rewrite transportf_square_postwhisker ; rewrite transportf_f_square ; rewrite square_id_right_v ; refine (_ @ !(square_id_left_v _)) ; unfold transportb_square ; rewrite transportf_f_square ; use transportf_square_eq ; apply idpath). + abstract (intro p ; pose proof (p @ square_id_left_v _) as p' ; clear p ; pose proof (maponpaths (λ z, transportf_square _ _ (_ ⋆v z)) (!(lax_double_functor_id_square _ _)) @ p') as p'' ; clear p' ; unfold transportb_square in p'' ; rewrite transportf_square_postwhisker in p'' ; rewrite transportf_f_square in p'' ; rewrite square_id_right_v in p'' ; unfold transportb_square in p'' ; rewrite transportf_f_square in p'' ; refine (!_ @ maponpaths (transportf_square (id_left _) (id_left _)) p'' @ _) ; unfold transportb_square ; rewrite transportf_f_square ; apply transportf_square_id). + abstract (apply isaset_square). + abstract (apply isaset_square). Defined.
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.