Commit 2023-03-03 08:09 f03c0dc8

View on Github →

feat: port CategoryTheory.PathCategory (#2580)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/PathCategory.lean

added theorem CategoryTheory.Paths.ext_functor

added def CategoryTheory.Paths.lift

added theorem CategoryTheory.Paths.lift_cons

added theorem CategoryTheory.Paths.lift_nil

added theorem CategoryTheory.Paths.lift_spec

added theorem CategoryTheory.Paths.lift_toPath

added theorem CategoryTheory.Paths.lift_unique

added def CategoryTheory.Paths.of

added def CategoryTheory.Paths

added theorem CategoryTheory.Prefunctor.mapPath_comp'

added def CategoryTheory.composePath

added theorem CategoryTheory.composePath_comp'

added theorem CategoryTheory.composePath_comp

added theorem CategoryTheory.composePath_cons

added theorem CategoryTheory.composePath_id

added theorem CategoryTheory.composePath_nil

added theorem CategoryTheory.composePath_toPath

added def CategoryTheory.pathComposition

added def CategoryTheory.pathsHomRel

added def CategoryTheory.quotientPathsEquiv

added def CategoryTheory.quotientPathsTo

added def CategoryTheory.toQuotientPaths