Activity for user205
| Type | On... | Excerpt | Status | Date |
|---|---|---|---|---|
| Edit | Post #291817 |
Post edited: |
— | 6 months ago |
| Edit | Post #291817 | Initial revision | — | 6 months ago |
| Question | — |
Interpreting $\text{Prop}$ in Set Consider a type theory with a universe $\text{Prop}$ of logical propositions (for now, it is not necessarily impredicative). Write $\text{T}$ for the decoding function for this universe. If we stipulate proof irrelevance (i.e., say that for any $P:\text{Prop}$ and any two terms $a,b:\text{T}(P)$, ... (more) |
— | 6 months ago |
| Edit | Post #288016 |
Post edited: |
— | over 1 year ago |
| Edit | Post #288016 |
Post edited: |
— | over 1 year ago |
| Edit | Post #288016 |
Post edited: |
— | over 1 year ago |
| Edit | Post #288016 | Initial revision | — | over 1 year ago |
| Question | — |
Considering the "type" $\Pi x:A.\Pi y:B(x).Type$ I'm still trying to wrap my head around introducing type theories by means of LF. Suppose I declare the following constants: $A:Type, \\ B:(El(A))Type$ and the necessary constants for the pi-type. And suppose I want to consider (in the object type theory) a family of types which depends on $x:A$ a... (more) |
— | over 1 year ago |
| 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) |
— | over 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) |
— | over 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) |
— | over 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) |
— | over 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) |
— | over 1 year ago |
| Edit | Post #288007 |
Post edited: |
— | over 1 year ago |
| Edit | Post #288007 |
Post edited: |
— | over 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) |
— | over 1 year ago |
| Edit | Post #288007 |
Post edited: |
— | over 1 year ago |
| Edit | Post #288007 | Initial revision | — | over 1 year ago |
| Question | — |
Defining the two universes from Calculus of Constructions in LF Consider LF, the logical framework used to define UTT (unified theory of dependent types). The next two quotes are from here. >LF is a simple type system with terms of the following forms: >$$\textbf {Type}, El(A), (x:K)K', [x:K]k', f(k),$$ >where the free occurences of variable $x$ in $K'$ ... (more) |
— | over 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) |
— | over 1 year ago |
| Edit | Post #287995 |
Post edited: |
— | over 1 year ago |
| Edit | Post #287995 | Initial revision | — | over 1 year ago |
| Question | — |
On Tarski-style universes in type theory I'm looking at this note about universes in type theory. For Tarski-style universes (page 2), as far as I understand, the "$a$" in $a:Ui$ are formal names of types, whereas the "$Ti(a)$" in $Ti(a) \ type$ are actual types. What I don't understand is the purpose of "$ui:U{i+1}$" and "$T{i+1}(ui)=Ui... (more) |
— | over 1 year ago |
| Edit | Post #287991 |
Post edited: |
— | over 1 year ago |
| Edit | Post #287991 |
Post edited: |
— | over 1 year ago |
| Edit | Post #287991 | Initial revision | — | over 1 year ago |
| Question | — |
The purpose of logical frameworks in specifying type theories I'm trying to understand the notion of a logical framework and how/why/when it's used to define type theories. I'm looking at Luo's "Computation and Reasoning" (1994), where he considers "LF, a typed version of Martin-Lof's logical framework". >LF is a simple type system with terms of the followin... (more) |
— | over 1 year ago |