Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
More propositions and stuff entered at bicategory of relations.
Started trying to finish off the proof that a bicategory of relations is the same thing as a unitary pre-tabular allegory. What I’ve put there is pretty vague for now; I think the basic idea is solid, but it needs a bit more work.
Thanks! I don’t have time to read this over right now (though I’m looking forward to it later) but I just wanted to point out that we do have cartesian bicategory spelled in lowercase. I added a redirect for the capitalized version.
OK, I’m pretty happy with this now. See what you think.
It might be nice to summarize the long calculation in terms of things like string diagrams. (But I’d have to think about what I mean by that, exactly, since there is an obvious objection here that this would be circular.)
I agree, it’s not very pretty, but of course string diagrams only make sense if the tensor is functorial. If you like I could draw out the diagrams I used and upload them – I don’t have a scanner, but maybe a photograph of the page would do.
That might help! Thanks.
When you say “string diagrams only make sense if the tensor is functorial” I presume you’re referring to string diagrams for a monoidal (bi)category. But mightn’t there be some other kind of string diagram that would work here? It seems like the string diagrams here would need to talk about local finite products rather than the tensor, anyway.
@Todd: I’ve uploaded a PDF to my personal web instead: here. Sorry about the delay — I found a tiny mistake that meant I had to throw out and re-prove a bunch of stuff.
@Mike: Not the way I did it, no. The difficult bits don’t stay in a single hom set, as you can see in the PDF. But of course I may just have done it in an over-complicated way.
Couldn’t we prove this in a slicker way like this? Any unital pretabular allegory embeds into a unital tabular allegory by splitting its coreflexives. But every unital tabular allegory is the allegory of relations in a regular category, which we know is a bicategory of relations, and any full sub-bicategory of a bicategory of relations that’s closed under the tensor product (both binary and nullary) is again such.
Oh, yes, good idea. That’s much simpler. I might end up using that instead (with credit, of course).
Edit: OK, I’ve changed bicategory of relations accordingly. Much nicer.
It’s at least simpler if we assume as known the properties of splitting coreflexives in allegories, and the equivalence of unital tabular allegories with regular categories. It’s not clear to me that those proofs, written out in full, are any shorter than your direct proof — but perhaps this way is more intuitive.
Although I have to admit I feel a little dirty whenever I prove anything by invoking an embedding theorem….
That’s a fair point, but your way is definitely more intuitive and ’structural’ generally. As for using an embedding theorem, it does feel a bit like cheating, doesn’t it? But then it’s hardly any different to, say, proving things about real numbers using complex analysis, or hyperreals. In fact, the basic argument in the original direct proof is essentially the same as the one in the proof that is a bicategory of relations. So if we unwound or ’beta-reduced’ the slick proof far enough, we’d probably arrive at something quite like the direct one.
A good point.
It’s striking how much I find myself thinking about “beta-reducing” proofs, now that I’ve more or less internalized proofs-as-programs. I wonder whether it’s something I did as much before but just without having a name for it.
1 to 16 of 16