Commit 2025-02-08 20:24 1c667105
View on Github →refactor(CategoryTheory): a structure describing transfinite compositions (#21417)
This PR introduces a structure CategoryTheory.TransfiniteCompositionOfShape J f which contains the data to express that a morphism f in a category C is a certain transfinite composition of morphisms indexed by a well ordered type J. This structure is extended in order to redefine MorphismProperty.transfiniteCompositionsOfShape.