## Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

## Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorMike Shulman
• CommentTimeDec 19th 2017

Created a stubby poset-valued set.

• CommentRowNumber2.
• CommentAuthormaxsnew
• CommentTimeDec 19th 2017
• (edited Dec 19th 2017)

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.

• CommentRowNumber3.
• CommentAuthorMike Shulman
• CommentTimeDec 19th 2017

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.

• CommentRowNumber4.
• CommentAuthormaxsnew
• CommentTimeFeb 9th 2018

Just found mention of “$H$-valued sets” on the tripos page. Are they the same? They look very similar.

• CommentRowNumber5.
• CommentAuthorMike Shulman
• CommentTimeFeb 10th 2018

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.