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. 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.
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.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.Examples.StructuredCospans. Require Import UniMath.CategoryTheory.Limits.Pushouts. Require Import UniMath.CategoryTheory.Limits.Preservation. 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.DoubleFunctor. Require Import UniMath.Bicategories.DoubleCategories.Core.DoubleCats. Require Import UniMath.Bicategories.DoubleCategories.Core.UnivalentDoubleCats. Require Import UniMath.Bicategories.DoubleCategories.Examples.StructuredCospansDoubleCat.