Definition is_disp_invertible_2cell_rinvunitor {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_rinvunitor f) (disp_rinvunitor ff). Proof. use tpair. - exact (disp_runitor ff). - split. + etrans. { apply disp_rinvunitor_runitor. } apply (transportf_paths (λ p, _ ==>[p] _)). apply B. + etrans. { apply disp_runitor_rinvunitor. } 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.