Commit 2024-07-05 06:46 ee4303e0

chore: make MorphismProperty.RespectsIso a typeclass (#14353) Most of the properties of properties of morphisms should be made typeclasses. For example, IsMultiplicative, HasTwoOutOfThreeProperty are already typeclasses (because it is convenient for the localization of categories). In this PR, MorphismProperty.RespectsIso is made a typeclass. One of the reasons to do so is that it should ease the development of the notion of "representable" morphisms of presheaves #14208. Another is that most of the reasonable properties of morphisms which we encounter satisfy this property: we should not have to remember the names of lemmas which assert this trivial property!