fact: Definition cell_of_internal_sfib_over {B : bicat} {b₁ b₂ e₁ e₂ : B} {fb gb : b₁ --> b₂} (γ : fb ==> gb) {p₁ : e₁ --> b₁} {p₂ : e₂ --> b₂} (fe : mor_of_internal_sfib_over p₁ p₂ fb) (ge : mor_of_internal_sfib_over p₁ p₂ gb) : UU := ∑ (γe : fe ==> ge), cell_of_internal_sfib_over_homot γ γe.
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