mathlib3
fix(category_theory/finite_limits): fix definition, and construct from finite products and equalizers
#1427
Merged
Merged
fix(category_theory/finite_limits): fix definition, and construct from finite products and equalizers #1427
mergify
merged
27 commits into
master
from
fix_finite_limits
chore(category_theory): require morphisms live in Type
3a394670
move back to Type
647b9ece
fix(category_theory/finite_limits): fix definition, and construct fro…
c4795504
fixes
484b1443
Merge branch 'master' into fix_finite_limits
035e2e6b
fix duplicate name
d31b8750
make fin_category a mixin
33ecc219
fix
8c6e3cea
fix
58036eb4
oops
38346ce4
Merge branch 'master' into fix_finite_limits
a70b6642
Merge branch 'fix_finite_limits' of github.com:leanprover-community/m…
24815016
Merge remote-tracking branch 'origin/master' into category_no_sorts
d9700b92
fixes
ec618c1a
merge
8220aa34
oops missing universe change
5f1ad5b0
Merge remote-tracking branch 'origin/master' into fix_finite_limits
714bb147
merge
a1abdaa3
finish documentation
26b61819
fix namespace
5aa68e5c
Merge remote-tracking branch 'origin/master' into fix_finite_limits
a87cded3
jcommelin
commented
on 2019-09-20
move variables to the right place
dab05c7c
don't repeat yourself
d31b157b
update module doc-string now that the files have been merged
79de1ada
inlining has_limit instances
953c5ccc
Merge remote-tracking branch 'origin/master' into fix_finite_limits
66c61250
jcommelin
approved these changes
on 2019-09-21
![mergify[bot]](https://avatars.githubusercontent.com/in/10562?v=4&s=60)
Merge branch 'master' into fix_finite_limits
c02cd5aa
Login to write a write a comment.
Login via GitHub