category_theory.is_iso_of_hom_simple source