Activity for user205
| Type | On... | Excerpt | Status | Date |
|---|---|---|---|---|
| Comment | Post #288003 |
[... cont'd] I tried looking at a simpler (for you - maybe trivial) example, viz how $\Pi$ formation rule follows in the object type theory after introducing the constant $\Pi$. I believe I can show that it follows from the three premises $\Gamma \vdash a:Type, \Gamma \vdash \Pi : (A:Type)(B:(El(A))T... (more) |
— | about 1 year ago |
| Comment | Post #288003 |
I don't understand why the term you mention at the end is well-formed. The second argument of $\lambda$ is supposed to be of type $(El(A))Type$ but $\Pi(B,A)$ is not of that type. Also, in the embedded $\lambda$, the second argument is $A$, which is not of type $(El(A))Type$ either. [to be continued.... (more) |
— | about 1 year ago |
| Comment | Post #288007 |
Thank you, now the purpose of declaring the constant $T_0$ is clear. Regarding $(A:Type)(x:El(A))El(A)$, to check my understanding, is the term $(A:Type)(x:A)A$ ill-formed in LF because it is not possible to prove that $\Gamma \vdash (x:A)A \textbf{ kind}$ for any $\Gamma$ using the derivation rules ... (more) |
— | about 1 year ago |
| Comment | Post #288005 |
Let's consider Calculus of Constructions again. In it, there isn't an infinite hierarchy of universes, there are only two universes if my understanding is correct. So I was wondering if there is any example of a term in Calculus of Constructions that wouldn't be "classified by some type"? And what is... (more) |
— | about 1 year ago |
| Comment | Post #288007 |
Oh, this makes things much clearer. (I know you partially restated what you had said in your answer, but sometimes restatements are very helpful, and this is one such case.) So essentially Luo chooses to use the symnol $El$ instead of $T_0$ when defining LF itself, and when we use LF to define other ... (more) |
— | about 1 year ago |
| Comment | Post #288005 |
I think it would be easier for me to understand the second part of your answer if we consider a small concrete example, so I asked a [separate question](https://math.codidact.com/posts/288007) about the two universes $\ast$ and $\square$ from CoC.
One question that I didn't include to my new post:... (more) |
— | about 1 year ago |
| Comment | Post #288003 |
Many thanks for such a detailed answer. I'm sure I'll be returning to it and re-reading it many times. Regarding the inference rules for pi-types in the object type theory, you say they are "encoded by having inhabitants of appropriate types that correspond to those inference rules and equations ensu... (more) |
— | about 1 year ago |