proposition: Proposition structured_cospans_double_cat_functor_associator : double_functor_associator (structured_cospans_double_cat_associator PX₁ L₁) (structured_cospans_double_cat_associator PX₂ L₂) structured_cospans_double_cat_functor_comp.
proof: Proof. intro ; intros. use struct_cospan_sqr_eq. rewrite transportf_disp_mor2_struct_cospan ; cbn. use (MorphismsOutofPushoutEqual (isPushout_Pushout (PX₂ _ _ _ _ _))) ; cbn. - refine (assoc _ _ _ @ _). etrans. { apply maponpaths_2. refine (assoc _ _ _ @ _). apply maponpaths_2. apply PushoutArrow_PushoutIn1. } do 2 refine (assoc' _ _ _ @ _). etrans. { apply maponpaths. refine (assoc _ _ _ @ _). apply maponpaths_2. apply PushoutArrow_PushoutIn1. } refine (assoc _ _ _ @ _). etrans. { apply maponpaths_2. refine (assoc _ _ _ @ _). apply maponpaths_2. apply PushoutArrow_PushoutIn1. } refine (assoc' _ _ _ @ _). etrans. { apply maponpaths. apply PushoutArrow_PushoutIn1. } refine (!_). refine (assoc _ _ _ @ _). etrans. { apply maponpaths_2. refine (assoc _ _ _ @ _). apply maponpaths_2. apply PushoutArrow_PushoutIn1. } do 2 refine (assoc' _ _ _ @ _). etrans. { apply maponpaths. refine (assoc _ _ _ @ _). apply maponpaths_2. apply PushoutArrow_PushoutIn1. } etrans. { apply maponpaths. refine (!(functor_comp _ _ _) @ _). apply maponpaths. apply PushoutArrow_PushoutIn1. } refine (_ @ functor_comp _ _ _). refine (_ @ id_left _). apply maponpaths_2 ; cbn. apply idpath. - refine (assoc _ _ _ @ _). etrans. { apply maponpaths_2. refine (assoc _ _ _ @ _). apply maponpaths_2. apply PushoutArrow_PushoutIn2. } refine (!_). refine (assoc _ _ _ @ _). etrans. { apply maponpaths_2. refine (assoc _ _ _ @ _). apply maponpaths_2. apply PushoutArrow_PushoutIn2. } use (MorphismsOutofPushoutEqual (isPushout_Pushout (PX₂ _ _ _ _ _))) ; cbn. + refine (assoc _ _ _ @ _). etrans. { apply maponpaths_2. refine (assoc _ _ _ @ _). apply maponpaths_2. refine (assoc _ _ _ @ _). apply maponpaths_2. apply PushoutArrow_PushoutIn1. } do 2 refine (assoc' _ _ _ @ _). etrans. { apply maponpaths. refine (assoc _ _ _ @ _). apply maponpaths_2. apply PushoutArrow_PushoutIn2. } etrans. { apply maponpaths. refine (!(functor_comp _ _ _) @ _). apply maponpaths. apply PushoutArrow_PushoutIn2. } etrans. { refine (!(functor_comp _ _ _) @ _). apply maponpaths. apply PushoutArrow_PushoutIn1. } refine (!_). refine (assoc _ _ _ @ _). etrans. { apply maponpaths_2. refine (assoc _ _ _ @ _). apply maponpaths_2. apply PushoutArrow_PushoutIn1. } do 2 refine (assoc' _ _ _ @ _). etrans. { apply maponpaths. refine (assoc _ _ _ @ _). apply maponpaths_2. apply PushoutArrow_PushoutIn1. } refine (assoc _ _ _ @ _). etrans. { apply maponpaths_2. refine (assoc _ _ _ @ _). apply maponpaths_2. apply PushoutArrow_PushoutIn2. } refine (assoc' _ _ _ @ _). etrans. { apply maponpaths. apply PushoutArrow_PushoutIn1. } exact (!(functor_comp _ _ _)). + refine (assoc _ _ _ @ _). etrans. { apply maponpaths_2. refine (assoc _ _ _ @ _). apply maponpaths_2. refine (assoc _ _ _ @ _). apply maponpaths_2. apply PushoutArrow_PushoutIn2. } do 2 refine (assoc' _ _ _ @ _). etrans. { apply maponpaths. refine (assoc _ _ _ @ _). apply maponpaths_2. apply PushoutArrow_PushoutIn2. } etrans. { apply maponpaths. refine (!(functor_comp _ _ _) @ _). apply maponpaths. apply PushoutArrow_PushoutIn2. } etrans. { refine (!(functor_comp _ _ _) @ _). apply maponpaths. apply PushoutArrow_PushoutIn2. } refine (!_). refine (assoc _ _ _ @ _). etrans. { apply maponpaths_2. refine (assoc _ _ _ @ _). apply maponpaths_2. apply PushoutArrow_PushoutIn2. } etrans. { apply maponpaths_2. apply PushoutArrow_PushoutIn2. } refine (assoc' _ _ _ @ _). refine (id_left _ @ _). apply PushoutArrow_PushoutIn2. Qed.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat UniMath.CategoryTheory.TwoSidedDisplayedCats.DisplayedFunctor UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence UniMath.CategoryTheory.TwoSidedDisplayedCats.Examples.StructuredCospans UniMath.CategoryTheory.Limits.Pushouts UniMath.CategoryTheory.Limits.Preservation UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Examples.BicatOfUnivCats UniMath.Bicategories.DoubleCategories.Basics.DoubleCategoryBasics UniMath.Bicategories.DoubleCategories.Core.DoubleFunctor UniMath.Bicategories.DoubleCategories.Core.DoubleCats UniMath.Bicategories.DoubleCategories.Core.UnivalentDoubleCats UniMath.Bicategories.DoubleCategories.Examples.StructuredCospansDoubleCat