Mastodawn

@jcreed Very nice post! Btw, T -> (-) and the functor U (which can be defined as T v (-)) are used in the setting of "synthetic phase distinctions", eg https://dl.acm.org/doi/pdf/10.1145/3776673.

(I have yet to find a use case for √ in this setting, but maybe this isn't surprising because I care about models with T = 0, where √ doesn't exist.)

@HarrisonGrodin thanks for the reference! Although: I would have thought T v (-) would turn A -> B into A -> B + 1 rather than A -> 1. But I did have the idea earlier (that didn't make it into the blogpost) that U(X) could be expressed as the pushout of X <- X x T -> T. Does that sound right to you? Are we starting from different assumptions somehow?

@jcreed Oh yes, that's what I mean by v - the "join" (pushout you described), not the coproduct. (I believe it's written this way because for h-props P and Q, this P v Q is still an h-prop.)

@HarrisonGrodin great, then that sounds exactly right and I agree. Btw, is it a coincidence that the notation in your paper lines up with the mathoverflow question here https://mathoverflow.net/questions/424346/internal-language-of-the-sierpi%C5%84ski-topos ? I imagine it's entirely possible if so, ∙ and ∘ are not exactly very exotic symbols, but it is an amusing coincidence in that case :)

Internal language of the Sierpiński topos

What is an internal language of the Sierpiński topos, which is defined as arising from the category $\mathsf{Set}^{\to}$, the category of arrows in $\mathsf{Set}$? Or more generally, is there a rough

MathOverflow

@HarrisonGrodin oh wow and I am getting pretty excited reading your paper here, this sounds like it might be exactly the thing I was hoping would work out

@HarrisonGrodin hmmm but now I am racing ahead to see if you have an internalization of the ?? in abs × — ⊣ ◯ ⊣ ?? ⊣ ●
...maybe this will become clear if I keep reading...

@jcreed Oops, race condition, correctly guessed you might want this on another subthread 😅 No, we don't have this, and Shulman's no-go theorem says you can't have it without additional judgemental structure. So if you care to have √, I think you have to start with that adjoint triple in cohesive type theory (or maybe just √ -| Closed in spatial type theory), and then define abs as Closed(0).

@jcreed From the perspective of AFAT, √ lets you isolate "concrete" data, which would have to be judgmentally quarantined off to preserve the noninterference property. However, the existence of √ would mean that you couldn't set abs to false, which is how we extract the efficient "concrete" code...

@HarrisonGrodin right ok that's familiar, I think, it's the thing that fundamentally requires flat-like custom judgemental machinery, yeah?

https://www.jonmsterling.com/0094/

Jon Sterling 5d ago

@jcreed @HarrisonGrodin Some further thougths about the additional adjoints that might interest you…

Lately, the ideas from this blog post seem to have led to a very interesting paper by Theocharis and Brady: https://arxiv.org/abs/2605.00655

On the relationship between QTT and STC

Jon Sterling 5d ago

@jcreed @HarrisonGrodin Regarding synthetic phase distinctions (without \sqrt), perhaps it will be helpful for me to give a little history. This stuff goes back to Bob Harper's and my attempts in early 2020 to re-understand the Harper–Mitchell–Moggi 1990 model of ML modules without an explicit phase separation. We wrote this up in "Logcial Relations as Types" (https://www.jonmsterling.com/sterling-harper-2021/), and I quickly realised that this would be useful for many more things than ML modules and parametricity.

1. "Synthetic Tait computability" for doing metatheory and other logical relations proofs. With this, @carloangiuli and I solved the normalisation conjecture for cubical type theory: https://www.jonmsterling.com/sterling-angiuli-2021/, which was expanded into my PhD thesis https://www.jonmsterling.com/sterling-2021-thesis/.
2. In the final chapter of my PhD thesis, I suggested that this language should be used as a basis for refinement types & erasure, though it was not until my linked blog post that I noticed the use of the amazing right adjoint. I am very glad that people have finally taken up this suggestion.
3. Continuing with PL applications, Bob and I did an interpretation of information flow control: https://www.jonmsterling.com/sterling-harper-2022/. Please note that while the denotational semantics is good, the adequacy proof in this paper is bogus (see errata). I believe there is another proof, but I haven't got around to it. (1/2)

Logical relations as types: proof-relevant parametricity for program modules

Jon Sterling 5d ago

4. With Yue Niu, @HarrisonGrodin, and Bob Harper, we proposed to use the synthetic phase distinction to model cost, in the "cost-aware logical framework”: https://www.jonmsterling.com/niu-sterling-grodin-harper-2022/. Harrison has led the way with many further developments in this direction, including Decalf (https://www.jonmsterling.com/grodin-niu-sterling-harper-2024/), and the Abstraction Functions as Types paper (https://arxiv.org/abs/2502.20496) which in my view really elegantly closes the loop back to LRAT in a way that greatly exceeded my expectations and imagination at the beginning of this line of work.

I don't exactly work on this stuff anymore because one does not want to be buried by one's PhD thesis. But I still find it interesting, and I do think there remains some possible untapped potential for using this structure to give simpler alternatives to existing theories in a number of areas. (2/2)

A cost-aware logical framework