Commit 2019-05-14 20:21 7b579b79

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