Commit 2019-05-05 07:02 1e8f438c

feat(presheaves) (#886)

• feat(category_theory/colimits): missing simp lemmas
• feat(category_theory): functor.map_nat_iso
• define functor.map_nat_iso, and relate to whiskering
• rename functor.on_iso to functor.map_iso
• add some missing lemmas about whiskering
• fix(category_theory): presheaves, unbundled and bundled, and pushforwards
• restoring (opens X)ᵒᵖ
• various changes from working on stalks
• rename nbhds to open_nhds
• fix introduced typo
• typo
• compactify a proof
• rename presheaf to presheaf_on_space
• fix(category_theory): turn has_limits classes into structures
• naming instances to avoid collisions
• breaking up instances.topological_spaces
• fixing all the other pi-type typclasses
• fix import
• oops
• fix import
• missed one
• typo
• restoring eq_to_hom simp lemmas
• removing unnecessary simp lemma
• remove another superfluous lemma
• removing the nat_trans and vcomp notations; use \hom and \gg
• a simpler proposal
• getting rid of vcomp
• fix
• splitting files
• update notation
• fix
• cleanup
• use iso_whisker_right instead of map_nat_iso
• proofs magically got easier?
• improve some proofs
• remove crap
• minimise imports
• chore(travis): disable the check for minimal imports
• Update src/algebraic_geometry/presheafed_space.lean Co-Authored-By: semorrison scott@tqft.net
• writing op_induction tactic, and improving proofs
• squeeze_simping
• cleanup
• rearranging
• Update src/category_theory/instances/Top/presheaf.lean Co-Authored-By: semorrison scott@tqft.net
• fix open statements, and use op_induction
• rename terms of PresheafedSpace to X Y Z. rename field from .X to .to_Top
• forgetful functor
• update comments about unfortunate proofs
• add coercion from morphisms of PresheafedSpaces to morphisms in Top