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. 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.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations.