proposition: Lemma contr_cat_eq {F : functor C D} (ff : fully_faithful F) : C = D.
proof: Proof. apply subtypePath. - intro; apply isapropiscontr. - apply catiso_to_category_path. use tpair. + exact F. + apply contr_cat_fully_faithful_to_isiso; assumption. Defined.
imports: UniMath.Foundations.Preamble UniMath.MoreFoundations.PartA UniMath.Algebra.Groups UniMath.Algebra.RigsAndRings UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.catiso UniMath.CategoryTheory.Additive UniMath.CategoryTheory.CategoriesWithBinOps UniMath.CategoryTheory.PreAdditive UniMath.CategoryTheory.PrecategoriesWithAbgrops UniMath.CategoryTheory.Categories.HSET.Core