Documentation

Mathlib.CategoryTheory.PathCategory.MorphismProperty

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.

A reformulation of CategoryTheory.Paths.induction in terms of MorphismProperty.