mathlib3

5e3d465c - feat(category_theory/category/PartialFun): The category of types with partial functions (#11866)

feat(category_theory/category/PartialFun): The category of types with partial functions (#11866) Define `PartialFun`, the category of types with partial functions, and show its equivalence with `Pointed`.