Keith wrote:

> So, given a functor \$$G: \mathcal{D} \to \mathcal{C}\$$, we can create a new functor from that acts by pre-composition, this functor acts backward to the original functor, like pullbacks did, so I'll call it \$$G^*\$$,

> \$G^* : [\mathcal{C},-] \to [\mathcal{D},-], \\\\ G^* = G\circ- \$

You mean

$G^* = - \circ G ,$

because as you said, we are _pre_-composing with \$$G\$$, and we're using the usual notation where \$$(F \circ G)(d) = F(G(d))\$$ does \$$G\$$ _first_.

> then given another functor \$$F : \mathcal{C} \to \mathbf{Set}\$$, we can create a new functor,

> \$G^*(F) : [\mathcal{C},\mathbf{Set}] \to [\mathcal{D},\mathbf{Set}], \$
so then \$$H :\mathcal{D} \to \mathbf{Set}\$$ is sort of like when there was a subset we wanted to look at, and \$$\mathrm{Lan}_G(H)\$$ is like the pullback's left-adjoint (wasn't that an existential quantifier)?

> Am I getting this right, or am I torturing analogies here?

No, everything you say here is right!

What I called \$$F \circ G\$$ is indeed often called the **pullback of \$$F\$$ along \$$G\$$** and written \$$F^\ast(G)\$$. The left Kan extension functor \$$\mathrm{Lan}_G\$$ is the left adjoint of the pullback functor \$$G^*\$$.

And indeed, the left Kan extension is connected to existential quantifiers - though it's more closely connected to sums, which is why Fong and Spivak call it \$$\sum\$$. Back when we were studying preorders, also known as \$$\textbf{Bool}\$$-categories, we were often interested in just whether or not something is true. Now we're often interested in the _set of ways_ in which something is true. For example, we don't just care about whether there is a German in our database: we want to know the actual set of Germans!

The only reason I've been writing stuff like

> $\textrm{composing with } G : \mathbf{Set}^{\mathcal{C}} \to \mathbf{Set}^{\mathcal{D}}$

$G^\ast : \mathbf{Set}^{\mathcal{C}} \to \mathbf{Set}^{\mathcal{D}}$