Definition ap_functor_data : psfunctor_data (fundamental_bigroupoid X HX) (fundamental_bigroupoid Y HY). Proof. use make_psfunctor_data. - exact f. - exact (λ _ _, maponpaths f). - exact (λ _ _ _ _ s, maponpaths (maponpaths f) s). - exact (λ x, idpath (idpath (f x))). - exact (λ _ _ _ p q, !(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.