Definition comp_psfunctor : psfunctor C E. Proof. use make_psfunctor. - exact comp_psfunctor_data. - exact comp_is_ps. - split. + intros a ; cbn. is_iso. * exact (psfunctor_id G (F a)). * exact (psfunctor_is_iso G (psfunctor_id F a)). + intros a b c f g ; cbn. is_iso. * exact (psfunctor_comp G (#F f) (#F g)). * exact (psfunctor_is_iso G (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.