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: reading & references

Topic: Existing Work on Heyting-valued Groupoids


view this post on Zulip Alyssa Renata (Aug 12 2024 at 17:48):

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?

view this post on Zulip Fernando Yamauti (Aug 12 2024 at 19:21):

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.

view this post on Zulip Alyssa Renata (Aug 12 2024 at 20:38):

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.

view this post on Zulip Morgan Rogers (he/him) (Aug 13 2024 at 09:07):

This sounds like something @Joshua Wrigley could easily answer?

view this post on Zulip Joshua Wrigley (Aug 13 2024 at 10:36):

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.

view this post on Zulip Morgan Rogers (he/him) (Aug 13 2024 at 12:42):

Sorry Josh!

view this post on Zulip Alyssa Renata (Aug 13 2024 at 15:09):

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!