proposition: Lemma discrete_category_iso_path_groupoid (C : discrete_category) : catiso C (discrete_category_hset (setcategory_objects_set (_,, discrete_category_is_setcategory C))).
proof: 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.
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