fact: Definition isequiv_isiso_prop 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 _ _).
imports: Category.Core NaturalTransformation.Core Category.Morphisms NaturalTransformation.Paths Category.Univalent SetCategory.Core HoTT.Basics HoTT.Types TruncType