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.
started adding some actual content to categorical semantics: wrote sections defining the interpretation of
Contexts and type judgements
terms
substitution
in dependent type theory.
Prompted by discussion in another thread starting here, on the terminology of “categorical” or “categorial”, and since the latter variant wasn’t even mentioned here in this entry, I have tried my hand on a new section Terminology (here).
Please feel invited to expand/edit. I don’t feel strongly about what exactly this section says, I just feel strongly that some such a section is needed for clarification, here in this entry and especially in other entries where both terms are being used interchangeably.
1 to 2 of 2