> So, a good place to try and understand underlying linguistic structure is informal mathematics, something he studied in his 1993 paper Type theory and the informal language of mathematics. This investigates both directions of the passage between formal and informal mathematics: sugaring and formalization.
Okay...
> x:A ⊢ B(x): Type
I'm lost.