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.
Created a stubby poset-valued set.
Looks like a comma double category from $F$ to $P$. Objects are functions $F A \to P$ and horizontal morphisms are squares from some $F R : F A \nrightarrow F B$ to $\leq_P$ along those functions. Then you should have vertical arrows which are of the form $F f$ and make a commutative triangle and some kind of squares. I’m not very familiar with models of linear logic though so I don’t know if those notion already has a name for coherence spaces.
That was exactly my thought on reading it!! There ought to be a general theory of when comma double categories inherit structure from their inputs. Comma double categories have also been used recently to induce structure on decorated cospans, and I believe that some forms of the Dialectica construction can also be represented as comma double categories. However, I don’t have time to think about this any more right now.
Just found mention of “$H$-valued sets” on the tripos page. Are they the same? They look very similar.
They do look somewhat similar, but I don’t think they’re the same. There are no symmetry or transitivity requirements, and the morphisms between them are different.
1 to 5 of 5