Lemma discrete_category_iso_path_groupoid (C : discrete_category) : catiso C (discrete_category_hset (setcategory_objects_set (_,, discrete_category_is_setcategory C))). Proof. use tpair. - use make_functor. + use make_functor_data. * exact (idfun _). * intros a b f. apply isotoid. -- apply univalent_category_is_univalent. -- exact (@pregroupoid_hom_weq_iso C _ _ f). + use make_dirprod. * intro; apply setproperty. * intros ? ? ? ? ?; apply setproperty. - use make_dirprod. + intros a b. use isweq_iso. * intros f. apply idtoiso. assumption. * intro; apply discrete_category_hom_prop. * intro; apply setproperty. + apply idisweq. 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.