mathlib3
feat(category_theory): adjoint equivalences and limits under equivalences
#986
Merged
Merged
feat(category_theory): adjoint equivalences and limits under equivalences #986
mergify
merged
14 commits into
master
from
limits-isos
jcommelin
commented
on 2019-05-06
jcommelin
commented
on 2019-05-06
kim-em
commented
on 2019-05-06
feat(category_theory): adjoint equivalences and limits
29d2fa6e
opposite of discrete is discrete
58058599
fix error (I don't know what caused this to break)
bfd336b0
Use tidy a bit more
b8ff7dd7
construct an adjunction from an equivalence
3f9268a0
use adjunction notation
487762b2
formatting
e0c2c9cd
do adjointify_η as a natural iso directly, to avoid checking naturality
bd8c2bbb
tersifying
fc2bbd43
fix errors, a bit of cleanup
a7d9b1ee
fix elements.lean
56521547
Merge remote-tracking branch 'blessed/master' into limits-isos
496c2ead
fix error, address comments
738e1226
rwbarton
approved these changes
on 2019-05-14
Merge branch 'master' into 'limits-isos'
54ebf5a4
Login to write a write a comment.