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 have created an entry notions of type to be included under “Related notions” in the relevant entries.
(I have managed to refrain from titling it “types of types”.)
Which notions of types are still missing in the table?
Perhaps types in model theory?
Perhaps types in model theory?
Thanks. I will have to pass this question on to someone more expert than me.
My impression was that the plain Lab entry type – stubby as it still is – is meant to subsume in particular this notion of type in model theory. If that is right, I would rather expand the entry type (which deserves to be expanded anyway) with a section along the line of that Wikipedia entry, than create a separate entry “type (in model theory)”.
But maybe I am mixed up about this. What do you (you all) think?
No, I think type is about types in type theory, which are not the same as types in model theory.
However, given the current content of notions of type, it seems that the intent is to talk about various notions of type in type theory.
So if and when anybody wants to write about types in model theory, then they should a disambiguating note to type (as well as links from articles on model theory) and write it at model-theoretic type or whatever.
1 to 5 of 5