Proposition pstrans_id_inv {B₁ B₂ : bicat} {F G : psfunctor B₁ B₂} (τ : pstrans F G) (x : B₁) : (psnaturality_of τ (id₁ x))^-1 • (τ x ◃ (psfunctor_id G x)^-1) = ((psfunctor_id F x)^-1 ▹ τ x) • lunitor _ • rinvunitor _. Proof. use vcomp_move_L_pM ; [ is_iso | ]. use vcomp_move_R_Mp ; [ is_iso | ]. use vcomp_move_L_pM; [ is_iso | ]. cbn -[psfunctor_id]. rewrite !vassocr. exact (!(pstrans_id τ x)). Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Core.AdjointUnique. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Require Import UniMath.Bicategories.DisplayedBicats.DispUnivalence. Require Import UniMath.Bicategories.DisplayedBicats.Examples.Prod. Require Import UniMath.Bicategories.DisplayedBicats.Examples.FullSub. Require Import UniMath.Bicategories.PseudoFunctors.Display.Base. Require Import UniMath.Bicategories.PseudoFunctors.Display.Map1Cells. Require Import UniMath.Bicategories.PseudoFunctors.Display.Map2Cells. Require Import UniMath.Bicategories.PseudoFunctors.Display.Identitor. Require Import UniMath.Bicategories.PseudoFunctors.Display.Compositor. Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat. Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor. Import PseudoFunctor.Notations.