Definition disp_path_pgroupoid : disp_psfunctor p1types_disp pgrpds_disp path_groupoid. Proof. use make_disp_psfunctor. - exact pgrpds_disp_2cells_isaprop. - exact pgrpds_disp_locally_groupoid. - exact (λ X x, x). - intros X Y f x y p. simpl in *. exact (p ,, pr2 (path_groupoid Y) _ _ p). - abstract (intros X Y f g α x y p q αα ; cbn in * ; exact (!αα)). - abstract (intros X x ; apply idpath). - abstract (intros X Y Z f g x y z p q ; apply idpath). Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.TransportMorphisms. Require Import UniMath.CategoryTheory.Groupoids. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.Categories.StandardCategories. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Examples.OneTypes. Require Import UniMath.Bicategories.Core.Examples.Groupoids. Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor. Require Import UniMath.Bicategories.PseudoFunctors.Biequivalence. Require Import UniMath.Bicategories.PseudoFunctors.Examples.PathGroupoid. Require Import UniMath.Bicategories.PseudoFunctors.Examples.Identity. Require Import UniMath.Bicategories.PseudoFunctors.Examples.Composition. Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat. Require Import UniMath.Bicategories.Transformations.PseudoTransformation. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.DisplayedBicats.DispUnivalence. Require Import UniMath.Bicategories.DisplayedBicats.Examples.FullSub. Require Import UniMath.Bicategories.DisplayedBicats.Examples.PointedOneTypes. Require Import UniMath.Bicategories.DisplayedBicats.DispPseudofunctor. Require Import UniMath.Bicategories.DisplayedBicats.DispTransformation. Require Import UniMath.Bicategories.DisplayedBicats.DispModification. Require Import UniMath.Bicategories.DisplayedBicats.DispBiequivalence. Require Import UniMath.Bicategories.DisplayedBicats.DispBuilders.