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 : MorphismProperty (Paths V))
(id : ∀ {v : V}, P (CategoryStruct.id (of.obj v)))
(comp : ∀ {u v w : V} (p : of.obj u ⟶ of.obj v) (q : v ⟶ w), P p → P (CategoryStruct.comp p (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 : MorphismProperty (Paths V))
(id : ∀ {v : V}, P (CategoryStruct.id (of.obj v)))
(comp : ∀ {u v w : V} (p : u ⟶ v) (q : of.obj v ⟶ of.obj w), P q → P (CategoryStruct.comp (of.map p) q))
:
A reformulation of CategoryTheory.Paths.induction' in terms of MorphismProperty.