# Commit 2019-05-14 20:21 7b579b79

View on Github →feat(category_theory): adjoint equivalences and limits under equivalences (#986)

- feat(category_theory): adjoint equivalences and limits
- Define equivalences to be adjoint equivalences.
- Show that one triangle law implies the other for equivalences
- Prove that having a limit of shape
`J`

is preserved under an equivalence`J ≌ J'`

. - Construct an adjoint equivalence from a (non-adjoint) equivalence

- Put
`nat_iso.app`

in the`iso`

namespace, so that we can write`α.app`

for`α : F ≅ G`

. - Add some basic lemmas about equivalences, isomorphisms.
- Move some lemmas from
`nat_trans`

to`functor_category`

and state them using`F ⟶ G`

instead of`nat_trans F G`

(maybe these files should just be merged?) - Some small tweaks, improvements
- opposite of discrete is discrete This also shows that C^op has coproducts if C has products and vice versa Also fix rebase errors
- fix error (I don't know what caused this to break)
- Use tidy a bit more
- construct an adjunction from an equivalence
add notation
`⊣`

for an adjunction. make some arguments of adjunction constructors implicit - use adjunction notation
- formatting
- do adjointify_η as a natural iso directly, to avoid checking naturality
- tersifying
- fix errors, a bit of cleanup
- fix elements.lean
- fix error, address comments