fact: Definition has_inserter_ump_1_left_adjoint_equivalence_pr1 : invertible_2cell (has_inserter_ump_1_left_adjoint_equivalence_mor · inserter_cone_pr1 cone₂) (inserter_cone_pr1 q) := comp_of_invertible_2cell (rassociator_invertible_2cell _ _ _) (comp_of_invertible_2cell (lwhisker_of_invertible_2cell _ γ₁) (comp_of_invertible_2cell (lassociator_invertible_2cell _ _ _) (comp_of_invertible_2cell (rwhisker_of_invertible_2cell _ (inserter_ump_mor_pr1 H _ _)) (comp_of_invertible_2cell (rassociator_invertible_2cell _ _ _) (comp_of_invertible_2cell (lwhisker_of_invertible_2cell _ εx) (runitor_invertible_2cell _)))))).
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Invertible_2cells UniMath.Bicategories.Core.BicategoryLaws UniMath.Bicategories.Core.Unitors UniMath.Bicategories.Core.EquivToAdjequiv UniMath.Bicategories.Morphisms.Adjunctions UniMath.Bicategories.Morphisms.FullyFaithful UniMath.Bicategories.Morphisms.Properties.ContainsAdjEquiv UniMath.Bicategories.Limits.Inserters