I think there's perhaps an analogy to be made between FP terminology that comes from math, and is therefore unfamiliar to non-math people, and type theory notat

I think there's perhaps an analogy to be made between FP terminology that comes from math, and is therefore unfamiliar to non-math people, and type theory notation such as this. For example, an FP "functor" comes from the idea of (endo)functor from category theory, but people try to rename it (e.g. "Mappable") to make programmers understand it better. In the same way, you're proposing to rename the turnstile to an arrow symbol. The article "Why 'Functor' Doesn't Matter" [0] is relevant. In this case, the turnstile symbol comes from logic, and means "entails": Given the information on the left, you can derive the judgement on the right. There is an important distinction to be made between the turnstile and the double arrow [1]. For what it's worth, I haven't formally learned higher-level math, but I've been able to pick up type theory notation just by getting used to it. I can't necessarily explain how; it was just a gradual thing for me. [0] https://www.parsonsmatt.org/2019/08/30/why_functor_doesnt_matter.html https://www.parsonsmatt.org/2019/08/30/why_functor_doesnt_ma... [1] https://math.stackexchange.com/questions/286077/implies-rightarrow-vs-entails-models-vs-provable-vdash https://math.stackexchange.com/questions/286077/implies-righ...