Def category_theory.arrow.iso_mk'

feat(algebraic_geometry/open_immersion): Restricting a morphism twice is isomorphic to one restriction. (#15710)