Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: theory: category theory

Topic: type theory of a topos

Christian Williams (Apr 13 2021 at 21:19):

Toposes are cartesian closed --- but often functors are not, so we consider geometric morphisms. These preserve geometric logic; but the full internal language, dependent type theory (represented by the codomain fibration), is not preserved.

How do we describe the construction which sends a topos to its internal language? We have to accept that geometric morphisms are not locally cartesian closed. $Lang: Topos\to -$ : What is the codomain of this functor?

Christian Williams (Apr 13 2021 at 21:22):

We could use logical functors which preserve all topos structure, but there are theorems that show these are actually rare and special.

Christian Williams (Apr 13 2021 at 21:31):

We can say $Lang: Topos\to Fib$ sends each topos to its codomain fibration $cod(E):Arr(E)\to E$, and since geometric morphisms preserve finite limits this is functorial --- but this does not reflect the fact that $cod(E)$ has dependent sums and products.

Christian Williams (Apr 13 2021 at 21:38):

If anyone has ideas or references on the (functorial) construction from a topos to its type theory, please let me know.

Matteo Capucci (he/him) (Apr 14 2021 at 06:20):

I suspect the right thing to do is to send a topos to its tripos of subobjects, hence a fibration

Matteo Capucci (he/him) (Apr 14 2021 at 06:22):

There is actually an adjunction between triposes and toposes iirc
You can surely extend it on both sides to less structured hyperdoctrines and less structured categories

Matteo Capucci (he/him) (Apr 14 2021 at 06:22):

My standard reference for all this stuff is Jacobs' Categorical Logic

Matteo Capucci (he/him) (Apr 14 2021 at 06:25):

Another pov one may pursue is to consider toposes and syntactic sites. I'm less familiar with this but it's what you find in Caramello's book

Morgan Rogers (he/him) (Apr 14 2021 at 12:49):

Christian Williams said:

We can say $Lang: Topos\to Fib$ sends each topos to its codomain fibration $cod(E):Arr(E)\to E$, and since geometric morphisms preserve finite limits this is functorial --- but this does not reflect the fact that $cod(E)$ has dependent sums and products.

When you say "this does not reflect the fact that..." do you mean that this Lang functor doesn't reflect that structure in a technical sense?

Christian Williams (Apr 14 2021 at 15:11):

I mean that the codomain fibration of an LCCC has fibered sums and products, but they are not preserved by geometric morphisms and so we have to take the codomain to be only Fib and not CCFib (co/cocartesian Fib; also called *-bifibrations)

Christian Williams (Apr 14 2021 at 15:19):

It would be very helpful to see an adjunction between toposes and triposes. Do you know a reference?

Morgan Rogers (he/him) (Apr 14 2021 at 15:35):

Christian Williams said:

I mean that the codomain fibration of an LCCC has fibered sums and products, but they are not preserved by geometric morphisms and so we have to take the codomain to be only Fib and not CCFib (co/cocartesian Fib; also called *-bifibrations)

Surely you can describe the category whose objects are those of CCFib but whose morphisms are just morphisms of fibrations? What obstacle are you encountering here?

Christian Williams (Apr 14 2021 at 18:45):

yes, that is an option. I just want to know what it really means type-theoretically, and why we can't do better.

Christian Williams (Apr 14 2021 at 18:46):

geometric morphisms preserve a decent amount of structure, so there should be some more we can say.

Christian Williams (Apr 14 2021 at 18:47):

I've just been surprised with how little I've found about the functoriality of the construction of internal type systems. I haven't even seen inference rules for induced maps of type systems.

Christian Williams (Apr 14 2021 at 18:50):

the attitude seems to be "of course we can get MLTT from a topos", but when it comes to specifying it as a functorial construction, I've seen no discussion that topos morphisms do not preserve type constructors, what this means for type theory and how to deal with it.

Morgan Rogers (he/him) (Apr 14 2021 at 19:05):

Ah yep, that's a general feature of the topos theory literature: there's a lot that has been done in principle but so few people applying the tools that most of them are not developed to the point of usefulness, especially from the perspective of functoriality (either that or they have been used infrequently enough as to be difficult to find).
If you know what type constructions you're particularly interested in preserving (and you can express them in a form I can understand :wink: ) I can help you to identify which class of geometric morphisms you actually need. For example, locally connected morphisms have inverse images which commute with dependent products, and that might be a sufficient class for your purposes.

Christian Williams (Apr 14 2021 at 19:07):

