Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I’m having trouble understanding the relationship between what is described in the page generalized algebraic theory and what is in the referenced article by Cartmell.
For example, the nLab page seems to contemplate three levels of symbols—“supersort”, “sort”, and “operation”—while if I understand correctly, Cartmell’s GATs only have symbols at two levels, for sorts and operations. Also, I would only expect a GAT’s sort symbols to be applied to terms, not types as the nLab page seems to contemplate. (The nLab page speaks of “derived operations in the theory of sorts” rather than types, but I believe the same concept is intended.) My intuition is that the world of GATs in Cartmell’s sense more or less corresponds to a certain sublanguage of LF (rather than $F_\omega$), so there shouldn’t be anything like a symbol that is applied to arguments that are types and yields a type.
The author of those remarks apparently hasn’t been around for some time, so I don’t know that an explanation of that description would be forthcoming.
For what it’s worth, the “definition” generalized algebraic theory is a bit lackluster (I realise the onus is on me to do something about it, but in case anyone out there has the info at their fingertips…)
1 to 5 of 5