PR #2100 feat(category_theory): images

feat(category_theory): images #2100

mergify merged 9 commits into master from categorical_images

feat(category_theory): images

72d64fa0

oops, forgot to add file

3e1110f3

jcommelin commented on 2020-03-07

Update src/category_theory/category/default.lean

97a852b3

some improvements

357da125

merge

6c157044

linting

abea0e26

oops

3ae89083

kim-em added awaiting-review

cipher1024 assigned

jcommelin 6 years ago

jcommelin approved these changes on 2020-03-09

Update src/category_theory/limits/shapes/images.lean

6bda40ae

jcommelin added ready-to-merge

jcommelin removed awaiting-review

Merge branch 'master' into categorical_images

b542959e

mergify merged 62abc4d5 into master 6 years ago

mergify deleted the categorical_images branch 6 years ago

Reviewers

jcommelin

Assignees

jcommelin

Labels

ready-to-merge

Milestone

No milestone