mathlib

92b27e12 - feat(category_theory/discrete_category): generalize universes for comp_nat_iso_discrete (#12340)