Commit 2025-11-02 18:17 b90d0b5c
View on Github →chore(CategoryTheory/FiberedCategory/HomLift): Unify IsHomLift and IsHomLiftAux (#31125)
The definition IsHomLiftAux is not necessary, as inductives can be classes themselves. (see for example Decidable).
This PR makes Functor.IsHomLift itself an inductive, taking out the middle man.