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 ...


4

$\text{absurd} : (A : \text{U}) \to 0 \to A$ and $\text{elim} : (A : 0 \to \text{U}) \to (x : 0) \to A\,x$ are equivalent. To go right, use $\text{absurd}\,(A\,x)\,x$. To go left, use $\text{elim}\,(\lambda\,x.\,A)\,x$. Also, both types are propositions because of the $0$-s in domains. There's not much reason to assume or use $\text{elim}$ instead of $\text{...


3

If you intend to formalize meta-theorems in a proof assistant, then it's probably better to avoid the general weakening rule because it will pollute all your inductive arguments. Every single induction on the derivation will contain the case "but what if the context got larger using weakening?" and that's going to be super annoying. I would ...


2

It is false that the only well-typed occurrence of Prf has to be of the form Prf(all ...). For example, in the context with a variable p : Prop we can form the type Prf(p) which is not of the stated form. Another possibility is that we have a Prf(t) for some closed term t : Prop which is not of the form all ... but it normalizes to it. The purpose of Prf is ...


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