proposition: Lemma is_invertible_2cell_lwhisker {C : prebicat} {a b c : C} (f : a --> b) {g1 g2 : b --> c} {x : g1 ==> g2} (inv_x : is_invertible_2cell x) : is_invertible_2cell (f ◃ x).
proof: Proof. use make_is_invertible_2cell. - exact (f ◃ inv_x^-1). - abstract ( etrans; [ apply lwhisker_vcomp |]; etrans; [ apply maponpaths; apply (vcomp_rinv inv_x) |]; apply lwhisker_id2). - abstract ( etrans; [ apply lwhisker_vcomp |]; etrans; [ apply maponpaths; apply (vcomp_linv inv_x) |]; apply lwhisker_id2). Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.Bicategories.Core.Bicat