Def CategoryTheory.Functor.Fiber.mk

Modification history

2024-10-19 13:51

Mathlib/CategoryTheory/FiberedCategory/Fiber.lean

feat(FiberedCategory/Fiber): define the fibers of a functor (#13603) …

Added CategoryTheory.Functor.Fiber.mk View on Github →