Skip to main content
37 votes
Accepted

What is predicativity?

Impredicativity is one of those soft concepts that appears in many related forms, but it is difficult to explain what precisely they share. Let me try anyhow. Impredicativity allows us to single out, ...
Andrej Bauer's user avatar
  • 9,553
30 votes
Accepted

What set-theoretic definitions can't easily be formalized in a type theory?

Almost no pen-and-paper mathematics is written in ZFC. The vast majority of mathematical texts is actually written in something that resembles structural set theory and is closer to type theory than ...
Andrej Bauer's user avatar
  • 9,553
24 votes
Accepted

Why should you "never resort to polymorphism when initiality would do"?

Initiality comes with a powerful universal property which allows you to, internally, prove statements about the constructions you perform. If you give me an element of ...
gallais's user avatar
  • 1,256
22 votes

What are the differences between MLTT and CIC?

I do not think I would align typed conversion with CiC versus MLTT. From my perspective, the move from untyped to typed conversion is simply an example of technology improving over time. While it ...
Neel Krishnaswami's user avatar
20 votes
Accepted

So many data types, so little time

I find my mathematics and programming background do not endow me with much understanding of type theory as it pertains to proof assistants. So many data types, so little time Oregon Programming ...
Guy Coder's user avatar
  • 2,846
18 votes

What are the differences between MLTT and CIC?

The short answer is: $\mathbf{MLTT}$ relies on $\Pi$, $\Sigma$, $\mathbf{Id}$, $\mathbf{0}$, $\mathbf{1}$, $\mathbf{2}$, $\mathbf{W}$, and $\mathbf{CiC}$ relies on $\Pi$, $\Sigma$, $\mathbf{Id}$, ...
Namdak Tönpa's user avatar
18 votes
Accepted

Tools for checking the consistency of a type theory

One can think of type theory as an algebraic theory on steroids (there is technical merit to this claim). Every algebraic theory has a model, namely the trivial one whose carrier is the singleton. A ...
Andrej Bauer's user avatar
  • 9,553
17 votes
Accepted

What are the motivations for different variants of categorical models of dependent type?

I would divide these models into three general groups. Structures that are more "categorical", arising naturally from categories "in nature" without the need for strictification ...
Mike Shulman's user avatar
  • 3,180
16 votes

How to represent mathematical partial functions in a type-theory based proof assistant?

Another possibility would be to take the result of division to lie in 1-dimensional projective space over Q. Since Q has ...
Mike Shulman's user avatar
  • 3,180
16 votes

Can mathematical formalizations in NuPRL be trusted as correct in the greater mathematical practice?

As an author of this paper, I think I would write it a little bit differently if I had the chance today. Before I begin, let me echo Andrej's comment that Nuprl is a very significant moment in the ...
Jonathan Sterling's user avatar
15 votes

Bringing OOP features into proof assistants?

Object oriented programming cannot easily be integrated into proof assistants, because object types are naturally mixed-variance. For example, a Java interface like: ...
Neel Krishnaswami's user avatar
15 votes
Accepted

Bringing OOP features into proof assistants?

Semantics The main OOP investigation and modeling in second order type theory was done by Luca Cardelli and Martin Abadi, e.g. in Theory of Objects and later was continued by Anton Setzer in Object-...
Namdak Tönpa's user avatar
15 votes
Accepted

What axioms have a computational interpretation?

This is a very broad question. Actually, it is even a whole research area, which is a major theme of what I would call the French school of type theory. Extending the Curry-Howard isomorphism from &...
Pierre-Marie Pédrot's user avatar
14 votes
Accepted

What is the difference between judgmental equality, definitional equality, and equality types?

This answer to this question about η-equivalence in Coq draws a distinction between judgmental equality and definitional equality. This is an incorrect attribute to the answer you linked to. Sarah ...
ice1000's user avatar
  • 6,256
14 votes
Accepted

Can mathematical formalizations in NuPRL be trusted as correct in the greater mathematical practice?

At least one of the authors of the paper is around so they can speak for themselves what they meant. I can comment on what they wrote, but let me make a disclaimer first, lest someone misunderstand me:...
Andrej Bauer's user avatar
  • 9,553
