Timeline for Adjoints to inclusion pseudofunctors from topoi to Cat
Current License: CC BY-SA 4.0
14 events
when toggle format | what | by | license | comment | |
---|---|---|---|---|---|
Aug 30 at 0:40 | answer | added | Mike Shulman | timeline score: 2 | |
Aug 27 at 23:33 | comment | added | Kevin Carlson | Right, sorry about my misreading; it's actually well-known that toposes are monadic over categories and natural isomorphisms between functors. It's apparently also known that, say, cartesian closed categories are not monadic over the full 2-category of categories you're looking for and I would guess that however that works also rules this out for toposes. | |
Aug 27 at 4:21 | comment | added | Ilk | Thinking about it now, I dont think I know of any place in literature that considers general transformations of logical functors, not only isos. | |
Aug 27 at 4:15 | comment | added | Ilk | @KevinCarlson that has another issue, it uses natural isos instead of transformations, my 2-category with logical functors in question is slightly different than the one usually considered in literature, where only natural isos tend to be considered. | |
Aug 27 at 3:31 | comment | added | Kevin Carlson | It's supposedly well-known that the 2-category of toposes and logical morphisms is 2-monadic over categories, which in particular involves a left adjoint answering part of your question. For instance you can see this claimed here: ncatlab.org/nlab/show/topos I'm realizing I don't know a reference, though; Blackwell, Kelly, and Power don't get all the way there in their canonical paper on 2-monads. | |
Aug 26 at 13:20 | comment | added | Paul Taylor | I hadn't heard of Dostál's work: maybe you could add a sentence and link about it. I was thinking in terms of a type theory with powersets, for which you would build a model by interating this construction: add a new object that classifies subobjects in the given category. Osius's categorical set theory and my work built on that might help. Beware I am just guessing. | |
Aug 26 at 10:38 | comment | added | Ilk | @PaulTaylor What do you mean by the "like the von Neumann hierarchy" part? My current guess is approaching it through, Dostál's Pseudoadjoint Functor Theorem. But that form gives a recognition of a pseudoadjoint pair of pseudofunctors rather than a recognition of left/right pseudoadjoint, so it will likely need some massaging to get into the correct form. | |
Aug 26 at 9:18 | comment | added | Paul Taylor | This is a difficult question and you haven't got any answers yet, so I'll throw in some guesses to start the discussion: you may want the base 2-category to be Lex (categories with finite limits); then the free Grothdieck topos should be something like the Yoneda embedding and the free logical topos something like the von Neumann hierarchy; there probably aren't any right adjoints. | |
Aug 25 at 12:21 | history | edited | Ilk | CC BY-SA 4.0 |
fix typo
|
Aug 25 at 11:47 | history | edited | Ilk | CC BY-SA 4.0 |
clarify which bifunctors
|
Aug 25 at 8:58 | comment | added | David Roberts♦ | By bifunctor, do you mean a ncatlab.org/nlab/show/… ? | |
Aug 25 at 4:10 | history | edited | Ilk | CC BY-SA 4.0 |
switch terminology from adjoint to image when talking about geometric morphisms to be clearer
|
Aug 25 at 0:30 | history | edited | Ilk | CC BY-SA 4.0 |
added 31 characters in body
|
Aug 25 at 0:13 | history | asked | Ilk | CC BY-SA 4.0 |