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.4k
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 ...
- 28.3k
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 ...
- 266
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
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
...
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
$...
- 13.7k
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$ (...
- 28.3k
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 ...
- 13.7k
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 ...
- 13.7k
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/...
- 13.7k
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 ...
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 ...
- 13.7k
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 β ...
- 11.4k
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,177
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,653
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,444
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.4k
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.4k
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 ...
- 2,040
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,444
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 ...
- 32.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 ...
- 28.3k
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
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 ...
- 28.3k
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,444
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,444
Only top scored, non community-wiki answers of a minimum length are eligible