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. 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.
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.