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 ...
Neel Krishnaswami's user avatar
16 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 ...
Levi Pearson's 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 ...
Andrej Bauer's user avatar
  • 28.9k
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 ...
Jasper Hugunin's user avatar
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$ (...
Andrej Bauer's user avatar
  • 28.9k
10 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 ...
David Christiansen's user avatar
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 ...
cody's user avatar
  • 13.9k
9 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 ...
cody's user avatar
  • 13.9k
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 ...
cody's user avatar
  • 13.9k
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/...
cody's user avatar
  • 13.9k
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 ...
Max New's user avatar
  • 1,675
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 ...
Łukasz Lew's user avatar
  • 1,187
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/...
Jesper's user avatar
  • 356
8 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 ...
András Kovács's user avatar
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 ...
Neel Krishnaswami's user avatar
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 ...
Neel Krishnaswami's 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: ...
András Kovács's user avatar
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 ...
Neel Krishnaswami's user avatar
6 votes

Type checking, Hypothetical judgments, meaning explanations and computational type theory

Part of the problem is we cannot say that we have a checker for categorical judgments, because these often reduce to hypothetical judgments. For instance, the categorical judgment $M\in A\to B$ ...
Jonathan Sterling's user avatar
6 votes
Accepted

Fixed points in dependent type theories

I think the idea of unifying type and term-level fixpoints is natural, though I have to admit I'm not sure that reducing the number of constructions of a system is not always a recipe for conceptual ...
cody's user avatar
  • 13.9k
6 votes

When a type is a value?

I will offer a semantic perspective. The relationship between values and general computations may be expressed in terms of an adjunction between two categories: \begin{align*} F &: \mathcal{V} \to ...
Andrej Bauer's user avatar
  • 28.9k
6 votes

Intuition Behind Strict Positivity?

Another good source for going beyond strictly positive types is the PhD thesis of Ralph Matthes: http://d-nb.info/956895891 He discusses extensions of System F with (strictly) positive types in ...
Henning Basold's user avatar
6 votes
Accepted

PHOAS with extrinsic typing?

The standard well-formed-related predicate can be relatively easily extended to handle untyped PHOAS. The main subtlety is how to handle reduction at the type level. Here's a start of a two-place ...
Jason Gross's user avatar
6 votes
Accepted

Defining finite sets inductively in a proof assistant?

There are many variants of finite sets in constructive mathematics. One that can be defined using just inductive definitions, and is therefore amenable to formalization in type theory, is the ...
Andrej Bauer's user avatar
  • 28.9k
6 votes
Accepted

Impredicativity + large eliminations (with no excluded middle) in Coq

No: strong elimination of large inductive types (SELIT) is itself inconsistent because it breaks the layering of universes by trivially allowing you to smuggle a large value in a Prop box and take it ...
Stefan's user avatar
  • 390
6 votes

Model of MLTT with $\eta$ rule where function extensionality fails

The simplest one that I know about is the $\text{Set}$-based polynomial model ("container" model). Here, every context is interpreted as a family of sets, i.e. a $Q : \text{Set}$ together ...
András Kovács's user avatar
6 votes
Accepted

What technique is used to implement type checking for CoC?

May I have a reference to why η expansion is invalid for CoC? It's not invalid. It's up to choice whether $\eta$-conversion for functions (or other types) is included. The original CoC paper seems to ...
András Kovács's user avatar
6 votes
Accepted

What are the pros and cons for type cases in dependent type theories?

The basic idea is clearest when you think about things in terms of Tarski-style universes. There, you have a data type of codes, and an interpretation function which maps codes to types. In this case, ...
Neel Krishnaswami's user avatar
6 votes
Accepted

Example use cases for induction-recursion

Here is one article that discussed induction-recursion. Here's their code: ...
ice1000's user avatar
  • 965
6 votes
Accepted

Dependent type theory and definitions of cumulativity

The contravariant rule for functions would indeed work, and it is supported by the semantics in Generalized Universe Hierarchies and First-Class Universe Levels. The reason for invariant function ...
András Kovács's user avatar

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