mathlib3
feat(category_theory/limits): pullbacks from binary products and equalizers
#2143

Merged

feat(category_theory/limits): pullbacks from binary products and equalizers #2143

mergify merged 11 commits into master from shape-iso2

feat(category_theory/limits): derive has_binary_products from has_lim…

48d05546

Rename *_of_diagram to diagram_iso_*

41111043

feat(category_theory/limits): pullbacks from binary products and equa…

5bb4290b

Fix build

56bbb5fa

TwoFX added blocked-by-other-PR

Fix indentation

cbea7034

TwoFX removed blocked-by-other-PR

Merge branch 'master' into shape-iso2

b1772659

merge

5003e899

kim-em commented on 2020-03-14

typos

1773496e

kim-em approved these changes on 2020-03-14

kim-em added ready-to-merge

kim-em removed ready-to-merge

Fix proof

462ac4fd

Remove some simp lemmas that were duplicated during merge

6fac3392

kim-em added ready-to-merge

Merge branch 'master' into shape-iso2

0ded0e20

mergify merged c240fcb3 into master 6 years ago

mergify deleted the shape-iso2 branch 6 years ago

Reviewers

kim-em

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone