Questions tagged [type-theory]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
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 ...
MWB's user avatar
  • 1,617
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 ...
David Roberts's user avatar
  • 33.8k
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: ...
James's user avatar
  • 541
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 ...
steve's user avatar
  • 447
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 ...
StudentType's user avatar
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 ...
luqui's user avatar
  • 585
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 ...
Michael Bächtold's user avatar
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 ...
user984603's user avatar
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 ...
Christopher King's user avatar
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 ...
Kaa1el's user avatar
  • 411
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 (...
Jason Rute's user avatar
  • 6,237
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 ...
antianticamper's user avatar
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 ...
Todd Trimble's user avatar
  • 52.3k
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 ...
goblin GONE's user avatar
  • 3,693
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$...
Kaveh's user avatar
  • 5,362
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 ...
Simon Henry's user avatar
  • 39.9k
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". (...
Hexirp's user avatar
  • 335
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 ...
Tom LaGatta's user avatar
  • 8,372
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 ...
Mikhail Katz's user avatar
  • 15.1k
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 ...
Ali Caglayan's user avatar
  • 1,185
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? ...
Jonathan Beardsley's user avatar
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 ...
ಠ_ಠ's user avatar
  • 5,933
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 ...
Marcus Booster's user avatar
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 ...
Jacques Carette's user avatar
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}$...
winitzki's user avatar
  • 271
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 ...
teil's user avatar
  • 4,261
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 ...
Cory Knapp's user avatar
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$...
StudentType's user avatar
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 ...
user65526's user avatar
  • 629
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 ...
Gro-Tsen's user avatar
  • 29.8k
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". ...
YKY's user avatar
  • 508
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 ...
npq's user avatar
  • 131
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 ...
მამუკა ჯიბლაძე's user avatar
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 ...
Anthony's user avatar
  • 231
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 ...
Erwan Aaron's user avatar
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, ...
Ben Millwood's user avatar
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,...
Grisha Taroyan's user avatar
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),...
Heleyrine Brookvinth's user avatar
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 <...
Dan Arnon's user avatar
  • 121
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 ...
François G. Dorais's user avatar
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 ...
Keith's user avatar
  • 211
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 ...
Mike Battaglia's user avatar
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, ...
user avatar
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....
Bartosz Milewski's user avatar
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 ...
user347155's user avatar
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 ...
Jacques Carette's user avatar
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,...
Timothy Chow's user avatar
  • 78.1k
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)....
Philippe Gaucher's user avatar
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=%...
user2377's user avatar
  • 439

1
2 3 4 5