feat(category_theory/monad): monadic adjunctions #1176
mergify
merged
30 commits into
master
from
monadic-adjunction
feat(category_theory/limits): equivalences create limits
d0c44ccb
equivalence lemma
1d141d6e
Merge branch 'master' into has_limit_comp_equivalence
80ad2b75
feat(category_theory/monad): monadic adjunctions
4286db3d
move file
0edcd8a7
fix
d80525ee
kim-em
changed the title
add @[simp]
b16a7ec2
Merge branch 'has_limit_comp_equivalence' of github.com:leanprover-co…
a9790400
Merge branch 'master' into has_limit_comp_equivalence
d4fe53fd
use right_adjoint_preserves_limits
3f307926
Merge branch 'master' into has_limit_comp_equivalence
e4f6130b
merge
434d34d3
fix
64e94424
fix
a44f2ecf
Merge branch 'master' into has_limit_comp_equivalence
c5337a02
Merge branch 'master' into has_limit_comp_equivalence
a65dd634
undo weird changes in topology files
2a97cef7
merge
4849ac45
formatting
71c68028
do colimits too
67c35425
merge
643b9803
Merge branch 'master' into monadic-adjunction
6aa4b811
kim-em
changed the title
missing proofs
12cdc428
Merge branch 'master' into monadic-adjunction
11f78158
convert monad to a typeclass decorating a functor
cfe5bda4
changing name
80f0d123
cleaning up
76b1c969
oops
81fcbe5d
minor
5720e43c
jcommelin
approved these changes
on 2019-07-20
![mergify[bot]](https://avatars.githubusercontent.com/in/10562?v=4&s=60)
Merge branch 'master' into monadic-adjunction
7556172a
Login to write a write a comment.
Login via GitHub