Questions tagged [type-theory]
The type-theory tag has no usage guidance.
11
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 ...
- 1,617
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 ...
- 5,283
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 (...
- 6,257
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 ...
- 447
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 ...
- 33.9k
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 ...
- 40.2k
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". (...
- 335
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? ...
- 10.1k
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 ...
- 475
10
votes
0
answers
307
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,...
- 78.6k
3
votes
2
answers
493
views
Can we write Tangled Type Theory without reference to type sequences?
I just want to know if Tangled Type Theory $\mathsf{TTT}$ of Randall Holmes ([see: Holmes - NF is consistent, p:11, Holmes - The equivalence of NF-style set theories with “tangled” type theories; the ...
- 9,266