¿Está cerrada la categoría de los finofuntores$\mathsf{Set}$ cartesianos?

Question

¿Está cerrada la categoría de los finofuntores$\mathsf{Set}$ cartesianos?

Usando el cálculo de extremos, podría derivar una fórmula para el exponencial (esto se presenta en el artículo Contenedores de orden superior de Altenkirch et al.):$$G^F(X) = \int_Y (X \to Y) \to F Y \to G Y$ $

¿Cómo puedo mostrar que este límite existe cuando$F$ y$G$ son finitos? ¿Cómo puedo mostrar que esta expresión da lugar a un endofunctor finito?

Answer 1

Me gustaría manejar esto al observar que su finitary endofunctor categoría $[\mathrm{Set},\mathrm{Set}]_{\mathrm{fin}}$ es equivalente a la categoría de todos los functors $[\mathrm{Set}_{\mathrm{fin}},\mathrm{Set}]$ a partir de la categoría de finito de conjuntos: los conjuntos son la libre cocompletion bajo filtrada colimits finito de conjuntos. Ahora, el último tiene un Cartesiana cerrada estructura definida por la misma fórmula como el tuyo, como lo hace cualquier presheaf categoría. Por lo tanto $[\mathrm{Set},\mathrm{Set}]_{\mathrm{fin}}$ debe admitir una Cartesiano estructura cerrada transferido desde que en $[\mathrm{Set}_{\mathrm{fin}},\mathrm{Set}]$. Pero su fórmula necesariamente calcula el homs en cualquier Cartesiano estructura cerrada, por lo que este transferidos estructura es la que quería verificar que existe.