s d (m : morphism set_cat s d) `{IsEquiv _ _ m} : IsIsomorphism m := Build_IsIsomorphism set_cat s d m m^-1%function (path_forall _ _ (eissect m)) (path_forall _ _ (eisretr m)).
Require Import Category.Core NaturalTransformation.Core. Require Import Category.Morphisms NaturalTransformation.Paths. Require Import Category.Univalent. Require Import SetCategory.Core. Require Import HoTT.Basics HoTT.Types TruncType.