Activity for user205
| Type | On... | Excerpt | Status | Date |
|---|---|---|---|---|
| Question | — |
Introducing a dependent function in the metalanguage without pi-types Consider the metalanguage where there are two forms of judgments: 1) $\text{kind}(K)$, asserting that $K$ is a kind 2) $k\in K$, asserting that $k$ is a thing of kind $K$ The family of kinds is defined as follows: 1) $\text{kind}(\text{Context})$ 2) $\text{kind}(\text{type}(\Gamma))$ for eve... (more) |
— | 7 days ago |
| Question | — |
Obtaining the semantics of simple type theory as a particular case of the set-theoretic semantics of dependent type theory There is a standard set-theoretic semantics for Martin-Löf type theory, where a context $\Gamma$ is interpreted as a set $[\![{\Gamma}]\!]$, a type $A$ in context $\Gamma$ is interpreted as a family of $[\![{\Gamma}]\!]$-indexed sets $(A\gamma){\gamma \in [\![{\Gamma}]\!]}$, a context extension $\Ga... (more) |
— | 13 days 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) |
— | about 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) |
— | about 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) |
— | about 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) |
— | about 1 year ago |