mathlib3
feat(category_theory/*): define `Cat` and a fully faithful functor `Mon ⥤ Cat`
#1235

Merged

feat(category_theory/*): define `Cat` and a fully faithful functor `Mon ⥤ Cat` #1235

mergify merged 10 commits into leanprover-community:master from urkud:single-obj-cat

urkud requested a review 6 years ago

urkud changed the title ~~feat(category_theory/*): define `Cat` and a fully faithful functor `Mon ⥤ Cat`~~ feat(category_theory/*): define `Cat` and a fully faithful functor `Mon ⥤ Cat` NOT READY YET 6 years ago

cipher1024 added WIP

feat(category_theory/*): define `Cat` and a fully faithful functor `M…

d04cca6a

urkud force pushed from bce89c4c to d04cca6a 6 years ago

Merge branch 'master' into single-obj-cat

8bc9afe9

Drop 2 commas

e96d9646

urkud changed the title ~~feat(category_theory/*): define `Cat` and a fully faithful functor `Mon ⥤ Cat` NOT READY YET~~ feat(category_theory/*): define `Cat` and a fully faithful functor `Mon ⥤ Cat` 6 years ago

jcommelin removed WIP

jcommelin assigned

rwbarton 6 years ago

jcommelin assigned

jcommelin 6 years ago

jcommelin requested a review from

kim-em 6 years ago

kim-em commented on 2019-07-19

Merge branch 'master' into single-obj-cat

2b7076fe

Drop `functor.id_comp` etc, add `Cat.str` instance, adjust module-lev…

cfbc518f

Merge branch 'master' into single-obj-cat

02676b2e

Make `α` and `β` arguments of `map_hom_equiv` explicit

193d274d

Merge branch 'master' into single-obj-cat

2022683e

jcommelin commented on 2019-07-22

jcommelin approved these changes on 2019-07-22

jcommelin added ready-to-merge

Merge branch 'master' into single-obj-cat

2e51f27c

Merge branch 'master' into single-obj-cat

347c552e

mergify merged 7c09ed5e into master 6 years ago

urkud deleted the single-obj-cat branch 6 years ago

Reviewers

jcommelin

kim-em

Assignees

rwbarton

jcommelin

Labels

ready-to-merge

Milestone

No milestone

mathlib3 feat(category_theory/*): define `Cat` and a fully faithful functor `Mon ⥤ Cat` #1235 Merged

feat(category_theory/*): define `Cat` and a fully faithful functor `Mon ⥤ Cat` #1235

mathlib3
feat(category_theory/*): define `Cat` and a fully faithful functor `Mon ⥤ Cat`
#1235

Merged