If Rel is enriched over suplattices what is Span enriched over?

33 Views Asked by At

In Rel the category of relations between sets you can "and", "or" and do several other operations over relations in nice ways. I don't fully get the details here but we can say the category of relations is enriched over the category of suplattices.

But if Rel is enriched over suplattices then what is Span enriched over?

So in Rel you can do the usual logical operations "and" $\wedge$, "or" $\vee$, "implication" $\rightarrow$ and quantifiers "exists" $\exists$, "forall" $\forall$. These correspond to the operations of a complete lattice. I think you want to think of Rel a enriched in the category corresponding to preserving $\exists$.

Now in Span you ought to be able to do the same operations but basically over objects instead of propositions. product $\times$, sum $+$, exponentials $\rightarrow$ and dependent sum $\Sigma$ and dependent product $\Pi$.

I'm very confused here though. I doubt it makes sense to think of Span as being enriched in some category of co-complete categories. I've read that maybe "locally presentable categories" are related to suplattices but I don't know enough to be sure here. Span as a double category enriched over locally presentable categories does kind of sound like a thing but also not like a thing I'm very sure about.

It kind of reminds me of geometric morphisms in topos stuff? I don't really get that stuff well either though.

As a small extra thing I'm sure there has to be a word for what FinRel and FinSpan are enriched over as well. Maybe there might be a classical vs constructive issue here? It doesn't make sense to do dependent sum over matrices of natural numbers to me.