proposition: Lemma isisomorphism_isequiv_set_cat `{H' : IsEquiv _ _ m} : IsIsomorphism (m : morphism set_cat x y).
proof: Proof. exists (m^-1)%core; apply path_forall; intro; destruct H'; simpl in *; eauto. Qed.
imports: Category.Core Functor.Core HomFunctor Category.Morphisms Category.Dual Functor.Dual Category.Prod Functor.Prod NaturalTransformation.Core SetCategory.Core Functor.Composition.Core Basics.Trunc Types.Universe HIT.iso HoTT.Truncations.Core