Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-30 20:11 5800f69a

View on Github →

feat(category_theory/Quiv): the free/forgetful adjunction between Cat and Quiv (#7158)

Estimated changes

Created src/category_theory/category/Quiv.lean

added def category_theory.Cat.free

added def category_theory.Quiv.adj

added def category_theory.Quiv.forget

added def category_theory.Quiv.lift

added def category_theory.Quiv.of

added def category_theory.Quiv

Modified src/category_theory/functor.lean

modified structure category_theory.functor

Created src/category_theory/path_category.lean

added def category_theory.compose_path

added theorem category_theory.compose_path_comp

added def category_theory.paths.of

added def category_theory.paths

added theorem category_theory.prefunctor.map_path_comp'

Modified src/combinatorics/quiver.lean

added def prefunctor.comp

added def prefunctor.id

added def prefunctor.map_path

added theorem prefunctor.map_path_comp

added theorem prefunctor.map_path_cons

added theorem prefunctor.map_path_nil

added structure prefunctor

modified inductive quiver.path