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.
Andrew Hirsch (Apr 05 2020 at 14:58):So I'm working with something that's almost a fibred span, but the fibration is sort of "getting in the way" of the opfibration. I'm wondering if anyone has seen something like this before:
I have a programming language, fibred over contexts as normal. However, this also has a notion of trust, which we can think of as a thin category. The rule is that we can't use something owned by Alice to compute something owned by Bob unless Alice trusts Bob. This gives an opfibration over trust... almost. The problem is, there _are_ morphisms from Alice owned things to Bob owned things, but they're only due to weakening, i.e. the action of the projection morphism in the category of contexts.
It seems like this structure keeps most of the nice things about the opfibration, since we still have a functor from trust to Cat that picks out the fibres, it's just that there are more morphisms between these then we want, but those are of a very specific type.
I know that this is a pretty specific situation, but it seems like something that might have come up before, since "this is true up to weakening" is something that comes up in logic and programming languages quite a bit.