Questions tagged [type-theory]

Type structure is a syntactic discipline for enforcing levels of abstraction.

Filter by
Sorted by
Tagged with
2
votes
2answers
166 views

How does axiom K contradict univalence?

I have seen it claimed several times that axiom K is inconsistent with univalence (e.g. here and here), but I have never seen a proof sketch. Specifically, I'm curious about how this manifests in the ...
1
vote
1answer
82 views

Are coproduct types redundant in presence of natural numbers and $\Sigma$-types?

In the homotopy type theory book section A.2.5 defines $\Sigma$-types, A.2.6 coproduct types and A.2.9 the natural numbers type. If we already have $\Sigma$-types and the natural numbers type can we ...
7
votes
0answers
157 views

$\lambda$-definability and structure preserved by homomorphisms

I imagine there are some standard results that bear on this, but I'm having trouble finding a proof or refutation of it. Some prelimary definitions. A Henkin structure $A = (A^\cdot, ⟦\cdot⟧_A)$ for ...
7
votes
2answers
277 views

What's the categorical semantics of definitional equality?

The categorical semantics of a dependent type theory is normally described as a CwA/CwF/CompCat/etc. and in these models, we can talk about propositional equality by interpreting an 'identity type'. ...
6
votes
3answers
1k views

How does type theory change how one thinks about programming?

I have been dabbling in HoTT and I am convinced that dependent type theory is much more suitable than set theory for proof assistants. Now, this made me wonder - how fundamental is Type Theory ...
2
votes
2answers
169 views

What is the point of the eliminator for the unit type?

In the HoTT book p. 436 A.2.8 the eliminator $\mathrm{ind}_{\mathbf{1}}$ for the unit type is described. What is the point of it? What if you did not introduce it and instead just replaced all the ...
5
votes
1answer
105 views

$\eta$-reduction not locally confluent on well-typed terms

This paper says: "In the presence of a unit type, $\eta$-reduction is not even locally confluent on well-typed terms [20]." [20] is a reference to a 300-page book with no further details and ...
2
votes
0answers
67 views

Reference request: characterisation of simultaneous substitution

For simply typed λ-calculus, a simultaneous substitution from $\Gamma$ to $\Delta$ is concretely a type-preserving map from variables in $\Delta$ to terms in $\Gamma$. See, for example, Programming ...
8
votes
0answers
152 views

Constructive Strong Normalization of the Extended Calculus of Constructions

The extended calculus of constructions (ECC) is basically the calculus of constructions with cumulative universes. I use the definition which Zhaohui Luo used in his PhD theses which contained a proof ...
3
votes
1answer
133 views

How to think about `comp` in cubical type theory

Consider the definition: ...
2
votes
1answer
97 views

External failure of law of excluded middle in Martin-Löf type theory

Is there an explicit type $T$ in Martin-Löf type theory such that $(T\to \mathbf{0})\to\mathbf{0}$ has an explicit closed term and $T$ can be shown externally to not have closed terms?
0
votes
0answers
81 views

CubicalTT: successor of add proof?

Lecture 2 of the cubical type theory lectures provide a proof of (suc a) + b = suc (a + b): ...
1
vote
0answers
69 views

MLTT/MiniTT: why do normal forms of sum types carry environments?

I am learning how to implement MiniTT: a simple type theoretic language, which is a dependently typed language with sum types, mutual recursive/inductive definitions and a universe of small types. A ...
6
votes
1answer
180 views

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

