proposition: Proposition functor_double_comp_eq {C₁ C₂ : category} {D₁ : twosided_disp_cat C₁ C₁} {D₂ : twosided_disp_cat C₂ C₂} {F : C₁ ⟶ C₂} {FF : twosided_disp_functor F F D₁ D₂} {Cm₁ : hor_comp D₁} {Cm₂ : hor_comp D₂} (FC : double_functor_hor_comp FF Cm₁ Cm₂) {x₁ x₂ y₁ y₂ z₁ z₂ : C₁} {v₁ : x₁ --> x₂} {v₂ : y₁ --> y₂} {v₃ : z₁ --> z₂} {h₁ : D₁ x₁ y₁} {h₂ : D₁ x₂ y₂} {k₁ : D₁ y₁ z₁} {k₂ : D₁ y₂ z₂} (s₁ : h₁ -->[ v₁ ][ v₂ ] h₂) (s₂ : k₁ -->[ v₂ ][ v₃ ] k₂) : double_hor_comp_mor Cm₂ (#2 FF s₁) (#2 FF s₂) ;;2 functor_double_comp_cell FC _ _ = transportb_disp_mor2 (id_right _ @ !(id_left _)) (id_right _ @ !(id_left _)) (functor_double_comp_cell FC _ _ ;;2 #2 FF (double_hor_comp_mor Cm₁ s₁ s₂)).
proof: Proof. exact (pr2 FC x₁ x₂ y₁ y₂ z₁ z₂ v₁ v₂ v₃ h₁ h₂ k₁ k₂ s₁ s₂). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos UniMath.CategoryTheory.TwoSidedDisplayedCats.DisplayedFunctor UniMath.Bicategories.DoubleCategories.Basics.DoubleCategoryBasics