yes, definitely.

Christian Williams (Apr 14 2021 at 19:08):

great, thanks! yes, locally connected seems like the right class - but as you said before, precomposition
$[F,Set]:[D,Set]\to [C,Set]$ is only locally connected under pretty special conditions.

Christian Williams (Apr 14 2021 at 19:09):

and I'm focused on plugging $y:Cat\to Topos$ into the construction from toposes to type systems.

Morgan Rogers (he/him) (Apr 14 2021 at 19:11):

In that case Corollary 4.58 here might be useful to you: if you restrict yourself to fibrations between small categories rather than arbitrary functors, then you will get locally connected morphisms out of the other end.

Morgan Rogers (he/him) (Apr 14 2021 at 19:11):

(It's a nice sufficient, although not necessary, condition)

Morgan Rogers (he/him) (Apr 14 2021 at 19:12):

To extract what I said from the result, just take the Grothendieck topologies to be trivial.

Morgan Rogers (he/him) (Apr 14 2021 at 19:13):

The general necessary and sufficient conditions preceding that result are a little scary-looking; @Riccardo Zanfa and I will be working to simplify them in the near future as part of our collaboration on fibrations.

Christian Williams (Apr 14 2021 at 19:15):

hm, very interesting.

Christian Williams (Apr 14 2021 at 19:15):

but this seems to be taking the left Kan extension rather than precomposition?

Morgan Rogers (he/him) (Apr 14 2021 at 19:16):

Where?

Christian Williams (Apr 14 2021 at 19:19):

we have a fibration $F:C\to D$ inducing a geometric morphism $Sh(C)\to Sh(D)$, going in the same direction

Morgan Rogers (he/him) (Apr 14 2021 at 19:19):

Also, clarifying point, are you going to presheaves or copresheaves? Based on this message it sounds like the latter?

Christian Williams (Apr 14 2021 at 19:20):

no, I mean presheaves

Morgan Rogers (he/him) (Apr 14 2021 at 19:20):

Christian Williams said:

we have a fibration $F:C\to D$ inducing a geometric morphism $Sh(C)\to Sh(D)$, going in the same direction

Yes, $F:C \to D$ induces an essential geometric morphism $\mathrm{PSh}(C) \to \mathrm{PSh}(D)$ going in the same direction; the inverse image functor is precomposition with $F^{\mathrm{op}}$.

Christian Williams (Apr 14 2021 at 19:21):

ah, yeah and the functor in that direction is right Kan extension. yeah this stuff is new and very bizarre to me

Morgan Rogers (he/him) (Apr 14 2021 at 19:22):

No problem, I'm happy to explain as much as you need!

Christian Williams (Apr 14 2021 at 19:22):

so restricting to fibrations gives us a locally connected, that's useful

Christian Williams (Apr 14 2021 at 19:23):

do you know any other ways of getting them?

Morgan Rogers (he/him) (Apr 14 2021 at 19:23):

Indeed, the thing about fibrations is that when $F$ is a fibration, $\mathrm{Lan}_{F^{\mathrm{op}}}$ is computed by taking colimits of the fibers of $F$, so you also get a much more manageable description of that functor in that situation.

Morgan Rogers (he/him) (Apr 14 2021 at 19:25):

That is, $\mathrm{Lan}_{F^{\mathrm{op}}}(X)(D) = \mathrm{colim}_{C \in F^{-1}(D)} X(C)$

Christian Williams (Apr 14 2021 at 19:26):

wait why are you talking about Lan now?

Morgan Rogers (he/him) (Apr 14 2021 at 19:26):

Christian Williams said:

do you know any other ways of getting them?

Locally connected morphisms are stable under pullback, so technically yes, but no other ways that I expect you would find useful :wink:

Morgan Rogers (he/him) (Apr 14 2021 at 19:27):

Christian Williams said:

wait why are you talking about Lan now?

Because you said "this stuff is new and very bizarre to me", I'm just trying to fill out the picture a little bit.

Morgan Rogers (he/him) (Apr 14 2021 at 19:28):

In general the left and right Kan extensions along a functor are tricky to calculate, so it's nice to know when they turn out to be nicer.

Christian Williams (Apr 14 2021 at 19:28):

oh, what's bizarre is the convention that geometric morphisms go in the direction of the right adjoint, when often that right adjoint is more mysterious than things we usually think about.

Morgan Rogers (he/him) (Apr 14 2021 at 19:29):

Blame the topologists for working with points! :wink:

Christian Williams (Apr 14 2021 at 19:29):

the right adjoint to preimage is much less obvious than the left adjoint, and it's extremely misleading when they call the right adjoint direct image because it's not.

Morgan Rogers (he/him) (Apr 14 2021 at 19:31):

That one is also the fault of geometers, but they couldn't see the whole picture when they were building this stuff, so we can't be too hard on them.

Christian Williams (Apr 14 2021 at 19:32):

huh, okay. yeah, I'm starting to study the Elephant, so I'll learn more about the background

Morgan Rogers (he/him) (Apr 14 2021 at 19:32):

Also, when $F$ is faithful, the induced geometric morphism is localic, which means that it can also be expressed as a map of internal locales in the codomain topos, and at that point the direct image is really a direct image again.

Morgan Rogers (he/him) (Apr 14 2021 at 19:33):

(it's just a direct image in a much more obscure internal sense :upside_down: )

Christian Williams (Apr 14 2021 at 19:33):

wow, okay. interesting

Christian Williams (Apr 14 2021 at 19:34):

so the functors I care about are translations between theories, say finite limits for example

Christian Williams (Apr 14 2021 at 19:34):

I wonder if restricting to fibrations might still be a large and useful class

Morgan Rogers (he/him) (Apr 14 2021 at 19:34):

Are there any constraints on translations besides preserving finite limits?

Christian Williams (Apr 14 2021 at 19:35):

well, the theories I really care about are "properly cartesian closed categories", so finite limits and cartesian closed

Christian Williams (Apr 14 2021 at 19:36):

but no other conditions besides preserving that

Christian Williams (Apr 14 2021 at 19:41):

it seems like only allowing fibrations would restrict the possible translations too much

Morgan Rogers (he/him) (Apr 14 2021 at 19:42):

Oh hey, you might not even need to restrict to fibrations! If your functors preserve finite limits, then they're also morphisms of sites (as well as comorphisms), which is to say that Lan_F will be left exact too. It's plausible that cartesian closedness will constrain the geometric morphisms enough that you'll get local connectedness, but I can't say for certain off the top of my head.

Christian Williams (Apr 14 2021 at 19:43):

I was (vaguely) wondering about that! that would be great

Christian Williams (Apr 14 2021 at 19:44):

I was focused on precomposition, so the cartesian closedness of the functor didn't help at all. but using Lan might work

Christian Williams (Apr 14 2021 at 19:44):

if it does, that would be extremely useful

Morgan Rogers (he/him) (Apr 14 2021 at 19:45):

Or it might be that you instead have that Lan_F is cartesian closed, which would be interesting in its own right, since then you might be better off considering the geometric morphisms in the opposite direction.

Christian Williams (Apr 14 2021 at 19:45):

yeah. I would be surprised if this was not already known

Mike Shulman (Apr 14 2021 at 19:46):

Christian Williams said:

the right adjoint to preimage is much less obvious than the left adjoint, and it's extremely misleading when they call the right adjoint direct image because it's not.

I would say rather than different groups of mathematicians use the phrase "direct image" for different things. Same with "pushforward".

Christian Williams (Apr 14 2021 at 19:46):

but I want/should try to do it myself

Christian Williams (Apr 14 2021 at 19:46):

ah, okay sure

Morgan Rogers (he/him) (Apr 14 2021 at 19:47):

(Lan_F may fail to be LCCC, so the geometric morphism $(Lan_F \dashv F)$ may not be locally connected, but that's up to you to find out :) )

Christian Williams (Apr 14 2021 at 19:49):

finally an approach to this problem that feels satisfying.

Christian Williams (Apr 14 2021 at 19:50):

thanks for your help

Morgan Rogers (he/him) (Apr 14 2021 at 19:51):

No problem! Good luck!

Christian Williams (Apr 15 2021 at 04:56):

so far I've tried some coend calculations and not quite seeing a strategy, so I'm following more closely the proof in The Elephant A4.1.10 : if $F:C\to D$ is cartesian then $Lan_F:[C^{op},Set]\to [D^{op},Set]$ is cartesian.

Christian Williams (Apr 15 2021 at 04:59):

Johnstone has a different way of thinking about taking left Kan extension then evaluating, as the composite
$Lan_F(-)(d) = [C^{op},Set] \xrightarrow{U^*} [(d/F)^{op},Set]\xrightarrow{colim} Set$

Christian Williams (Apr 15 2021 at 05:00):

where $U: d/F \to C$ is the $C$-projection of the comma category $d/F$.

Christian Williams (Apr 15 2021 at 05:01):

this is another way of writing $\int^c (-)c \times D(d,Fc)$

Christian Williams (Apr 15 2021 at 05:02):

this view is odd to me at first, but illuminating in how it is used.

Christian Williams (Apr 15 2021 at 05:03):

the argument is that $U^*$ is cartesian because it is a right adjoint, and $colim$ is cartesian precisely because comma categories in cartesian categories are filtered, which are exactly the colimits which commute with finite limits.

Christian Williams (Apr 15 2021 at 05:04):

it's very clever: $d/F$ is nonempty because $d\to 1\simeq F1$.

Christian Williams (Apr 15 2021 at 05:05):

for every pair of objects $\phi: d\to Fa$, $\phi':d\to Fa'$ there is a least upper bound $d\xrightarrow{\phi,\phi'} Fa\times Fa'\simeq F(a\times a')$

Christian Williams (Apr 15 2021 at 05:06):

and for every pair of morphisms $Ff, Fg: Fa\to Fa'$, an equalizer.

Christian Williams (Apr 15 2021 at 05:08):

so using a powerful result, forming filtered colimits $[(d/F)^{op},Set]\to Set$ is cartesian.

Christian Williams (Apr 15 2021 at 05:08):

then because limits in $[D^{op},Set]$ are defined pointwise, this composite being cartesian for every object $d\in D$ implies that $Lan_F:[C^{op},Set]\to [D^{op},Set]$ is cartesian.

Christian Williams (Apr 15 2021 at 05:12):

so that's really nice and that's a whole story in itself. right now I'm wondering: can this be extended to closed?

Christian Williams (Apr 15 2021 at 05:13):

Conjecture/Hope : if $F:C\to D$ is cartesian closed, then $Lan_F:[C^{op},Set]\to [D^{op},Set]$ is as well.

Christian Williams (Apr 15 2021 at 05:15):

the fact that filtered colimits commute with finite limits probably does not offer much help.

Christian Williams (Apr 15 2021 at 05:17):

my first instinct is to try to translate that proof into a coend calculation, if possible, just to get a different grasp

Christian Williams (Apr 15 2021 at 05:19):

(but I doubt it's possible, and it's not necessary.)

Christian Williams (Apr 15 2021 at 05:22):

one thing I find promising is that $U: d/F\to C$ is a fibration! so I think $U^*$ should be locally cartesian closed.

Christian Williams (Apr 15 2021 at 05:23):

then the question is whether forming colimits $[(d/F)^{op},Set]\to Set$ is cartesian closed

Christian Williams (Apr 15 2021 at 05:24):

well, $colim$ is the same as $Lan_!$, extending along $!:C\to 1$

Christian Williams (Apr 15 2021 at 05:24):

but I don't think that helps.

Christian Williams (Apr 15 2021 at 05:28):

let $P,Q:C^{op}\to Set$. then $Lan_F([P,Q])(d) \simeq \int^c P,Q\times D(d,Fc)$

Christian Williams (Apr 15 2021 at 05:29):

$\simeq \int^c C^{op},Set\times D(d,Fc)$

Christian Williams (Apr 15 2021 at 05:31):

maybe you can flip around the $C$-presheaf hom using Isbell duality?

Christian Williams (Apr 15 2021 at 05:33):

well, I guess I should recognize and use the fact that the question can be reduced to the case of $Lan_!$

Christian Williams (Apr 15 2021 at 05:33):

(and a special shape of $Lan$, at that)

Christian Williams (Apr 15 2021 at 05:35):

of course we're just asking whether the canonical map $colim([P,Q])\to [colim P, colim Q]$ is an isomorphism, for $P,Q: (d/F)^{op}\to Set$

Christian Williams (Apr 15 2021 at 05:38):

probably the time to just take a familiar presheaf category and do sanity checks

Christian Williams (Apr 15 2021 at 05:41):

okay, we can just think about graphs as a presheaf category $Gph = [\{s,t:E\to V\},Set]$

Christian Williams (Apr 15 2021 at 05:42):

what does $colim:Gph\to Set$ do?

Christian Williams (Apr 15 2021 at 05:43):

it takes a graph $s,t:E\to V$ and forms its coequalizer

Christian Williams (Apr 15 2021 at 05:44):

the graph where nodes are connected components, and edges are self-loops.

Christian Williams (Apr 15 2021 at 05:45):

does this process preserve the internal hom?

Christian Williams (Apr 15 2021 at 05:47):

$G,H = Gph(y(V)\times G, H)$

Christian Williams (Apr 15 2021 at 05:49):

so the nodes of $[G,H]$ are graph morphisms $y(V)\times G\to H$

Christian Williams (Apr 15 2021 at 05:52):

I think I need a break, to mull it over more casually

Christian Williams (Apr 15 2021 at 06:13):

so $[G,H]$ is the graph whose nodes are graph morphisms and edges are graph transformations.

Christian Williams (Apr 15 2021 at 06:13):

$colim(G)$ is the set of connected components of $G$.

Christian Williams (Apr 15 2021 at 06:14):

so : is $\pi_0[G,H]$ naturally isomorphic to $Set(\pi_0(G), \pi_0(H))$?

Christian Williams (Apr 15 2021 at 06:17):

I believe not.

Christian Williams (Apr 15 2021 at 06:24):

I can continue tomorrow. I think the distinction between graphs and reflexive graphs is important.

John Baez (Apr 15 2021 at 06:38):

I'm not sure about graphs, but for groupoids you can see $\pi_0[G,H]$ is different from $[\pi_0(G), \pi_0(H)]$. Take the circle $S^1$, i.e. the group $\mathbb{Z}$ regarded as one-object groupoid. The circle is connected so $\pi_0(S^1)$ has one element so $\mathsf{Set}(\pi_0(S^1), \pi_0(S^1))$ has one element, but you can wrap the circle around itself $n$ times for any $n \in \mathbb{Z}$ so $\pi_0([S^1,S^1])$ is a set isomorphic to $\mathbb{Z}$.

Morgan Rogers (he/him) (Apr 15 2021 at 07:53):

Christian Williams said:

this is another way of writing $\int^c (-)c \times D(d,Fc)$

I've never practiced using coends, so I actually find this the harder expression to parse :hushed:

Morgan Rogers (he/him) (Apr 15 2021 at 07:55):

Christian Williams said:

so that's really nice and that's a whole story in itself. right now I'm wondering: can this be extended to closed?

Ha, you probably shouldn't drop the "cartesian" in "cartesian closed" when dealing with geometric morphisms, there's an entirely separate notion of closed geometric morphism corresponding to the notion of a closed map.

Morgan Rogers (he/him) (Apr 15 2021 at 07:58):

Christian Williams said:

one thing I find promising is that $U: d/F\to C$ is a fibration! so I think $U^*$ should be locally cartesian closed.

Is that comment related to this, or is there some other connection between fibrations and lccc functors that I don't know about? I discovered something in this vein recently, but I have found very few mentions of the relationship between the two in the literature.

Morgan Rogers (he/him) (Apr 15 2021 at 08:05):

Christian Williams said:

of course we're just asking whether the canonical map $colim([P,Q])\to [colim P, colim Q]$ is an isomorphism, for $P,Q: (d/F)^{op}\to Set$

You shouldn't expect this to be true in general; you should be using the shape of $(d/F)^{\mathrm{op}}$. For example, the category you mentioned in defining the topos of graphs isn't filtered, so colim (which coincides with taking the set of connected components of the graph, by the way) doesn't preserve limits, so it's pretty unlikely that it's going to preserve exponentials!

Christian Williams (Apr 16 2021 at 20:20):

so right now I want to check whether forming filtered colimits, as a functor $colim:[D^{op},Set]\to Set$ where $D$ is a filtered category, preserves internal hom.

Christian Williams (Apr 16 2021 at 20:23):

we can take the category whose presheaves are reflexive graphs,
$s,t:V\to E$ and $i:E\to V$ with $is=id_V$ and $it=id_V$.

Christian Williams (Apr 16 2021 at 20:25):

wait, need to be careful about directions, thinking about the opposite category. okay.

Christian Williams (Apr 16 2021 at 20:29):

this is a filtered category, because the pair of objects has an upper bound $E$, and the pair $s,t$ has $is=it$.

Christian Williams (Apr 16 2021 at 20:31):

so taking the colimit of a graph just forms the coequalizer of the source and target morphisms - the set of connected components.

Christian Williams (Apr 16 2021 at 20:31):

for reflexive graphs, all that changes is that this is a reflexive coequalizer. does that change much?

Christian Williams (Apr 16 2021 at 20:32):

we are still asking whether $\pi_0([G,H])\simeq [\pi_0(G),\pi_0(H)]$

Christian Williams (Apr 16 2021 at 20:33):

this question is slightly less hopeless when we have self-loops.

Christian Williams (Apr 16 2021 at 20:33):

but still, it does not seem true.

John Baez (Apr 16 2021 at 21:55):

So concretely you're asking if the "connected component" functor $\pi_0$ from $\mathsf{RGraph}$ to $\mathsf{Set}$ is cartesian closed?

John Baez (Apr 16 2021 at 21:55):

I was trying to disprove this with a counterxample the other day, but I don't think I got one.

John Baez (Apr 16 2021 at 21:57):

Hmm, how about this. Let $G = H$ be the reflexive graph with two vertices v and w, an edge from v to w, and an edge from w to v (along with the two required "identity" edges).

John Baez (Apr 16 2021 at 21:58):

This graph is connected so $[\pi_0(G), \pi_0(H)]$ has just one element, right?

John Baez (Apr 16 2021 at 21:58):

On the other hand maybe $\pi_0([G,H])$ has more than one element.

John Baez (Apr 16 2021 at 21:59):

There are exactly two maps from $G$ to $H$ that map both vertices of $G$ down to one vertex of $H$, correct?

John Baez (Apr 16 2021 at 21:59):

And there are exactly two maps from $G$ to $H$ that are bijective on vertices, correct?

John Baez (Apr 16 2021 at 22:00):

So, if I'm correct, $[G,H]$ has 4 vertices, corresponding to the 4 maps I just specified.

John Baez (Apr 16 2021 at 22:01):

But I don't think $[G,H]$ has edges connecting all these 4 vertices. Am I wrong?

Christian Williams (Apr 16 2021 at 22:07):

(we're talking, and realized this is not a counterexample. in this case $[G,H]$ is connected.)

Christian Williams (Apr 16 2021 at 22:07):

but it shouldn't be too hard to find a minimal counterexample.

Christian Williams (Apr 16 2021 at 23:26):

actually, it may be true if we include a condition of finitude.

Christian Williams (Apr 16 2021 at 23:27):

I can write it up here later.

John Baez (Apr 17 2021 at 04:15):

I think there's a nice counterexample when G and H are infinite.

John Baez (Apr 17 2021 at 04:16):

Let G be the discrete graph on vertices {0,1,2,...}

John Baez (Apr 17 2021 at 04:17):

Let H be the graph that's the coproduct of graphs H(n) for n = 1,2,3,... where H(n) is the graph with vertices {0,1,2,..n} and one edge from i to i+1.

John Baez (Apr 17 2021 at 04:18):

(I'll do nonreflexive directed graphs but you can easily tweak my counterexample for reflexive graphs).

John Baez (Apr 17 2021 at 04:20):

Let f: G $\to$ H be the graph map that maps the vertex n to the vertex 0 in the subgraph H(n).

John Baez (Apr 17 2021 at 04:21):

Let g: G $\to$ H be the graph map that maps the vertex n to the vertex n in the subgraph H(n).

John Baez (Apr 17 2021 at 04:24):

Note that f and g give the same element of $[\pi_0(G) ,\pi_0(H)]$ since they map each vertex n to the nth component of H.

John Baez (Apr 17 2021 at 04:25):

However, f and g give different elements of $\pi_0([G,H])$, because there is no finite sequence of graph transformations going from f to g!

Christian Williams (Apr 17 2021 at 07:10):

this is a good counterexample. but it's unclear what's going on categorically, how this condition comes into play

Reid Barton (Apr 17 2021 at 17:09):

The colimit that defines $\pi_0$ isn't filtered. Filtered colimits are colimits over a filtered category, not the opposite of a filtered category.

Christian Williams (Apr 17 2021 at 18:49):

ah okay, I was getting mixed up. need to think of another simple example.

Reid Barton (Apr 17 2021 at 18:49):

But anyways, the conclusion that this is a finiteness issue is correct. One way to cook up a counterexample would be to take $X : D \to \mathrm{Set}$ to be the constant functor on a set $S$. Then the colimit of $X$ is also $S$ (filtered categories are connected) so the question about preserving exponentials amounts to whether the colimit functor commutes with ${-}^S$. And this is true for $S$ finite but generally false for $S$ infinite.

Christian Williams (Apr 17 2021 at 18:50):

okay, yes that makes it very clear, thanks.

Christian Williams (Apr 17 2021 at 18:51):

but if we restrict to presheaves on finite sets, it may be true.