Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-09-11 10:07 ba7bd742

View on Github →

feat(category_theory): Yoneda, basic facts about natural isomorphisms, and an extensionality lemma using Yoneda lemma (#326)

feat(category_theory/yoneda_lemma)
feat(category_theory/natural_isomorphisms): basic facts about natural isomorphisms, and an extensionality lemma using Yoneda

Estimated changes

Created category_theory/natural_isomorphism.lean

added def category_theory.nat_iso.app

added theorem category_theory.nat_iso.comp_app

added theorem category_theory.nat_iso.hom_eq_coe

added theorem category_theory.nat_iso.inv_eq_symm_coe

added theorem category_theory.nat_iso.naturality_1

added theorem category_theory.nat_iso.naturality_2

added def category_theory.nat_iso.of_components

Modified category_theory/types.lean

added theorem category_theory.types.iso_mk_coe

Created category_theory/yoneda.lean

added def category_theory.yoneda.ext

added theorem category_theory.yoneda.map_app

added theorem category_theory.yoneda.naturality

added theorem category_theory.yoneda.obj_map

added theorem category_theory.yoneda.obj_map_id

added theorem category_theory.yoneda.obj_obj

added def category_theory.yoneda

added def category_theory.yoneda_evaluation

added theorem category_theory.yoneda_evaluation_map_down

added def category_theory.yoneda_lemma

added def category_theory.yoneda_pairing

added theorem category_theory.yoneda_pairing_map