22 votes
Accepted

Why it's impossible to declare an induction principle for Church numerals

The question you are asking is interesting and known. You are using the so-called impredicative encoding of the natural numbers. Let me explain a bit of the background. Given a type constructor $T : \...
user avatar
  • 26.7k
19 votes
Accepted

Why an infinite type hierarchy?

Actually, the approach of the CoC is more expressive -- it permits arbitrary impredicative quantification. For example, the type $\forall a.\; a \to a$ can be instantiated with itself to get $(\forall ...
user avatar
17 votes
Accepted

Dependent Sums and Products

I think what's confusing you is that $A \times B$ is both a product and a coproduct: It is the product of two factors, namely $A$ and $B$. It is the coproduct of $A$-many copies of $B$. Once you ...
user avatar
  • 26.7k
16 votes

In the Hott book, are the most of the type formers redundant? And if so, why?

You are asking several questions which are similar but distinct. Why doesn't the HoTT book use Church encodings for data types? Church encodings do not work in Martin-Löf type theory, for two ...
user avatar
15 votes
Accepted

Dependent Types and Compile Time Types

A language can be thought of as having both a static semantics, which determines the compile-time analysis that occurs; and a dynamic semantics, which determines the execution-time behavior of ...
user avatar
15 votes
Accepted

In the Hott book, are the most of the type formers redundant? And if so, why?

Let me explain why the suggested encoding of the empty type does not work. We need to be explicit about universe levels and not sweep them under the rug. When people say "the empty type", they might ...
user avatar
  • 26.7k
14 votes
Accepted

Defining inductive types in intensional type theory purely in terms of type-theoretic data

It turns out that $W$ types plus identity types (eq/= in Coq) allow you to construct pretty much all the general inductive types ...
user avatar
11 votes
Accepted

Reference for the fact that (0=1) implies false requires a universe in MLTT

I know of: Jan M. Smith, The independence of Peano's fourth axiom from Martin-Löf's type theory without universes, The Journal of Symbolic Logic 53(3), p. 840-845, 1988.
user avatar
11 votes
Accepted

Relating univalence for a theory of cateogries to the skeleton concept

I refer you to Chapter 9 of the HoTT book. In particular, a category is defined in such a way that isomorphic objects are equal, see Definition 9.1.6. As Example 9.1.15 points out, there really isn't ...
user avatar
  • 26.7k
10 votes
Accepted

Church-Rosser property for dependently typed lambda calculus?

It might be useful to quickly give the counter-example to CR in typed calculi with $\beta$ and $\eta$: $$ t=\lambda x:A.(\lambda y:B.\ y)\ x$$ And we have $$ t\rightarrow_\beta \lambda x: A.x$$ and $...
user avatar
  • 13.2k
10 votes

Preservation under Substitution with Telescopes

The most general form of substitution theorems speaks about arbitrary contexts: Define what it means to have a substitution $\sigma : \Gamma \to \Delta$ from a context $\Gamma$ to a context $\Delta$ (...
user avatar
  • 26.7k
9 votes
Accepted

Examples of Universe inconsistency in normal use of dependent types

This is a hard question to answer, in part because it's unclear what it means to get something "by accident". Regularly, though, people run into the ...
user avatar
  • 13.2k
9 votes
Accepted

Dependent types over Church-encoded type in PTS/CoC

You can't do this using the traditional Church encoding for Bool: #Bool = ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool ...
user avatar
9 votes

Why an infinite type hierarchy?

I'll compliment Neel's (excellent, as usual) answer with a bit more exposition on why levels are used in practice. The first important limitation of CoC is that it is trivial! A surprising ...
user avatar
  • 13.2k
9 votes
Accepted

Proof techniques for showing that dependent type checking is decidable

There is indeed a subtlety here, though things work out nicely in the case of type checking. I'll write down the issue here, since it seems to come up in many related threads, and try to explain why ...
user avatar
  • 13.2k
9 votes
Accepted

Intuition Behind Strict Positivity?

It sounds like you want an overview of normalization arguments for type systems with positive datatypes. I'd recommend Nax Mendler's PhD dissertation: http://www.nuprl.org/documents/Mendler/...
user avatar
  • 13.2k
9 votes
Accepted

Similarities and differences between Pie and popular languages with dependent types

I'd say that Pie is a much smaller version of the core languages of those systems. It's a bit closer to Lean's core than to Coq, Agda, or Idris, but the differences are not very large there. When I ...
user avatar
8 votes

Church-Rosser property for dependently typed lambda calculus?

Quite a bit is know about this. The concept of Pure Type Systems (PTS) is useful for showing Church-Rosser (CR) for large classes of typed $\lambda$-calculi. Paraphrasing (1): PTS with only β ...
user avatar
8 votes
Accepted

Motivation for Dependent Type

Actually, the motivation for introducing dependent types goes in the opposite direction! Curry had noticed that there was a direct correspondence between typed terms in the $SK$ calculus and proofs in ...
user avatar
  • 13.2k
8 votes
Accepted

If the untyped language is terminating, can we still derive a contradiction from `Type : Type`?

The 'logic' of the contradiction with Type:Type is that you can create a term of any type including 'empty' type by 'cheating' by never returning. This is ...
user avatar
  • 1,147
8 votes
Accepted

Preservation under Substitution with Telescopes

The property, which I would call "typing of substitution" should hold in any type theory, and is not dependent on the exchange property (which I assume is what you mean by permutation) The key is ...
user avatar
  • 1,474
8 votes
Accepted

Small kernel (i.e. proof-verifier) for Agda?

It is true that Agda currently has a much shakier foundation than say Coq or Lean. It does have an internal term syntax that could be seen as a core language (https://github.com/agda/agda/blob/master/...
user avatar
  • 356
7 votes

Proving running time upper bounds for algorithms in dependent type theory

As usual, (a) the high-level conceptual approach is basically the same as it is on paper, but (b) mechanization makes new things reasonable to attempt. The way you do things is to define a cost ...
user avatar
7 votes

What are the negative consequences of extending CIC with axioms?

One first reason to reject axioms is that they might be inconsistent. Even for the axioms that are proved consistent, some of them have a computational interpretation (we know how to extend ...
user avatar
  • 1,910
7 votes

Explicit set of types and terms in MLTT

How do you actually construct the sets of types and terms (more) formally in set theory, and convince me that these actually do form a set? It's essentially the same argument that BNF grammars ...
user avatar
7 votes
Accepted

Structural equality of Pi Types with heterogeneous equality?

I am not aware that J or K exists for heterogeneous equality. It does not need an elimination principle, because it can be simply defined as a sigma type: ...
user avatar
7 votes
Accepted

What's the categorical semantics of definitional equality?

Definitional equality is the same as equality in the metatheory. It works exactly the same way as in 1-category theory. If I have a category $\mathbb{C}$ and some morphisms $f,g : \mathbb{C}(A, B)$, I ...
user avatar
6 votes
Accepted

How to translate the axiom schema of induction by Curry-Howard?

First a correction. The statement $$\forall P \,.\, (P(0) \Rightarrow (\forall n . P(n) \Rightarrow P(S n)) \Rightarrow \forall m . P(m)),$$ is not the schema of induction, but rather induction ...
user avatar
  • 26.7k
6 votes

Parametricity and projective eliminations for dependent records

I just talked to Dan Doel and he explained that his reference was in fact one Neel Krishnaswami. He saw a comment on n-cafe by you that one could do strong induction using parametricity, so he went ...
user avatar
  • 1,344
6 votes

What is a canonical term of $\text{Id}_A(x,y)$ if $x$ is not jugdmentally identical to $y$?

Yes, in general $\mathrm{Id}_{A}(x, y)$ will not have a canonical form. Consider the case when $x$ and $y$ are distinct free variables -- obviously you can postulate that $x$ and $y$ are equal, but ...
user avatar

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