Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-08-18 00:55 cfb27cbe

View on Github →

feat(category_theory): opposites, and the category of types (#249)

Estimated changes

Modified category_theory/category.lean

Modified category_theory/functor.lean

Modified category_theory/functor_category.lean

Modified category_theory/natural_transformation.lean

Created category_theory/opposites.lean

added theorem category_theory.functor.hom_obj

added theorem category_theory.functor.hom_pairing_map

added theorem category_theory.functor.opposite_map

added theorem category_theory.functor.opposite_obj

added def category_theory.op

Modified category_theory/products.lean

modified theorem category_theory.functor.prod_map

modified theorem category_theory.functor.prod_obj

modified theorem category_theory.nat_trans.prod_app

Created category_theory/types.lean

added theorem category_theory.functor_to_types.hcomp

added theorem category_theory.functor_to_types.map_comp

added theorem category_theory.functor_to_types.map_id

added theorem category_theory.functor_to_types.naturality

added theorem category_theory.functor_to_types.vcomp

added theorem category_theory.types_comp

added theorem category_theory.types_hom

added theorem category_theory.types_id

Modified tactic/ext.lean

added theorem ulift.ext