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/

@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

@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

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

@jonmsterling @HarrisonGrodin this historical context is great, thanks! I think the punchline that's exciting to me coming across in the recent paper is that you don't even *need* sqrt to accomplish glue and fracture. That's pretty cool. I was rabbit hole-ing in a different direction under the tacit (but unjustified!) assumption that it was needed

@jonmsterling @HarrisonGrodin ok, now my question is: is it also possible to prove internally the functoriality (or maybe the right thing to say is "faithfulness"?) of the glue/fracture equivalence? that the maps Glue(X_•, X_∘, χ) → Glue(Y_•, Y_∘, γ) are exactly the same as the pairs of maps f_• : X_• → Y_• and f_∘ : X_∘ → Y_∘ such that we get a commutative square
χ
X_• → ●X_∘
f_•↓ ↓●f_∘
Y_• → ●Y_∘
γ
?

@jcreed @HarrisonGrodin If I’m reading this right, that should be doable yes.

@jonmsterling @HarrisonGrodin nice! I was expecting/hoping it to be possible. It's pretty natural for me to imagine how you'd start the proof; like, surely you want to "extract" the f_• by hitting the Glue(X_•, X_∘, χ) → Glue(Y_•, Y_∘, γ) map with functoriality of ●, and then I guess it's obvious by the equivalence you've already shown that it gives you *some* map X_• → Y_•, so all I'm really asking is whether all the details work out nicely. I'm inclined to trust you that they do!

@jcreed @jonmsterling Yes!! This is exactly what we use in AFAT.

samir, witch in training 1d ago

jcreed 1d ago

@HarrisonGrodin @jonmsterling well this has turned out to be a great example of my favorite strategy of reading research papers, to wit
1. Do not read the research paper; in fact, refrain from being aware that it exists
2. Bang your head against the wall trying to invent something
3. Find out about the research paper, which does it way better than whatever you were trying
4. Read the research paper
5. Delight in the fact that the accomplishments of the paper make a lot of sense thanks to #2

Lindsey Kuper

@jcreed @HarrisonGrodin @jonmsterling I think that sometimes students do this and are unhappy that they're going about research "inefficiently" by "wasting" all that time on step (2), but (a) efficiency isn't all it's cracked up to be anyway, and (b) as you note, the time is in fact not wasted

jcreed 1d ago

@lindsey @HarrisonGrodin @jonmsterling yeah, strong agree!

jcreed 1d ago

@lindsey @HarrisonGrodin @jonmsterling I have to concede that it's a lot easier to have this positive attitude now that I'm "out of the game" of research --- like, there's no real professional stakes for me whether I get to publish a new idea or not --- and I do remember being a little stressed about it when I was a student, but nonetheless it *wasn't* time ill spent

Jon Sterling 1d ago

@jcreed @lindsey @HarrisonGrodin Yeah. I used to get stressed about it.

Nowadays, if I find out someone has done something satisfactorily it is kind of a relief because it means I can use it — or move on…