In Lecture 4 of Lurie's notes on categorical logic, it is proved when a functor $F: Syn_0(T) \to Set$ arises from a model of the weak syntactic category. I think I can follow most of the argument, up until when it is claimed that the bijections supplied by $\iota_{[\varphi(x)]}$ are natural in $[\varphi(x)]$.
Is this because if we have a map $[\varphi(x)] \to [\psi(y)]$ in $Syn_0(T)$, that the map $F([\varphi(x)])\to F([\psi(y)])$ is given by the graph of $f_M$, where $M$ is the functor Lurie builds out of $F$? Or is there another way to see that these bijections are natural?
Thank you very much
Let $[\theta]: [\varphi] \to [\psi]$ be given.
If $\theta$ is equivalent to some projection or change of variables, then by definition naturality holds.
For any other $\theta$, we just take the "graph"
Then we have
$$F(\theta) F(\pi_1) = F(\pi_2)$$ $$F(\theta) i_{[\varphi]}^{-1} M(\pi_1) i_{[\theta \wedge \varphi]}^{-1} = i_{[\psi]}^{-1} M(\pi_2) i_{[\theta \wedge \varphi]}^{-1} = i_{[\psi]}^{-1} M(\theta) M(\pi_1) i_{[\theta \wedge \varphi]}^{-1}$$ $$F(\theta) i_{[\varphi]}^{-1} = i_{[\psi]}^{-1} M(\theta)$$