Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-07-03 18:10 cb842345

View on Github →

feat(category_theory/yoneda): coyoneda lemmas (#1172)

feat(category_theory/yoneda): coyoneda lemmas
oops, didn't include everything I needed
oops
removing fully_faithful
missing underscore...

Estimated changes

Modified src/category_theory/equivalence.lean

Modified src/category_theory/full_subcategory.lean

Modified src/category_theory/fully_faithful.lean

added def category_theory.is_iso_of_fully_faithful

added theorem category_theory.preimage_comp

modified theorem category_theory.preimage_id

added theorem category_theory.preimage_map

Modified src/category_theory/types.lean

Modified src/category_theory/yoneda.lean

added def category_theory.coyoneda.is_iso

added theorem category_theory.coyoneda.naturality

added def category_theory.yoneda.is_iso