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.
Hi, I hope this is the right stream, but I'm wondering if someone knows more about Heyting-valued groupoids, or can point me in the right direction.
There is a notion of H-valued sets whose category is equivalent to the topos of sheaves on H, where H is a complete heyting algebra. I'm wondering if there have been work on generalizing this idea to H-valued groupoids in some appropriate sense of the word. More generally, the construction of H-valued sets is generalized by the tripos-to-topos construction, and so I'm also wondering if there's any work on some sort of tripos-to-(2,1)-topos construction.
Perhaps related to this question: The (2, 1)-category of groupoids should be a (2, 1)-topos. So, it is reasonable to expect a correct notion of H-valued groupoid to also yield a (2, 1)-topos. But is there a more accessible account of (2,1)-toposes that does not require wading through infinity-toposes as in Lurie's Higher Topos Theory?
What's even an H-valued groupoid? If it's just an internal groupoid in H-sets, you will get an internal groupoid in sheaves over H. But I don't think that describes all 2-sheaves over H...
A definition making the equivalence work would be nontrivial, I think. It seems worthwhile trying to work it backwards from sheaves to H-sets and, then, try copying the procedure starting with sheaves valued in groupoids in order to get the correct definition... but I don't even remember how was the equivalence and I'm too lazy to search for it.
I suppose my question is exactly that I'm not sure what an H-valued groupoid should be formally, and was just wondering if anyone has encountered something along these lines. Thank you for the ideas though, I will try out the sheaves valued in groupoids.
This sounds like something @Joshua Wrigley could easily answer?
Morgan Rogers (he/him) said:
This sounds like something Joshua Wrigley could easily answer?
I'm not sure I can easily answer this.
Fernando Yamauti said:
What's even an H-valued groupoid?
I would agree with Fernando that answering this question would clarify what you are searching for. You seem to want a 2-topos out at the end, which for me would suggest that when generalising the tripos-to-topos construction, you should be replacing partial equivalence relations with some kernel pair groupoids. I'm not aware of any work in this direction.
Sorry Josh!
I think I am indeed quite iffy on what H-valued groupoid means, and I am working on clarifying what I mean of this notion. In any case, thanks for the perspective!