14 votes
Accepted

What are "fibration/cofibration" in type theory and what are their intuitions?

So, first, the origin of this term in the context of cubical type theory comes from its intended semantics, which are in turn inspired by the model-categorical semantics of homotopy type theory. Let's ...
daniel gratzer's user avatar
13 votes

In what intensional type theories can absurdity be made definitionally proof irrelevant?

If you are happy to have your False live in a separate sort, then you can do this with strict propositions in Coq (and any other system that have those, which I ...
Meven Lennon-Bertrand's user avatar
12 votes

What are the differences between MLTT and CIC?

The technical answers are correct, but they completely overlook the philosophical differences between the two formalisms. Martin-Löf type theory closely reflects Arendt Heyting's explanations of the ...
Lawrence Paulson's user avatar
12 votes

Can the development of proof assistants make mathematicians switch their framework?

The following is a made up opinion piece based on the observation of a statistically small sample of mathematicians. Please take it with a grain of salt. A typical working mathematician has little ...
Andrej Bauer's user avatar
  • 9,553
12 votes
Accepted

What's “conservativity” in terms of type theory and how is it useful?

Anja Petković Komel in her PhD thesis Meta-analysis of type theories with an application to the design of formal proofs studied transformations of type theories among other things. Definition 9.3.3 on ...
Andrej Bauer's user avatar
  • 9,553
11 votes
Accepted

How to represent mathematical partial functions in a type-theory based proof assistant?

A commonly used approach to keep things simple is to define a function Q -> Q -> Q which returns the same result as the partial function for covered argument ...
Ihar Bury's user avatar
  • 299
11 votes
Accepted

What are the possible kinds of type theories or logics with quotients?

If I may advertise me and my coauthor's own work, our paper Observational Equality : Now for Good describes $\mathrm{TT}^{\mathrm{obs}}$, a relatively simple dependent type theory that is a variation ...
Loïc Pujet's user avatar
  • 1,479
11 votes

What is the difference between judgmental equality, definitional equality, and equality types?

Nick de Bruijn invented the distinction between "definitional equality" and "book equality" in: Bruijn, de, N. G. (1975). Set theory with type restrictions. In A. Hajnal, R. Rado, ...
Alex Nelson's user avatar
  • 1,564
11 votes

What are the differences between MLTT and CIC?

Apart from judgmental equality, MLTT and CIC also differ in the following: The existence of an impredicative universe. CIC has Prop, and that's what makes it a part of the lambda cube. This universe ...
ice1000's user avatar
  • 6,256
11 votes

What set-theoretic definitions can't easily be formalized in a type theory?

Andrej's answer that "Almost no pen-and-paper mathematics is written in ZFC" is correct. But it's perhaps also worth noting that some pen-and-paper mathematics is written in ZFC (or, at ...
Mike Shulman's user avatar
  • 3,180
11 votes

What are the upsides and downsides of typed vs untyped conversion?

From the perspective of implementation of conversion checking, it really depends on the specific setting. For vanilla intuitionistic type theories without more exotic features (like cubical TT, ...
András Kovács's user avatar
11 votes

What is a universe?

Note: I'm approaching this from a purely syntactic perspective. I'm sure that a deeper answer could be given from the semantic perspective. In all type theories I'm aware of, a universe is a type that ...
Matthew McQuaid's user avatar
11 votes
Accepted

What is hereditary substitution and why should I use it?

First, eta for sums is not feasible, if you want to avoid quotients or conversion relations. I don't know about any description of eta-normal forms for sum types in the literature; the closest are &...
András Kovács's user avatar
11 votes
Accepted

What is a commuting conversion and why are they problematic?

Syntactically, commuting conversions are part of the $\eta$-rules for left-invertible types -- i.e., types which have pattern-matching eliminators. So if $e : A + B$, the $\eta$-equation for it looks ...
Neel Krishnaswami's user avatar
10 votes

What is predicativity?

System F allows for function types like $T=\Pi X. X \to X$, where $X$ ranges through all the types. In particular, $T$ is one of them! This means that the usual set-theoretic interpretation of $\Pi (a:...
Trebor's user avatar
  • 4,015

Only top scored, non community-wiki answers of a minimum length are eligible