Questions tagged [type-theory]
The type-theory tag has no usage guidance.
201
questions
152
votes
5
answers
27k
views
What makes dependent type theory more suitable than set theory for proof assistants?
In his talk, The Future of Mathematics, Dr. Kevin Buzzard states that Lean is the only existing proof assistant suitable for formalizing all of math. In the Q&A part of the talk (at 1:00:00) he ...
58
votes
8
answers
12k
views
How true are theorems proved by Coq?
Less tongue in cheek, is it known what the relative consistency is for theorems proved with an automatic theorem prover? Of course this depends somewhat on what assumptions one makes with respect to ...
44
votes
1
answer
8k
views
Homotopy Type Theory: What is it?
My question is, broadly, what is the main project of Homotopy Type Theory (HoTT). I asked a professor who is likely to be correct and he say the following:
There are three directions:
...
38
votes
8
answers
12k
views
Good introductory book to type theory?
I don't know anything about type theory and I would like to learn it.
I'm interested to know how we can found mathematics on it.
So, I would be interested by any text about type theory whose angle ...
33
votes
3
answers
5k
views
Top-down mathematics, or "Where it all begins"
Sorry if this is off-topic.
It was my attempt to take a top-down approach to mathematics.
Being an inexperienced undergraduate (so please take my writing here lightly), I've been presented with ZFC as ...
28
votes
5
answers
3k
views
How do we construct the Gödel’s sentence in Martin-Löf type theory?
In Martin-Löf dependent type theory (MLTT), under the proposition-as-types correspondence, we sometimes say that a proposition $A$ is true if the type $A$ is inhabited. However, there is no doubt that ...
28
votes
2
answers
5k
views
What is the manner of inconsistency of Girard's paradox in Martin Lof type theory
I am aware that assigning the type of Type to be Type (rather than stratifying to a hierarchy of types) leads to an inconsistency. But does this inconsistency allow the construction of a well-typed ...
27
votes
5
answers
3k
views
Formalizations of the idea that something is a function of something else?
I'll state my questions upfront and attempt to motivate/explain them afterwards.
Q1: Is there a direct way of expressing the relation "$y$ is a function of $x$" inside set theory?
More ...
25
votes
1
answer
1k
views
Coinduction for all?
Every undergraduate in mathematics learns about proofs by mathematical induction. Moreover, every undergraduate taking a course in theoretical computer science or logic learns about inductive ...
25
votes
1
answer
2k
views
Can you have a type theory where there is type of all types?
Normally in a type theory, you can not have a type of all types, due to Girard's paradox. This is somewhat similar to how in set theory, you cannot have a set of all sets.
Therefore, usually you just ...
25
votes
0
answers
4k
views
What's the point of cubical type theory?
I have been following through the development of homotopy type theory since 2013 because I was really interested in the foundation of mathematics. The novel idea of combining programming with homotopy ...
23
votes
2
answers
2k
views
Prospects for reverse mathematics in Homotopy Type Theory
Reverse mathematics, as I mean here, is the study of which theorems/axioms can be used to prove other theorems/axioms over a weak base theory. Examples include
Subsystems of Second Order Arithmetic (...
23
votes
1
answer
4k
views
What is the most transparent, rigorous definition of the Univalence Axiom?
I've been studying homotopy type theory and trying to grasp the Univalence Axiom. I have yet to find a concise, accessible, rigorous definition of Univalence. I have several excellent survey papers ...
23
votes
3
answers
2k
views
Surreal Numbers as Inductive Type?
Prompted by James Propp's recent question about surreal numbers, I was wondering whether anyone had investigated the idea of describing surreal numbers (as ordered class) in terms of a universal ...
22
votes
3
answers
2k
views
Why would the category of sets be intuitionistic?
This question is probably really naive. And, I hope the title doesn't come off as too combative. I think that topoi of $\mathbf{Set}$-valued sheaves provide an excellent motivation for higher-order ...
21
votes
3
answers
5k
views
History of the notation for substitution
One of the very common notations for syntactic substitution is $[\ /\ ]$.
However, there seems to be an inconsistency in the literature about its usage.
Many write $[t/x]$ for "substitute $t$ for $x$...
21
votes
2
answers
1k
views
$\infty$-categorical interpretation of type theory
One can read at several places that Martin-löf type theory should be the internal language of a locally Cartesian closed infinity category, and that the univalence axiom should distinguished infinity ...
19
votes
2
answers
1k
views
Are we sure the calculus of inductive constructions and ZFC plus countably many inaccessible cardinals are equiconsistent?
This answer says,
IIRC, the calculus of inductive constructions is equi-interpretable with ZFC plus countably many inaccessibles — see Benjamin Werner's "Sets in types, types in sets". (...
18
votes
3
answers
2k
views
How do we express measurable spaces using type theory?
A measurable space $(X,\mathcal X)$ consists of a set $X$ equipped with a $\sigma$-algebra of subsets $\mathcal X$. I would like to write computer programs involving measurable spaces, but to the best ...
18
votes
2
answers
1k
views
New articles by Errett Bishop on constructive type theory?
Recently two formerly unknown articles by Errett Bishop (1928-1983) were posted online by Martín Escardó. One is entitled "A general language", deals with constructive type theory, and ...
17
votes
2
answers
1k
views
What kind of category is generated by Cubical type theory?
What kind of ‘category’ is Cubical type theory the internal language of?
Its known that Martin-Löf type theories are the internal language of Locally cartesian closed categories, adding higher ...
17
votes
1
answer
3k
views
Forcing in Homotopy Type Theory
I apologize if this question doesn't make any sense. I'll just go ahead and delete it if that's the case. But the question is just the title. Is there a notion of forcing in homotopy type theory? ...
17
votes
1
answer
1k
views
In constructive mathematics, why does the category of abelian groups fail to be abelian?
I was reading the paper Towards Constructive Homological Algebra in
Type Theory by Thierry Coquand and Arnaud Spiwack, and they state that constructively, the category of abelian groups fails to be ...
16
votes
7
answers
3k
views
What is lambda calculus related to?
So I'm not much of a math guy but I've really enjoyed programming in Lisp and have become interested in the ideas of lambda calculus which it is based.
I was wondering if anyone had a suggestion ...
16
votes
3
answers
5k
views
What is the theory of polynomials?
We all know what polynomials are, along with their elementary properties and many effective algorithms for different representations of polynomials.
The question here is more of a universal algebra ...
16
votes
2
answers
3k
views
Why is there no product type in simply typed lambda-calculus?
$\DeclareMathOperator\Pair{Pair}\DeclareMathOperator\First{First}\DeclareMathOperator\Second{Second}\DeclareMathOperator\Left{Left}\DeclareMathOperator\Right{Right}\DeclareMathOperator\Choice{Choice}$...
15
votes
4
answers
1k
views
Reference request for type theory
I am interested in learning the theory of types, especially in how they can provide a foundation to mathematics different to sets and how they can avoid self-referential paradoxes by stipulating that ...
15
votes
2
answers
2k
views
What is the status of (universal) algebra in type theory?
With the recent interest in homotopy type theory as a foundation for mathematics, it seems natural to develop algebra within the framework of type theory. So far, I can't find much literature ...
14
votes
1
answer
614
views
Why the reflection rule trivializes higher paths in Martin-Löf Extensional Type theory?
Martin-Löf Extensional Type theory differs from its intensional counterpart in that it contains the so-called reflection rule that says that if $p : x = y$, then actually $x \equiv y$ (i.e. $x$ and $y$...
14
votes
1
answer
840
views
A peculiarity of Henkin's 1950 proof of completeness for higher order logic
My question concerns Henkin's original (1950) completeness proof in Completeness in the theory of types for classical higher order logic and type theory relative to so-called general models.
His 1950 ...
14
votes
1
answer
481
views
How exactly are realizability and the Curry-Howard correspondence related?
Consider, on the one hand:
the Curry-Howard correspondence between, on the one hand, types and terms (programs) in various flavors of typed $\lambda$-calculus, and on the other, propositions and ...
13
votes
4
answers
1k
views
Two interpretations of implication in categorical logic?
I am a bit confused about the interpretation of "implication" in the standard treatment of categorical logic, for example in [Bart Jacobs 1999] "Categorical Logic and Type Theory".
...
13
votes
1
answer
632
views
What is meant by a computational interpretation of univalence?
In homotopy type theory the univalence axiom implies function extensionality.
Suppose we have a recursive set we are not sure is empty (e.g. the set of even integers$\geq 4$ that are not a sum of two ...
13
votes
3
answers
897
views
Formal/rigorous treatment of (im)predicativity/predicativism
There are several places on the web where one may find quite intuitively understandable accounts of (im)predicativity; here on MO I found two questions with very good detailed answers (Predicative ...
13
votes
2
answers
741
views
What does first-order co-intuitionistic logic look like (and does it have an equivalent type theory)?
So, this is where I'm at so far:
Heyting algebras model propositional intuitionistic logic (IL)
so do Cartesian closed categories which also model the simply typed lamda calculus
co-Heyting algebras ...
12
votes
2
answers
1k
views
What does "simplification of proofs as evaluation of programs" mean?
I am currently going through Philip Walder's "Proposition as Types" and a passage of the introduction has struck me:
for each way to simplify a proof
there is a corresponding way to evaluate a ...
12
votes
2
answers
2k
views
Connection between codata and greatest fixed points
This is, I'm afraid, another question that MSE couldn't answer.
It's easy to see how inductively-defined data types correspond to least fixed points. Let's take the natural numbers as an example, ...
12
votes
1
answer
643
views
3 questions about basics of Martin-Löf type theory
I started to read the HoTT book. I'm now on chapter 1 and I have several questions concerning not even homotopical, but "regular" type theory.
On page 24, where the universes are introduced,...
12
votes
2
answers
800
views
An overview of mathematical-logical approaches in formalizing natural languages
Crossposted on Mathematics SE
I am an undergraduate mathematics student with a keen interest in pursuing research in the formalization of natural languages (from a more mathematical-logical approach),...
12
votes
1
answer
712
views
Why does Coq restrict Inductive definitions, and how is this related to Inaccessible cardinals?
Coq lets you define an inductive type of the following form:
Inductive Foo :=
| Base : Foo
| Positive : (nat -> Foo) -> Foo.
because the position of <...
11
votes
3
answers
1k
views
Equivalent form of the Univalence Axiom
I'm reading the new HoTT book and I'm wondering about a potential equivalent form of the Univalence Axiom: $(A \simeq B) \simeq (A = B)$.
For simplicity, I'm tacitly working in a fixed universe. It ...
11
votes
4
answers
2k
views
Can dependent sums be encoded as dependent products?
Please forgive any unorthodox notation or obvious errors here... I'm trying to get an intuition for dependently typed languages, so I'm starting out by seeing which analogies I can take from the ...
10
votes
2
answers
3k
views
How can the simply typed lambda calculus be Turing-incomplete, yet stronger than second-order logic?
It is well-known that the simply typed lambda calculus is strongly normalizing (for instance, Wikipedia). Hence, it is not strong enough to be Turing-complete, as also mentioned on the Wikipedia page ...
10
votes
2
answers
2k
views
What exactly is a judgement?
Before formulating my question, let me briefly sum up what I know about the topic (feel free to correct me if something I claimed is false!). This is for you good to see what my state of knowledge is, ...
10
votes
2
answers
941
views
Dependent sum/product and the base-change functor adjunctions
In type theory, the dependent sum $\sum_{x : A} T(x)$ and the dependent product $\prod_{x:A} T(x)$ are defined by their introduction/elimination rules.
In category theory, we use a base-change functor....
10
votes
1
answer
1k
views
Why are W-types called "W"?
Why are W-types called "W"?
Probably "W" means either "wellordered" or "wellfounded". (Martin-Löf uses the term "wellorder".) But these are notions ...
10
votes
2
answers
772
views
Category of Judgements?
I have been able to find a lot of information on the category of contexts -- for example, the page on syntactic categories at the nLab is a good starting point. However, when I try to find similar ...
10
votes
0
answers
305
views
Feferman's universes for proof assistants?
This question was prompted by a discussion from another MO question about the consistency of ZFC. There are some mathematicians who are comfortable with ZFC but uneasy with large cardinals. For them,...
9
votes
2
answers
2k
views
A (very naive) question about Homotopy Type Theory
In homotopy type theory, homotopy types can be viewed as logical types and it is possible to prove some theorems about them without using any underlying space (no simplicial set, no topological space)....
9
votes
3
answers
700
views
What is the definition of computational content?
I am interested in type theory and proof theory. I have read a lot of papers and books that use the term "computational content" (For example: https://scholar.google.com/scholar?hl=en&q=%...