proposition: 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: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.Bicategories.Core.Bicat