Lemma is_invertible_2cell_vcomp {C : prebicat} {a b : C} {f g h: C ⟦a, b⟧} {x : f ==> g} (inv_x : is_invertible_2cell x) {y : g ==> h} (inv_y : is_invertible_2cell y) : is_invertible_2cell (x • y). Proof. use make_is_invertible_2cell. - exact (inv_y^-1 • inv_x^-1). - abstract ( repeat rewrite vassocl; etrans; [apply vassoc4|]; etrans; [ apply maponpaths_2, maponpaths; apply (vcomp_rinv inv_y) |]; rewrite id2_right; apply (vcomp_rinv inv_x) ). - abstract ( repeat rewrite vassocl; etrans; [apply vassoc4|]; etrans; [ apply maponpaths_2, maponpaths; apply (vcomp_linv inv_x) |]; rewrite id2_right; apply (vcomp_linv inv_y) ). 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.