Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-09-17 15:50 19a246c4

View on Github →

fix(category_theory): require morphisms are in Type, again (#1412)

  • chore(category_theory): require morphisms live in Type
  • move back to Type
  • fixes

Estimated changes

modified def category_theory.over
modified def category_theory.under
modified def category_theory.Aut
modified def category_theory.End
modified structure category_theory.nat_trans
modified theorem category_theory.types_comp
modified theorem category_theory.types_hom
modified theorem category_theory.types_id