Definition is_disp_invertible_2cell_lunitor {B : bicat} {x y : B} {f : x --> y} {D : disp_bicat B} {xx : D x} {yy : D y} (ff : xx -->[f] yy) : is_disp_invertible_2cell (is_invertible_2cell_lunitor f) (disp_lunitor ff). Proof. use tpair. - exact (disp_linvunitor ff). - split. + etrans. { apply disp_lunitor_linvunitor. } apply (transportf_paths (λ p, _ ==>[p] _)). apply B. + etrans. { apply disp_linvunitor_lunitor. } apply (transportf_paths (λ p, _ ==>[p] _)). apply B. 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.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Core.Invertible_2cells.