Properties of morphisms in a path category. #
We provide a formulation of induction principles for morphisms in a path category in terms of
MorphismProperty. This file is separate from CategoryTheory.PathCategory.Basic in order to
reduce transitive imports.
theorem
CategoryTheory.Paths.morphismProperty_eq_top
(V : Type u₁)
[Quiver V]
(P : CategoryTheory.MorphismProperty (CategoryTheory.Paths V))
(id : ∀ {v : V}, P (CategoryTheory.CategoryStruct.id (CategoryTheory.Paths.of.obj v)))
(comp :
∀ {u v w : V} (p : CategoryTheory.Paths.of.obj u ⟶ CategoryTheory.Paths.of.obj v) (q : v ⟶ w),
P p → P (CategoryTheory.CategoryStruct.comp p (CategoryTheory.Paths.of.map q)))
:
A reformulation of CategoryTheory.Paths.induction in terms of MorphismProperty.
theorem
CategoryTheory.Paths.morphismProperty_eq_top'
(V : Type u₁)
[Quiver V]
(P : CategoryTheory.MorphismProperty (CategoryTheory.Paths V))
(id : ∀ {v : V}, P (CategoryTheory.CategoryStruct.id (CategoryTheory.Paths.of.obj v)))
(comp :
∀ {u v w : V} (p : u ⟶ v) (q : CategoryTheory.Paths.of.obj v ⟶ CategoryTheory.Paths.of.obj w),
P q → P (CategoryTheory.CategoryStruct.comp (CategoryTheory.Paths.of.map p) q))
:
A reformulation of CategoryTheory.Paths.induction' in terms of MorphismProperty.