Definition comp_mor_of_internal_sopfib_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_sopfib_over p₁ p₂ fb₁) (fe₂ : mor_of_internal_sopfib_over p₂ p₃ fb₂) : mor_of_internal_sopfib_over p₁ p₃ (fb₁ · fb₂). Proof. use make_mor_of_internal_sopfib_over. - exact (fe₁ · fe₂). - exact (comp_preserves_opcartesian (mor_of_internal_sopfib_over_preserves fe₁) (mor_of_internal_sopfib_over_preserves fe₂)). - use make_invertible_2cell. + exact (lassociator _ _ _ • (mor_of_internal_sopfib_over_com fe₁ ▹ _) • rassociator _ _ _ • (_ ◃ mor_of_internal_sopfib_over_com fe₂) • lassociator _ _ _). + is_iso. * apply property_from_invertible_2cell. * apply property_from_invertible_2cell. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.Examples.OpCellBicat. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Core.UnivalenceOp. Require Import UniMath.Bicategories.Morphisms.InternalStreetFibration.