proposition: Lemma functor_path_pregroupoid {X : UU} {D : category} (i : isofhlevel 3 X) (f : X → ob D) : functor (path_pregroupoid X i) D.
proof: Proof. use make_functor. - use make_functor_data. + apply f. + intros a b aeqb. exact (transportf (λ z, D ⟦ f a, z ⟧) (maponpaths f aeqb) (identity _)). - split. + intro; reflexivity. + intros a b c g h; cbn. refine (maponpaths (λ p, transportf _ p _) (maponpathscomp0 _ _ _) @ _). refine (!transport_f_f _ (maponpaths f g) (maponpaths f h) _ @ _). abstract (induction h; cbn; apply pathsinv0; apply id_right). Defined.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.PartA UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Setcategories UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Groupoids UniMath.CategoryTheory.Limits.Initial UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.exponentials UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.catiso