Pattern matching on $\cal U$ is allowed in XTT and Idris2 (for unerased types), and that implies the injectivity of type constructors (that's just my intuition, though -- I also wonder how do I prove ...
2
votes
2answers
425 views

Does univ : univ always lead to a contradiction in a dependently typed language?

I am currently following Checking Dependent Types with Normalization by Evaluation: A Tutorial by David Christiansen, where we consider the type of U (the universe ...
2
votes
1answer
158 views

Alternatives to Normalization by Evaluation

Reading about lambda calculus I got the impression that normalization is evaluation. So I don't understand what is meant by Normalization by Evaluation (used e.g. in several publications of A. Abel). ...
3
votes
0answers
79 views

Equality reflection without $\eta$

Are type theories with equality reflection (i.e. having a term of an identity type between two objects allows us to freely swap them) but not the $\eta$-rule for $\Pi$-types interesting? Does function ...
3
votes
2answers
357 views

What technique is used to implement type checking for CoC?

I am studying David Christiansen's tutorial on implementing a dependently typed language, where it says: Typed normalization by evaluation is far from the only way to implement conversion checking ...
10
votes
1answer
541 views

Why is regularity a problem in cubical type theory?

In my current understanding, regularity in cubical type theory is the following definitional equality (I'm using $A~\textbf{type}$ to emphasize the fact that $i \notin FV(A)$): $$ \cfrac{A~\textbf{...
5
votes
1answer
121 views

Definitional function extensionality for functions out of $\mathbf{2}$

Denote by $a$ and $b$ the canonical terms of $\mathbf{2}$. For any map $f:\mathbf{2}\to \mathcal{U}$ we have the eliminator$$\mathrm{ind}_{\mathbf{2}}(f) : \big(f(a) \times f(b)\big) \to \prod_{x:\...
0
votes
2answers
80 views

Pi-type over a list in dependent type theory

In a formalization I need to create an inductive type which has a term for each element in a list, something like this (I'll use Agda in the following, but everything here is standard dependent type ...
3
votes
1answer
147 views

Are uniqueness rules converse to introduction rules?

I've seen many people connecting introduction rules and elimination rules, saying that they're dual notion. Indeed, like in the categorical model, these rules are symmetric morphisms. However, if we ...
0
votes
1answer
89 views

Reference for context-free grammar for Martin-Löf type theory

Are the terms and the types of Martin-Löf type theory described by context-free grammars? Have such grammars been written down somewhere?
3
votes
0answers
85 views

Boltzmann sampling for containers/dependent polynomials?

I’d like to randomly sample from dependently-typed data structures. Has anyone looked at extending Boltzmann sampling to containers or dependent polynomials?
3
votes
1answer
216 views

Is just one W-type enough for formalizing mathematics?

We work in intensional Martin-Löf type theory with $0$, $1$, $2$, $\Pi$, $\Sigma$, $W$ and a cumulative hierarchy of universes. Suppose our goal is to formalize constructive mathematics. Now if we ...
2
votes
0answers
141 views

Set-theoretic encoding of functions in type theory

Functions usually get encoded in set theory as follows. A function $A\to B$ is a subset $f\subset A\times B$ such that $\pi_1:f\to A$ is a bijection. In type theory to give a function $A\to B$ is to ...
2
votes
1answer
106 views

Dependent eliminator for empty type in intensional Martin-Löf type theory

In calculus of inductive constructions you can just say that the empty type is the type with no constructors and it automatically builds the dependent eliminator. But let's say I'm setting up ...
-1
votes
1answer
94 views

How much type information do Hindley-Milner proof assistants need to remain sound?

A known benefit of the HM type system is that you can usually infer a term's most general type with no user-provided type annotations. For example, if my theory contains the standard axiom: $$\forall ...
1
vote
2answers
116 views

Explicit type system with infinite non-cumulative universe hierarchy

Is there an open-source proof assistant or at least an explicit set of rules written down somewhere for a type system with an infinite non-cumulative universe hierarchy and unique typing? I want to ...
0
votes
0answers
49 views

Complexity of finding typing derivation trees

In type theories where type checking is decidable do we have estimates for how much time/space it takes to find a typing derivation tree of a valid typing judgment? Do any published references do this ...
2
votes
0answers
75 views

What is the relation of parametricity and function extensionality?

In Agda function extensionality can be defined like this: funExt = {A : Set} {B : Set} {f1 f2 : A → B} → (∀ x1 x2 → x1 ≡ x2 -> f1 x1 ≡ f2 x2) → f1 ≡ f2 One may ...
2
votes
2answers
135 views

$\mathbb{N}$ in intensional MLTT with judgmentally commutative $+$ and $\times$

Is there a way to implement natural numbers in intensional Martin-Löf type theory so that addition and multiplication is judgmentally commutative?
4
votes
1answer
134 views

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

Consider intensional Martin-Löf type theory with judgmental $\eta$ rule for dependent product types. Is there a model of it where function extensionality fails?
4
votes
0answers
149 views

Model of homotopy type theory where propositional & judgmental equality coincide for closed terms

In intensional Martin-Löf type theory we can prove the metatheorem that two closed terms are propositionally equal iff they are judgmentally equal. Is there a non-empty model of homotopy type theory ...
2
votes
1answer
81 views

Normal term of double negation of W-type

Consider the intensional Martin-Löf type theory without axiom of choice or the law of excluded middle. Let $A:U_0$ be a type and $B:A\to U_0$ be a function such that $\Sigma_{a:A}(B(a)\to 0)$is ...
5
votes
1answer
298 views

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

To define a (non-indexed) W-type all we need is a type $A:U$ and a function $B:A\to U$ and we get a type $W_{a:A}B(a)$. To check that this definition is valid we only need to check that the ...
3
votes
1answer
153 views

Defining binary natural numbers without quotient types

Let's say we work in a dependent type theory with W-types and we want to have a type for binary natural numbers. We don't want to add quotient types or higher inductive types to the system. How to ...
3
votes
1answer
86 views

Relating functors to relational functors with the parametricity translation

$\newcommand{\Type}{\text{Type}}\newcommand{\id}{\text{id}}\newcommand{\map}{\text{map}}$ In attempting to answer the question: Rigorous proof that parametric polymorphism implies naturality using ...
2
votes
1answer
71 views

Surjection from a type to a universe

We work in homotopy type theory. Can there be a type $A:U_m$ and a map $f:A\to U_n$ for some $n\geq m$ such that the type $\prod_{T:U_n} \|\mathrm{fib}_f(T)\|$ is inhabited?
2
votes
1answer
94 views

Typing inference as a map on abstract syntax trees

Is there a reference that explains typing inference for Martin-Löf type theory as a computable map from abstract syntax trees of terms to abstract syntax trees of types? I don't want to identify non-...
5
votes
1answer
177 views

Choose term of coproduct type

We work in homotopy type theory. Denote the propositional truncation of a type $A$ by $\|A\|$ and the function type between types $A$ and $B$ by $A \to B$. Can you construct a term of the following ...
7
votes
1answer
395 views

Strongly normalizing type theory beyond induction-recursion

Are there known type theories in the literature, which have strong normalization proofs and their proof-theoretical strength goes beyond strength of type theories with induction-recursion?
4
votes
0answers
79 views

Relative consistency of various Martin-Löf style type theories

I am wondering about relative consistency of various Martin-Löf type theories, when compared to one another, I will use MLTT for the intensional Martin-Löf type theory with $\Pi$, $\Sigma$, $\mathbb{N}...
4
votes
0answers
150 views

What logic do refinement types correspond to?

I'm interested in applicability of refinement types to theorem-proving hence the questions about their logical expressiveness. Let's say, we have a type system which corresponds to some logic ...
3
votes
1answer
127 views

Structural normalization algorithm for the simply typed lambda calculus

I would like to know if there is a (piecewise) structural normalization algorithm for the simply typed lambda calculus. By structural I mean a recursive function that only calls itself on subterms of ...
8
votes
1answer
127 views

"Interesting" categories whose internal logic is a dependent-linear type theory

Dependent-linear type theories may be a functional programmer's dream, but is it categorically interesting, i.e. is it the internal language of an "interesting" category? By "...
0
votes
0answers
75 views

What do we call a type system where any term of any type ultimately parses down to $*:\mathbf{1}$?

If a type system allows inductive types (as in e.g. Coq) then we can coin new primitive constants that inhabit types. For example $0:\mathbb{N}$ is constructed when defining $\mathbb{N}$ and does not ...
4
votes
1answer
97 views

Context weakening as an explicit rule for languages of the the lambda cube?

I'm trying to formalize the syntax and typing judgments of the Calculus of Constructions in Coq. I'm choosing to use the Pure Type Systems presentation of CoC; however, I've seen mild variations in ...
6
votes
2answers
260 views

Intuition behind nested positivity and counterexamples

I'm looking at the nested positivity conditions for inductive types stated in the Coq manual. First off, are there any other references (not necessarily for Coq, but in dependent type theories ...
0
votes
2answers
225 views

Why is plus-comm a b $:\equiv$ refl (plus a b) not a proof of the commutativity of addition?

I've been curious about the 'geometric situation' that one has when considering the type $\prod_{(n,m:\textrm{Nat})}(\textrm{plus}\ n\ m) = (\textrm{plus}\ m\ n)$. Here, addition is defined in the ...

1
2 3 4 5
7