Lemma functor_path_pregroupoid {X : UU} {D : category} (i : isofhlevel 3 X) (f : X → ob D) : functor (path_pregroupoid X i) D. 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.
Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Setcategories. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Groupoids. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.exponentials. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.catiso. Require Import UniMath.Combinatorics.StandardFiniteSets. Section FunctorFromEmpty. End FunctorFromEmpty.