Theorem CategoryTheory.IsHomLift.of_commsq

Modification history

2024-10-19 13:51
Mathlib/CategoryTheory/FiberedCategory/HomLift.lean
feat(FiberedCategory/Fiber): define the fibers of a functor (#13603) …
Added CategoryTheory.IsHomLift.of_commsqView on Github →