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: learning: questions

Topic: Examples of interpreting internal logic in Psh(C)

Yiming Xu (Jun 02 2025 at 12:05):

My question is: Is there any interesting example of unfolding the definition of the semantics of internal logic, to obtain an interesting fact about presheaf categories? It is possible to randomly write down a geometric formula, and interpret it what it means in a trivial presheaf, say $\text{Psh}(2)$ where $2$ looks like $\cdot \to \cdot$. But I am searching for some rather interesting ones.

My question is pretty relevant to this old MSE post, asking about an example of proving an interesting fact using internal logic.

https://math.stackexchange.com/questions/394194/what-does-a-proof-in-an-internal-logic-actually-look-like?noredirect=1&lq=1

There are answers in some sheaf categories, but no one is in a presheaf category. As presheaf categories are simpler, I have the hope of getting an example there. Hints would also be greatly appreciated!