Mathlib Changelog
v3
Changelog
About
Github
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