Definition disp_inserter_disp_cat_id_comp : disp_cat_id_comp _ disp_inserter_disp_cat. Proof. use tpair. - simpl. intros x fx. exact (((psfunctor_id F x)^-1 ▹ fx) • lunitor _ • rinvunitor _ • (_ ◃ psfunctor_id G x)). - simpl. intros x y z f g fx fy fz αf βg. exact (((psfunctor_comp _ _ _)^-1 ▹ _) • rassociator _ _ _ • (_ ◃ βg) • lassociator _ _ _ • (αf ▹ _) • rassociator _ _ _ • (_ ◃ psfunctor_comp _ _ _)). Defined.
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.Core.BicategoryLaws. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat. Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor. Import PseudoFunctor.Notations. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.DisplayedBicats.DispAdjunctions. Require Import UniMath.Bicategories.DisplayedBicats.DispUnivalence. Require Import UniMath.Bicategories.DisplayedBicats.Examples.Sub1Cell.