Definition invertible_is_eso_full : is_eso_full e₂. Proof. intros c₁ c₂ m Hm l₁ l₂ k₁ k₂ p. simple refine (_ ,, _ ,, _). - simple refine (is_eso_lift_2 _ He Hm l₁ l₂ _ k₂ _). + exact ((α ▹ l₁) • k₁ • (Hα^-1 ▹ l₂)). + abstract (rewrite <- !rwhisker_vcomp ; rewrite !vassocl ; rewrite rwhisker_rwhisker_alt ; rewrite !vassocr ; use vcomp_move_R_Mp ; [ is_iso | ] ; cbn ; rewrite !vassocl ; rewrite p ; rewrite <- vcomp_whisker ; rewrite !vassocr ; apply maponpaths_2 ; rewrite rwhisker_rwhisker_alt ; apply idpath). - abstract (cbn ; use (vcomp_lcancel (α ▹ _)) ; [ is_iso | ] ; rewrite vcomp_whisker ; rewrite is_eso_lift_2_left ; rewrite !vassocl ; rewrite rwhisker_vcomp ; rewrite vcomp_linv ; rewrite id2_rwhisker ; rewrite id2_right ; apply idpath). - apply is_eso_lift_2_right. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Core.AdjointUnique. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Core.EquivToAdjequiv. Require Import UniMath.Bicategories.Morphisms.FullyFaithful. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Morphisms.DiscreteMorphisms. Require Import UniMath.Bicategories.Morphisms.Eso. Require Import UniMath.Bicategories.Limits.Pullbacks.