Questions tagged [type-theory]
For questions about type theory, including normalization, dependent types, identity types, inductive types, universe types, functional programming languages, proofs as programs in simply-typed lambda-calculi, Martin-Löf's intuitionistic type theory or related.Consider using one of the following tags: (lambda-calculus), (logic), (constructive-mathematics),(homotopy-type-theory) if related.
655
questions
11
votes
3
answers
723
views
Approaching Type theory and Category Theory as a starting point in the study of mathematics?
I'm a Computer Engineering student, with interest in Type Theory and Category Theory and i have a more pedagogical/philosophical question about these areas.
It seems that many researchers in Type ...
- 119
1
vote
1
answer
47
views
Typed logic vs many-sorted logic
I am confused as to what is the difference between many-sorted logic and typed logic.
Are they the same thing? If not, what are the differences?
- 82
0
votes
0
answers
78
views
Textbook of logic and sets based on type theory [closed]
Are there any textbooks on logic and sets at the level of prior knowledge to calculus that are based on type theory?
- 82
1
vote
0
answers
27
views
Specifying Calculus of Constructions (or something similar) 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 {...
- 223
1
vote
1
answer
45
views
Establishing $\Gamma, A: Type \vdash (A)Type\ \textbf{kind}$ in LF
This is a follow-up to my previous question. Consider the same LF as in that question:
LF is a simple type system with terms of the following forms:
$$\textbf {Type}, El(A), (x:K)K', [x:K]k', f(k),$$
...
- 223
2
votes
1
answer
91
views
Why use LF to define 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, ...
- 223
0
votes
0
answers
35
views
How do I define a notion of infinite coproducts for objects in a category?
As part of a project I'm working on; I am writing an interpreter for the STLC (simply typed $\lambda$-calculus) in which the type-checking algorithm treats isomorphic types as "equal".
I ...
6
votes
1
answer
188
views
Gödel on the “True Reason” for Incompleteness
In footnote 48a of his famous paper on incompleteness, Gödel writes:
[T]he true reason for the incompleteness inherent in all formal systems of mathematics is that the formation of ever higher types ...
- 113
0
votes
1
answer
57
views
Forcing $\pi_1(\tilde f(a))=f(a)$ for an object of a sigma type
Suppose I have an object $f$ of type $\Pi x:A.B(x)$, and consider a new type $\Pi (x:A).\Sigma (t:B(x)).C(t)$. If $\tilde f$ is an object of the second type and $a:A$, then $\pi_1(\tilde f (a)):B(x)$, ...
- 223
2
votes
1
answer
51
views
On iterated sigma type
Just to make sure I understand the notation in the excerpt below (from Corfield's "Modal Homotopy Type Theory") correctly, is the "sum" over $x:Activity, y:Achievement$" the ...
- 223
1
vote
2
answers
51
views
What is the point of "typal" computation rules?
The (recently created) page titled integers type on ncatlab.org, in the section "As the inductive type generated by an element and an equivalence of types", gives two different forms of the ...
- 167
1
vote
0
answers
35
views
How does one prove that constructive type theory is isomorphism-invariant?
In his paper Structuralism, Invariance and Univalence (pdf), Steve Awodey makes the following claim about constructive type theory:
The system of type theory has the important property that any ...
3
votes
2
answers
155
views
Unnested universes in type theory
All sources I looked at only talk about a nested family of universes $U_0 : U_1:U_2: \dots$ (for example, the HoTT book, or Notes on Universes in Type Theory, or this answer). If one has two (or more) ...
- 223
1
vote
1
answer
28
views
univalence and indiscernibility
Given $A, B: U$ (where $U$ is a universe), define $\mathsf{Indis}(A, B)$ to be $\prod_{Q: U \rightarrow U} Q(A) \leftrightarrow Q(B)$. (This just says that $A$ and $B$ are in a certain sense ...
- 607
1
vote
0
answers
19
views
Is there a name for the exponential semiring of G-sets?
Is there a name for the exponential semiring of G-sets?
In an ordinary type system, the types are like sets.
It's possible to extend this analogy and get a $G$-type system where every type is acted on ...
- 9,298
0
votes
0
answers
23
views
Accounting for dynamicity in type theory
Is there a type-theoretic way to express dynamicity? For example, if I want to account for inferences such as "John ate the apple" $\implies $ "The apple doesn't exist (anymore)" (...
- 223
1
vote
1
answer
51
views
understanding $\Pi$- and $\Sigma$-types via arithmetic interpretation
I'm trying to understand $\Sigma$- and $\Pi$- types in dependent type theory. On the bottom of page 9 of this document, there are two equations giving a justification for the names of $\Pi$- and $\...
- 321
1
vote
1
answer
43
views
sum types in MLTT without universes
Suppose that $X$ and $Y$ are types that do not depend on anything else. Let $i$ be the usual function of type $X \rightarrow X+Y$ and $j$ be the usual function of type $Y \rightarrow X+Y$ discussed in ...
- 607
2
votes
0
answers
87
views
getting new results with universes
One remarkable thing about introducing a universe U (or many universes) into Martin-Lof Type Theory is that it allows us to show that certain types are inhabited that we would not otherwise be able to ...
- 607
1
vote
2
answers
69
views
Prerequisites for understanding Type Theory
I am a computer scientist, and I am currently trying to understand the basis of programming languages (e.g. Haskell and Coq) in the mathematical foundations. I started by reading Types and Programming ...
- 111
2
votes
1
answer
64
views
An application of path induction
Does the rule of path induction (based or unbased, I don't care) allow us to infer
$$u:A, \ v:A, \ p:u=_A v \vdash t: p = \mbox{refl}(u) \hskip 1 cm (*)$$
for some term $t$? It seems to me that this ...
- 607
1
vote
0
answers
57
views
How do we establish the correspondence between the Krivine machine and classical logic?
In this paper, Krivine describes his machine and maps it to classical logic (he implements something like call/cc at the end).
Only, I have trouble understanding how he establishes this correspondence ...
- 11
-1
votes
1
answer
69
views
Tetration of Church numerals? [closed]
I haven't seen any examples of tetration of Church numerals, so I was trying to do it myself. Tetration is iterated exponention, for example: $2 \uparrow\uparrow 3={2^{2}}^{2}$. Unfortunately, I haven'...
- 1,374
0
votes
0
answers
35
views
Subterms of a lambda application?
In a book on Type theory I am working through, there is a definition for subterms where the third case covers lambda abstractions and is given by
$$Sub((\lambda x. M)) = Sub(M) \cup \{(\lambda x. M)\}$...
- 1,374
-2
votes
1
answer
49
views
What are some important results of type theory?
It would be great to have an overview of some of the most important results in type theory.
What are in your opinion some of the most important results/widely applicable results in type theory ...
0
votes
1
answer
34
views
defintional equality types
If $a$ and $b$ are definitionally equal terms of type $A$ - i.e., $a$ and $b$ can be $\beta \eta$ reduced to identical terms - what follows about the structure of the identity type $a=_A b$? For ...
- 607
0
votes
1
answer
79
views
What is variable substitution best thought of categorically? A natural transformation?
Here is an attempted proof in the category $\textbf{Ass}$ where objects are assertions (in a kind of ordered-and or CNF form - essentially a list of assertions) and morphisms are "proofs" ...
- 19.8k
1
vote
0
answers
87
views
Resources about Constructive "Extreme" Substructural Logics
Substructural logics can be obtained by dropping different structural rules, most commonly contraction, weakening, exchange. Effects of not having these rules have been studied widely in literature, ...
- 11
0
votes
1
answer
48
views
Confusion about dependent function type
Here's how dependent functions are introduced, according to the HoTT book:
To define $f: \prod_{x:A} B(x)$, where $f$ is the name of a dependent
function to be defined, we need an expression $\Phi: B(...
- 19
0
votes
0
answers
34
views
What do you call a function that maps within a type (or: space)
This question came up when I was trying to comment some code, but I think the language I'm looking for comes from category theory.
Suppose I have f: X -> X, ...
- 11
0
votes
1
answer
78
views
Why is $p$ a proof of $A$?
How do I see that "the logical proposition $A$ in (3) can be proved by the term $p$ in (4)"? What does it even mean that the term $p$ proves $A$ ?
(Source of the screenshot: https://www.cs....
- 19
5
votes
1
answer
57
views
Need help understanding $\alpha$-equivalence.
I am currently reading through Type Theory and Formal Proof.
I see that there is some variation in the literature in the fine details on the discussion on how $\alpha$-equivalence is developed, such ...
- 1,041
0
votes
0
answers
36
views
Universe CN and interpretation of "some"
From https://www.wiley.com/en-us/Formal+Semantics+in+Modern+Type+Theories-p-9781119489214 (pages 35-36):
[...] CN is the universe of all (interpretations of) common nouns. As
such, CN is the type ...
- 19
0
votes
0
answers
44
views
Notational questions about rules in type theory
Definition of contexts from here. The first rule says that the empty tuple (or sequence) is a context. The second and third ones I don't exactly understand.
I think the second has the premise "if ...
- 19
1
vote
1
answer
122
views
Proving that W-algebra homomorphisms are contractible
I don't understand the conclusion of the proof of Theorem 5.4.7 of the Homotopy Type Theory text and would like a more detailed explanation of how it works. Here's my attempt at divining an answer.
...
- 45
1
vote
1
answer
119
views
Category theory and types..?
I am reading "A Gentle Introduction to Category Theory - The calculational approach" , Marten M. Fokkinga.
In the book often a word mentioned is of "typing" and if an expressio ...
- 9,988
0
votes
1
answer
43
views
Foundations for learning LEAN
I am interested in learning LEAN. Visiting some forums and archives it seems that this uses type theory. Specifically, the "calculus of inductive constructions" is mentioned.
I have ...
- 1,060
5
votes
1
answer
162
views
If a type is an object and a function is a morphism. How to interpret a value in programming?
I've been reading Bartoz's "Category Theory for Programmers", and one question came to mind. In programming, types are objects and functions are morphisms. A functor is then a way to ...
- 2,752
4
votes
1
answer
170
views
The first-order metatheory of HoTT
Does there exist a (say, simply typed) first-order theory which axiomatizes a universe of $\infty$-groupoids, in a similar manner to how ZFC can be considered as an axiomatization of the universe of ...
- 41
0
votes
1
answer
77
views
Axiom of Choice in Intuitionistic Type Theory
I read that in Intuitionistic Type Theory the Axiom of Choice is a theorem that can be stated as:
$(\forall x \in A) (\exists y \in B(x)) C(x,y) \supset (\exists f \in (\Pi x \in A) B(x)) (\forall x \...
- 205
4
votes
0
answers
153
views
Reference for basic metatheory of Martin-Löf type theory
Section A.4 of the HoTT book states that the metatheoretic properties of Martin-Löf type theory (such as normalization and canonicity properties) can be proved using “standard techniques from type ...
- 363
0
votes
1
answer
42
views
Proof of $~FV \left(\lambda xyz ~.~xxy \right)=\emptyset $
I want to prove that $~ \lambda xyz ~.~xxy ~$ is a closed $\lambda$-term $~ \mathit{i.e.}~ FV \left(\lambda xyz ~.~xxy \right)=\emptyset ~$
The followings is my try.
$$\begin{align}
\lambda xyz ~.~...
- 1,489
2
votes
3
answers
106
views
Do Hindley-Milner theories have a Deduction Theorem?
Deduction Theorem: Given $\Gamma \cup \{A\} \vdash B$, we can deduce $\Gamma \vdash A \to B$
HM Counter-Example (?):
Take $A$ to be $\forall f : \alpha \to \alpha, \forall x : \alpha, f(x) = f(f(f(x)))...
- 151
2
votes
1
answer
72
views
Understanding recursion over higher order types
I'm reading this answer which defines Ackermann function via higher order recursion https://mathoverflow.net/a/47098
First we define an iteration function $g\colon\mathbb{N}\times\mathbb{N^N}\to\...
- 23
1
vote
1
answer
106
views
Do logical connectives in type theory not form well-formed formulas like they do in classical logic?
I have been doing exercises in Lean theorem prover where I was introduced to type theory.
There is a variety of type theories, this question applies to those that behave similarly to Lean's dependent ...
- 33
0
votes
0
answers
103
views
Sequent calculus as multilinear/tensor algebra?
Settings
I have been studying sequent calculus for several months and found that there should be a rule that is seemingly typical, even too trivial, but/hence no one officially mentions:
$$
\dfrac{
a ...
- 9
1
vote
0
answers
55
views
Why do type constructors automatically yield parametrised construction?
It does often seem to be the case that the unparametrised version of a concept in category theory is not as useful as the parametrised version. This is especially the case when categories are ...
- 3,206
2
votes
1
answer
118
views
What is an intensional type theory and what is a simple example of one?
What is an intensional type theory and what is a simple example of one?
I'm interested in understanding the sentence below in the prehistory section of the Wikipedia article on Homotopy Type Theory.
...
- 9,298
3
votes
1
answer
98
views
What are canonical injections in Martin Lof type theory
In the following paragraph from Martin Lof's 1972 paper...
If $A$ and $B$ are types, then so is there disjoint union $A + B$, which is the type of objects of form $i(a)$ with $a:A$ or $j(b)$ with $b:...
- 355
0
votes
0
answers
40
views
Type theory: A path from CC to UTT
I'm hoping for a book that will bring me up to speed with the Universal Theory of Dependent Types (UTT) as used in Agda. My current knowledge of the field is the Calculus of Constructions (CC), from ...
- 355