Presheaf categories are cartesian closed.

Stream: new members

[Yiming Xu]

I want to formalize the proof that presheaf categories are cartesian closed. (In the case that someone still remember, the exercise I tried several weeks ago is a special case of this statement). Is there any suggested brief roadmap to get it?

The proof is not long. Say, in Leinster, it looks like:
image.png

I will also need "every presheaf is a colimit of representables". Does it already exist somewhere?

[Yiming Xu]

By "roadmap" I am not asking a proof unless someone thinks there is a more direct approach (in a sense that easier to obtain using the results in mathlib). I am asking where would be the correct places to spot the theorems useful for formalizaing this proof, since I am not yet familiar with mathlib. Any attempt of helping would be greatly appreciated! Thanks in advance.

[Joël Riou]

@Dagur Asgeirsson has already formalized an abstract proof that functor categories are monoidal closed. In a WIP PR #19103, I shall obtain a more explicit construction.

[Yiming Xu]

Joël Riou said:

Dagur Asgeirsson has already formalized an abstract proof that functor categories are monoidal closed. In a WIP PR #19103, I shall obtain a more explicit construction.

Thanks a lot! May I please ask if you can inform me when you get it done? I am very interested in such a procedure.

[Dagur Asgeirsson]

If you're interested, the abstract proof Joël mentions is here. We have also had cartesian closure of type-valued presheaf categories for quite some time here

[Yiming Xu]

Dagur Asgeirsson said:

If you're interested, the abstract proof Joël mentions is here. We have also had cartesian closure of type-valued presheaf categories for quite some time here

Thanks so much for the quick reply! I will take a look.