Definition ap_psfunctor : psfunctor (fundamental_bigroupoid X HX) (fundamental_bigroupoid Y HY). Proof. use make_psfunctor. - exact ap_functor_data. - exact ap_functor_laws. - split. + intros a. exact (fundamental_groupoid_2cell_iso Y HY (idpath(idpath (f a)))). + intros a b c p q. exact (fundamental_groupoid_2cell_iso Y HY (!(maponpathscomp0 f p q))). 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.Invertible_2cells. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat. Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor. Import PseudoFunctor.Notations. Require Import UniMath.Bicategories.Core.Examples.TwoType.