Definition alg_disp_cat_id_comp : disp_cat_id_comp C alg_disp_cat. Proof. split ; cbn. - intros X f. refine (runitor f • linvunitor f • (psfunctor_id F X ▹ f) ,, _). is_iso. exact (psfunctor_id F X). - intros X Y Z f g hX hY hZ α β. refine ((lassociator hX f g) • (α ▹ g) • rassociator (#F f) hY g • (#F f ◃ β) • lassociator (#F f) (#F g) hZ • (psfunctor_comp F f g ▹ hZ) ,, _). is_iso. + exact α. + exact β. + exact (psfunctor_comp F f g). 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.