4

May I have a reference to why η expansion is invalid for CoC? It's not invalid. It's up to choice whether $\eta$-conversion for functions (or other types) is included. The original CoC paper seems to omit it, but as you see ATAPL includes it. I'm not certain, but $\eta$ may have been omitted from the original source because it was difficult to handle in the ...


3

They are different things. SClos is a case-split function, which is a function that pattern match on its parameter. Think of it as a lambda (if you know Haskell, you can think of it as a LambdaCase \case, which is a sugared lambda). This is definitely a canonical value in Mini-TT. The neutral value, OTOH, is an application on a case-split function, where the ...


1

IMHO universe hierarchy is particularly complicated to implement while the benefit is very small. It complicates programming in the language and the implementation of the language. The only benefit is to ensure the logical consistency. I guess that's why everybody is not writing about it. Here are some answers to your questions. I don't know much type theory ...


1

I have a shorter answer: normalization is usually used in conversion check of terms (aka definitional equality), and CoC has untyped conversion check. In conversion check, we normalize terms and compare 'em syntactically (think of it as comparing the ASTs). This probably means the normalization process doesn't have access to the types of terms, so it may not ...


Only top voted, non community-wiki answers of a minimum length are eligible