proposition: Lemma is_invertible_2cell_rwhisker {C : prebicat} {a b c : C} {f1 f2 : a --> b} (g : b --> c) {x : f1 ==> f2} (inv_x : is_invertible_2cell x) : is_invertible_2cell (x ▹ g).
proof: Proof. use make_is_invertible_2cell. - exact (inv_x^-1 ▹ g). - abstract ( etrans; [ apply rwhisker_vcomp |]; etrans; [ apply maponpaths; apply (vcomp_rinv inv_x) |]; apply id2_rwhisker). - abstract ( etrans; [ apply rwhisker_vcomp |]; etrans; [ apply maponpaths; apply (vcomp_linv inv_x) |]; apply id2_rwhisker). Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.Bicategories.Core.Bicat