{"id":"arxiv/2606.03369","url":"https://arxiv.org/abs/2606.03369","tags":["cs.LO","math.CT","math.LO"],"score":0,"title":"A calculus of types in Isbell nuclei","domain":"cs.LO","source":"arxiv","authors":["Juan Luis Gastaldi","Samantha Jarvis","Thomas Seiller","John Terilla"],"reviews":0,"subject":"cs.LO","summary":"We identify two constructions from different mathematical traditions. In linear logic and realisability, logical types are generated rather than fixed in advance: one begins with a universe of realisers equipped with execution, uses orthogonality to test their interactions, and takes types to be the biorthogonally closed subsets. In enriched Isbell duality, a quantitative relation induces an adjunction whose fixed points form a category, its nucleus. These constructions proceed by different means; we show that, in the present setting, they produce the same objects. The shared datum is…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"discussed":0,"published":"2026-06-02","reactions":{}}