Commit 2018-09-14 14:47 21233b7a

fix(category_theory/*): several minor fixes, preparatory to presheaves (#342)

• fix(category_theory/*): several minor fixes, preparatory to PR’ing the category of presheaves In category.lean, better proofs in instance [preorder α] : small_category α := …. In natural_isomorphism.lean, some rfl lemmas, natural isomorphisms describing functor composition, and formatting In examples/topological_spaces.lean, deciding to reverse the arrows in open_set X (the category of open sets, with restrictions), to reduce using opposites later, as well as describing the functoriality of open_set.
• additional simp lemmas