Commit 2018-11-24 03:53 beff80a7

feat(category_theory): preliminaries for limits (#488)

• style(category_theory): avoid long lines
• style(category_theory): rename embedding -> fully_faithful
• feat(category_theory/opposites): opposite of a functor
• style(category_theory/yoneda): minor changes
• make category argument implicit
• reverse order of arguments in yoneda_lemma
• avoid long lines
• feat(category_theory/functor_category): functor.flip
• feat(category_theory/isomorphism): eq_to_hom
• feat(category_theory/comma): comma categories
• feat(category_theory): pempty, punit categories
• feat(category_theory/products): add curried evaluation bifunctor It will be used later, to prove that (co)limits in diagram categories are computed pointwise.
• fixing order of definitions in opposites
• constructing fully_faithful instances