# Start a new discussion

## Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

## Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorKevin Watkins
• CommentTimeOct 13th 2018

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.

• CommentRowNumber2.
• CommentAuthorTodd_Trimble
• CommentTimeOct 13th 2018

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.

• CommentRowNumber3.
• CommentAuthorDavid_Corfield
• CommentTimeMar 25th 2021

One way to compare internalized/enriched categories here in a page that could use some attention.

• CommentRowNumber4.
• CommentAuthorDavid_Corfield
• CommentTimeMar 26th 2021