mathlib3

7b579b79 - feat(category_theory): adjoint equivalences and limits under equivalences (#986)

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