fact: Definition is_invertible_2cell_hcomp {C : bicat} {X Y Z : C} {f₁ g₁ : C⟦Y,Z⟧} {f₂ g₂ : C⟦X,Y⟧} (η₁ : f₁ ==> g₁) (η₂ : f₂ ==> g₂) (inv_η₁ : is_invertible_2cell η₁) (inv_η₂ : is_invertible_2cell η₂) : is_invertible_2cell (η₁ ⋆⋆ η₂).
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.Bicategories.Core.Bicat