(s d : set_cat) (m : s <~> d) : s <~=~> d := Build_Isomorphic (@isiso_isequiv s d m _). Global Instance isequiv_isiso_isequiv s d : IsEquiv (@ s d) | 0. Proof. refine (isequiv_adjointify (@ s d) (fun m => Build_Equiv _ _ _ (@isequiv_isiso s d m m)) _ _); simpl in *; clear; abstract ( intros [? ?]; simpl; unfold ; simpl; apply ap; apply path_ishprop ). Defined.
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.