# Tag Info

## Hot answers tagged type-theory

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, ...
• 9,553
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 ...
• 9,553
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 ...
• 1,256

### 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 ...
• 2,023
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 ...
• 2,846

### 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}$, ...
• 1,287
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 ...
• 9,553
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 ...
• 3,180

### 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 ...
• 3,180

### 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 ...

### 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: ...
• 2,023
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-...
• 1,287
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 &...
• 2,316
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 ...
• 6,256
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:...
• 9,553
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 ...

### 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 ...
• 5,146

### 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 ...

### 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 ...
• 9,553
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 ...
• 9,553
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 ...
• 299
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 ...
• 1,479

### 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, ...
• 1,564

### 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 ...
• 6,256

### 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 ...
• 3,180

### 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, ...
• 2,077

### 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 ...
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 &...
• 2,077
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 ...
• 2,023
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:...