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 ...
- 32.8k
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 ...
- 29.4k
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 ...
- 256
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$ (...
- 29.4k
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 ...
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 ...
- 14k
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 ...
- 14k
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/...
- 14k
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 ...
- 1,695
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 ...
- 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/...
- 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 ...
- 1,639
7
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 ...
- 14k
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 ...
- 32.8k
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 ...
- 32.8k
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:
...
- 1,639
7
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 ...
- 29.4k
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$ ...
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 ...
- 29.4k
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 ...
- 326
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 ...
- 271
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 ...
- 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 ...
- 1,639
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 ...
- 1,639
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, ...
- 32.8k
6
votes
Accepted
Example use cases for induction-recursion
Here is one article that discussed induction-recursion. Here's their code:
...
- 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 ...
- 1,639
5
votes
Accepted
Strong Normalization of Extended Calculus of Constructions (CC with cumulative universes)
I guess this is just an extension of my comment, but I've heard Luo cite Goguen's paper The metatheory of UTT which uses typed operational semantics. I'm afraid I can't find a free online version ...
- 14k
5
votes
How does type theory change how one thinks about programming?
To me, type theory bridges programming with models and proof theories. In particular, I can use category theory to think about programming languages when the underlying type theory has a categorical ...
- 965
5
votes
Accepted
Formulation of Tarski-style universes in LF
Papers on universes are usually concerned with universes that are large, i.e., most authors are intersted only in universes closed under dependent products. But nothing prevents us from having a baby ...
- 29.4k
Only top scored, non community-wiki answers of a minimum length are eligible