proposition: Lemma contr_cat_fully_faithful_to_isiso {F : functor C D} (ff : fully_faithful F) : is_catiso F.
proof: Proof. use make_dirprod; [assumption|]. apply isweqcontrcontr; apply contr_cat_iscontr. 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