LiftAlongMonomorphism/ColiftAlongEpimorphism

[mohamed-barakat]

The ability to compute LiftAlongMonomorphism/ColiftAlongEpimorphism is currently used to distinguish pre-abelian categories from abelian ones. However, in CAP they can be derived from the set-theoretic operations Lift/Colift with no further restriction. This defeats their purpose.

I encountered the problem in the nonlinear setup where LiftAlongMonomorphism/ColiftAlongEpimorphism should not be computable, but were automatically derived from Lift/Colift.

Solution: I would suggest adding the categorical properties IsCategoryWithRegularMonos/IsCategoryWithRegularEpis (or better names) and only derive LiftAlongMonomorphism/ColiftAlongEpimorphism from Lift/Colift only in case IsCategoryWithRegularMonos/IsCategoryWithRegularEpis was set to true.