3
$\begingroup$

In

Example(s) of monoidal symmetric closed category with NNO without infinite coproducts?

user Zhen Lin states the effective topos is locally cartesian closed. On nLab we have that locally cartesian closed with terminal object implies cartesian closed, and Hyland states (in his original paper on the effective topos) that there is such a terminal object and he calls it $1$ as usual. So cartesian closed implies cartesian monoidal implies symmetric monoidal. Is this line of reasoning alright? Am I missing something?

Also, since we can represent morphisms in a symmetric monoidal category as string diagrams (from Joyal and Street) does this mean we can do this for the effective topos? I would like to draw these!

If so, could someone help me there? My knowledge on all this is quite narrow and I only made this connection successfully.

Improve this question
$\endgroup$
2
  • 5
    $\begingroup$ Well, yes, toposes are cartesian closed by definition. As for string-like diagrams in symmetric monoidal closed categories, you can read what Baez and Stay say in their Rosetta Stone paper. But I'm not sure how truly useful this would be for studying the effective topos. $\endgroup$
    – Todd Trimble
    Commented Jun 24, 2019 at 20:50
  • 1
    $\begingroup$ Oh ok I didn't know that. Thank you, Todd. I have been trying to pick things up on my own as no one near me is familiar with topos theory. Thanks for the reference too. Also this idea is more along the lines of studying partial recursive functions through string diagrams, and about the feasability of the endeavor more than anything. Maybe some of what is well known of the effective topos could help. $\endgroup$
    – DV196883
    Commented Jun 24, 2019 at 21:15

0

Reset to default

You must log in to answer this question.