Category of Families Set^X

Stream: Is there code for X?

[Max New]

For any set $X$ there is a category $\textrm{Set}^X$ whose objects are families $A : X \to \textrm{Set}$ and morphisms from $A$ to $B$ are families of functions $\forall x. A x \to B x$ . I haven't found this definition. Is this implemented somewhere in mathlib that I can't find?

[Max New]

It's equivalent to presheaves over the discrete category generated by X but that includes a lot of trivial data and some constructions have simpler definitions (like if X is a monoid that $\textrm{Set}^X$ is a monoidal category is much simpler than the Day convolution which involves coends)

[Robert Maxton]

There's a namespace FunctorToType, and there's a few things about presheaves, but to my knowledge that's about it.

[Robin Carlier]

Isn't this CategoryTheory.pi?

[Robin Carlier]

(deleted)

[Max New]

Thank you, yes this is an instance of pi. pi (fun _ => Type) That should save at least some work

[Robin Carlier]

Since pi is an instance I think the inferred category instance of X → Type u will be the one you want, as long as you have file#Mathlib.CategoryTheory.Pi.Basic in your import graph.