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

Merged

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

mergify merged 5 commits into master from category_no_sorts

chore(category_theory): require morphisms live in Type

3a394670

move back to Type

647b9ece

kim-em requested a review 6 years ago

kim-em changed the title ~~fix(category_theory): require morphisms are in Type, again~~ fix(category_theory): require morphisms are in Type, again (merge this or #1417) 6 years ago

rwbarton commented on 2019-09-12

Merge remote-tracking branch 'origin/master' into category_no_sorts

d9700b92

fixes

ec618c1a

kim-em changed the title ~~fix(category_theory): require morphisms are in Type, again (merge this or #1417)~~ fix(category_theory): require morphisms are in Type, again 6 years ago

cipher1024 assigned

rwbarton 6 years ago

rwbarton approved these changes on 2019-09-17

rwbarton added ready-to-merge

Merge branch 'master' into category_no_sorts

bf64faeb

mergify merged 19a246c4 into master 6 years ago

mergify deleted the category_no_sorts branch 6 years ago

Reviewers

rwbarton

Assignees

rwbarton

Labels

ready-to-merge

Milestone

No milestone

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

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

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

Merged