fact: Definition comp_mor_of_internal_sfib_over {B : bicat} {e₁ e₂ e₃ b₁ b₂ b₃ : B} {fb₁ : b₁ --> b₂} {fb₂ : b₂ --> b₃} {p₁ : e₁ --> b₁} {p₂ : e₂ --> b₂} {p₃ : e₃ --> b₃} (fe₁ : mor_of_internal_sfib_over p₁ p₂ fb₁) (fe₂ : mor_of_internal_sfib_over p₂ p₃ fb₂) : mor_of_internal_sfib_over p₁ p₃ (fb₁ · fb₂).
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.DisplayedCats.StreetFibration UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Invertible_2cells UniMath.Bicategories.Core.Univalence