Commit 2024-11-15 02:04 e69ec59a
View on Github →chore(CategoryTheory/MorphismProperty): split HasTwoOutOfThreeProperty
(#18877)
Splits the HasTwoOutOfThreeProperty
typeclass into HasOfPrecompProperty
and HasOfPostcompProperty
. This allows more automation when working with P.Over Q X
categories.
Also shows that under suitable assumptions, HasOfPostcompProperty P
is equivalent to P ≤ P.diagonal
.