mathlib3
feat(category_theory/limits): construct limits from products and equalizers
#1362
Merged
Merged
feat(category_theory/limits): construct limits from products and equalizers #1362
mergify
merged
51 commits into
master
from
limits-constructions
providing minimal API for limits of special shapes
b56eb60e
apis for special shapes
d53fbece
fintype instances
2de84ddc
associators, unitors, braidings for binary product
0935f0c6
map
7244ebc1
instances
4bf314f5
assoc lemma
0ef49a42
coprod
e122f163
Merge branch 'master' into limits-shapes
4874a288
fix import
223ad515
names
5cfcddc1
adding some docs
493b4813
updating tutorial on limits
edde84b9
minor
79d79760
uniqueness of morphisms to terminal object
3b225b95
better treatment of has_terminal
e5fa7e20
various
3be27860
not there yet
44fa640a
deleting a dumb file
e940511c
remove constructions for a later PR
e4a4e810
getting there
f613a120
oops
9fd3a7bf
of_nat_iso
6a904b4c
merge
9926c244
feat(category_theory/limits/of_nat_isp)
75d95d01
merge
b33e91ea
progress on limits from products and equalizers
7e4d993b
Update src/category_theory/limits/limits.lean
852e144f
Update src/category_theory/limits/limits.lean
99d1ef74
use @[reassoc]
b4c5df76
Merge branch 'limits_nat_iso' of github.com:leanprover-community/math…
17bb2666
Merge branch 'master' into limits_nat_iso
c46bf218
fixing after rename
18db80c5
Merge branch 'master' into limits-shapes
b591907c
use @[reassoc]
3aa49a8a
fix renaming
eebfadf6
complete construction of limits from products and equalizers
d3c40c25
cleanup
d40e5c7d
cleanup
85bff294
Merge remote-tracking branch 'origin/lean-3.4.2' into limits-construc…
b4fc943d
Merge remote-tracking branch 'origin/limits-shapes' into limits-const…
c85a8600
Merge remote-tracking branch 'origin/limits_nat_iso' into limits-cons…
fe79aeac
Merge remote-tracking branch 'origin/master' into limits-constructions
a3832bfe
khoek
commented
on 2019-08-27
name instance
f478b2b8
Merge branch 'master' into limits-constructions
7b9fa3b4
kim-em
changed the title
merge
583552e2
khoek
commented
on 2019-08-31
whitespace
2e9455f7
kim-em
changed the title
Merge branch 'master' into limits-constructions
0c8b6609
jcommelin
commented
on 2019-09-01
Update src/category_theory/limits/limits.lean
10a0c5e1
Merge branch 'master' into limits-constructions
ff1350b9
jcommelin
commented
on 2019-09-02
use simpa
aa439718
jcommelin
approved these changes
on 2019-09-02
Reviewers
Assignees
No one assigned
Labels
ready-to-merge
Milestone
No milestone
Login to write a write a comment.
Login via GitHub