s d (m : morphism prop_cat s d) `{IsIsomorphism _ _ _ m} : IsEquiv m := Build_IsEquiv _ _ m m^-1%morphism (ap10 right_inverse) (ap10 left_inverse) (fun _ => path_ishprop _ _).
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.