Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-21 12:09 82ef19af

View on Github →

feat(category_theory/path_category): canonical quotient of a path category (#13159)

Estimated changes

Modified src/category_theory/path_category.lean

added theorem category_theory.compose_path_comp'

added theorem category_theory.compose_path_id

added theorem category_theory.compose_path_to_path

added def category_theory.path_composition

added def category_theory.paths_hom_rel

added def category_theory.quotient_paths_equiv

added def category_theory.quotient_paths_to

added def category_theory.to_quotient_paths

Modified src/category_theory/quotient.lean

added theorem category_theory.quotient.comp_closure.of