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.
715
questions
0
votes
0
answers
35
views
Type theory reference including applications to multiple computer languages
I'm wondering if anyone could recommend me a good text on the application of type theory to computer languages (plural).
What I'm looking for:
Discusses formal theory in moderately-rigorous terms
...
- 1,378
18
votes
2
answers
1k
views
What concretely does it mean to "do mathematics in a topos X"?
I don't know if this is the right kind of question, but I've heard people say this phrase "do mathematics in a topos", and the idea that Set is the topos people usually work in, but only one ...
- 13.4k
1
vote
0
answers
40
views
Is this restricted variant of predicate logic decidable, but expressive enough to be encoded by STLC ($\lambda \to$)?
As in the question, is it the case that a predicate calculus with these properties is decidable?
n-ary predicates
quantifiers
finite domain of discourse
impredicativity disallowed
no function terms
...
- 157
2
votes
0
answers
64
views
The continuum hypothesis in non-set theoretic foundations
I understand the continuum hypothesis and the fact that it's independent of ZFC, but what about other foundations of math? For example, what does it look like in a type theoretic foundation? Is it ...
- 275
4
votes
1
answer
153
views
How does type theory deal with the lack of completeness, compactness, etc.?
As far as I understand, type theory (let's say Simple Type Theory or one of its extensions such as Homotopy Type Theory) is a computational view of $\omega$th-order logic.
See this question: Type ...
user1345451
2
votes
1
answer
133
views
Definite description in homotopy type theory
I asked this question there and I have been suggested to ask it here.
In a paper by David Corfield, we have an account of definite description in homotopy type theory. The author gives the following ...
- 308
0
votes
0
answers
47
views
What is the model of a group (from Group Theory) from the perspective of Type Theory?
Given that a group is a set with a binary operation, how would you define a group in Type Theory?
I am starting with code sort of like this:
...
- 3,773
0
votes
1
answer
44
views
Internal vs External in type theory
I'm learning type theory, and at one point in the HoTT book, is mentionned "external" constructions. I was wondering what precisely means internal/external in type thoery.
- 395
0
votes
1
answer
45
views
HoTT universes (is it an axiom ?)
I just began to learn type theory and read HoTT.
In the book, it is said in chapter I that type theory presented here has no axioms and rather only rules. But a few pages later, cumulative universes ...
- 395
1
vote
1
answer
55
views
Morphism between product types as a product of diagonal maps
I am trying to follow this post
https://ncatlab.org/toddtrimble/show/Notes+on+predicate+logic
and I got confused on this paragraph:
From this point of view, a morphism between product types is a ...
- 4,223
6
votes
1
answer
92
views
Category of Sets vs Category of Types (& Yoneda Lemma)
I've been wondering for a while why we discuss the category of sets, $\mathbf{Set}$, all the time, but hardly discuss something like the category of all types and functions between them ($\mathbf{Type}...
- 73
1
vote
0
answers
92
views
What is the proof that Term Finding in Calculus of Constructions ($\lambda{C}$) is undecidable?
It is mentioned in a textbook "Type Theory and Formal Proof: An Introduction", but couldn't find the paper or proof anywhere on the internet.
To quote the textbook:
The question of Term ...
- 157
-1
votes
2
answers
165
views
What is a "type" in type theory?
Types are taken as atomic in type theories like homotopy type theory. But what is the best way to conceptualize what a type is? Is it appropriate to think of them as a property that defines a category?...
- 101
0
votes
1
answer
128
views
Category Theory built on Type Theories, Category theory as foundations
There are two questions I have, one quick and one probably long.
I am trying to investigate applications of category theory and I ran across “the category of types” in computer science.
Now, as I ...
5
votes
1
answer
191
views
Type theory vs "Theory On Top of Logic" mantra in Set Theories
I have a question about (especially second part of) following statement following statement from wikipedia emphasizing intrinsical feature in which type theory substantially differs from set theories:
...
- 7,499