Definition id_is_eso_full_eq_2 {c₁ c₂ : B} (m : c₁ --> c₂) {l₁ l₂ : b --> c₁} (k₁ : id₁ b · l₁ ==> id₁ b · l₂) (k₂ : l₁ · m ==> l₂ · m) (p : (k₁ ▹ m) • rassociator (id₁ b) l₂ m = rassociator (id₁ b) l₁ m • (id₁ b ◃ k₂)) : (linvunitor l₁ • k₁ • lunitor l₂) ▹ m = k₂.
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.