Library UniMath.Bicategories.DoubleCategories.DoubleFunctor.LeftUnitor

Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat.
Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos.
Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.DisplayedFunctor.
Require Import UniMath.Bicategories.DoubleCategories.DoubleCategoryBasics.
Require Import UniMath.Bicategories.DoubleCategories.DoubleFunctor.Basics.

Local Open Scope cat.

Unset Kernel Term Sharing.

Proposition comp_functor_lunitor
            {C₁ C₂ C₃ : category}
            {D₁ : twosided_disp_cat C₁ C₁}
            {D₂ : twosided_disp_cat C₂ C₂}
            {D₃ : twosided_disp_cat C₃ C₃}
            {I₁ : hor_id D₁}
            {I₂ : hor_id D₂}
            {I₃ : hor_id D₃}
            {Cm₁ : hor_comp D₁}
            {Cm₂ : hor_comp D₂}
            {Cm₃ : hor_comp D₃}
            {l₁ : double_cat_lunitor I₁ Cm₁}
            {l₂ : double_cat_lunitor I₂ Cm₂}
            {l₃ : double_cat_lunitor I₃ Cm₃}
            {F : C₁ ⟶ C₂}
            {FF : twosided_disp_functor F F D₁ D₂}
            {G : C₂ ⟶ C₃}
            {GG : twosided_disp_functor G G D₂ D₃}
            {FI : double_functor_hor_id FF I₁ I₂}
            {GI : double_functor_hor_id GG I₂ I₃}
            {FC : double_functor_hor_comp FF Cm₁ Cm₂}
            {GC : double_functor_hor_comp GG Cm₂ Cm₃}
            (Fl : double_functor_lunitor l₁ l₂ FI FC)
            (Gl : double_functor_lunitor l₂ l₃ GI GC)
  : double_functor_lunitor
      l₁ l₃
      (comp_hor_id FI GI)
      (comp_hor_comp FC GC).
Show proof.