I'm looking for a reference that covers things like the lemma below – it doesn't have to be the exact statement I'm going to give, anything in the general ballpark would probably be useful. Or if you know a very short proof of the lemma – that would be interesting too.
So, I have a map $\pi: E \to U$ in a category $C$ (let's say $C$ has finite limits) that I want to think as a kind of "small maps classifier", that is I'm going to say that a map is "$\pi$-small" if it is a pullback of $\pi: E \to U$ (or maybe if it is locally a pullback of $E\to U$ for some notion of locality).
I'm interested in figuring out if small maps are closed under composition. In general, this has no reason to be true of course, but if the polynomial endofunctor $P_\pi$ induced by $\pi$ is a cartesian monad (which is often the case) then this should imply that $\pi$-small maps are closed under-composition. More precisely – I think we have the following:
Lemma : Assume the map $\pi$ is exponentiable, and let $P_\pi$ the polynomial endofunctor induced by $\pi$ (that is $P_\pi(X) = \pi_*(X \times E)$ seen as an endofunctor $C \to C$). Then the following are equivalent:
- $\pi$-small maps (that is pullback of $\pi$) are closed under composition.
- There exists a cartesian natural transformation $P_\pi \circ P_\pi \to P_\pi$.
I'm mostly interested in (2) => (1) and I'm fine with assuming that $P_\pi \circ P_\pi \to P_\pi$ is part of a monad structure. But as I said, anything in that spirit would be of interest. I feel there are many area of category theory where this could have been studied (Models of type theory, algebraic set theory, theory of polynomial functor, etc…) but I couldn't find it in the literature… The proof isn't awfully hard, but unless I'm missing something it require lots of stuff (like properties of polynomial functors and the formula for their composition, with some tricky computation on top of this)
Best Answer
This is mentioned in Remark 13 in
and then followed up in detail in:
as well as in: