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…)
I have added pointer to
Also, I am removing this old query box discussion:
+– {: .standout} Might there be such a thing as an $n$-GAT, where a $0$-GAT is an algebraic theory and an $(n+1)$-GAT is defined as above except that the sort algebra is an $n$-GAT rather than an algebra? – Adam =–
+– {: .standout} I feel like there must be some sort of way to eliminate the notion of “arity” and put in its place an arbitrary (G)AT, recovering the original notion using the single-sorted Peano algebra (one constant “0”, one unary operation “S”, and no equations) or binary tree algebra (one constant “0”, one binary operation “B”, and no equations). But I can’t quite put my finger on how to do it. – Adam =–
1 to 6 of 6