# Questions tagged [type-theory]

For questions about type theory, including normalization, dependent types, identity types, inductive types, universe types, functional programming languages, proofs as programs in simply-typed lambda-calculi, Martin-Löf's intuitionistic type theory or related.Consider using one of the following tags: (lambda-calculus), (logic), (constructive-mathematics),(homotopy-type-theory) if related.

497 questions
Filter by
Sorted by
Tagged with
55 views

### Type theory and constructivist mathematics with paraconsistent logic?

Type theory, together with the Curry-Howard correspondence is a formal system for stating formal proofs of intuitionistic logic, which is used in constructive mathematics. Intuitionistic logic differs ...
48 views

78 views

### Strongly constructive proofs: Proofs that don't make use of decidability?

I was thinking about counting argumens from the perspective of constructivist / intuitionistic logic: A typical counting argument might have the following pattern: Suppose we have a finite set $S$ ...
76 views

### Rigorous definition of a type

What is a type in type theory? I tried to find a rigorous definition without luck. And that makes me wonder.. maybe there isn't any rigorous definition? My aim is to see how homotopy type theory ...
40 views

### ''Relax Type'' in Computational Logical Framework

I am reading a nlab article about Matt Oliveri's computational logical framework. It introduces new type constructors such as $\textsf{Relax}$. I tried to read the author's justification for the ...
53 views

### ''$\Gamma\vdash A\ \textrm{true}$'' in Martin-Löf type theory

I have a basic question about the notation ''$\Gamma\vdash A\ \textrm{true}$'' in Martin-Löf type theory. In his 1984 book, Martin-Löf says that if we have $\Gamma\vdash a:A$ and we do not care about ...
54 views

### Dependent tensor product in the category of abelian groups

In the category of set (or more generally an arbitrary locally cartesian closed category), we can think of a dependent product $\prod_{I}X$ of a "type family'' $X\to I$ index over $I$. For ...
476 views

40 views

### Do types and Curry-Howard correspondence belong to some kind of semantics of programming languages?

Is it correct that types belong to semantics of programming languages? In what kind of semantics are types studied: operational, denotational, and/or axiomatic semantics? Does the Curry-Howard ...
53 views

### Path induction for homotopies between functions

Consider a version of HoTT where every type former specifies the "shape" of its identity type definitionally (e.g. an equality of pairs is a pair of equalities, equality of types is ...
70 views

### Missing (important?) substitution rule

I am reading The HoTT Book and I noticed that there is an extensive use of a very reasonable principle: if we have $b \equiv c : A$ then we can conclude $(a =_A b) \equiv (a =_A c) : \mathcal{U}$, for ...
143 views

### Propositional truncation $||$-$||$ and double negation $\neg\neg$

I have a basic question about propositional truncation $||$-$||$ and double negation $\neg\neg$. According to the recursion rule of $||$-$||$, $A\rightarrow B=||A||\rightarrow B$ as long as $B$ is a ...
80 views

### $\neg\neg$-Stability

I see that some authors say that there are sets, for example, $\mathbb{N}$ and $\mathsf{Bool}$, that are $\neg\neg$-stable (i.e., satisfying $\neg\neg X\rightarrow X$). I understand what it means when ...
89 views

### $\textsf{isStable}(A)\rightarrow\textsf{isProp}(A)$?

I meet both $\neg\neg$-stable and proof-irrelevant types in Harper's handouts on homotopy type theory. I know clearly that proof irrelevance does not imply stability, but does stability imply proof ...
17 views

### Universe of all Types

Suppose we have a universe of all types $U_{\infty}$ that includes itself. Can someone explain why it is unsound -- in particular that we can deduce that every type, including the empty type, is ...
104 views

### Is category theory just type theory with different words?

According this this category theory provides a semantics for type theory. To me this means that category theory and type theory are essentially the same system just with different words. In fact this ...
135 views

### Proof-irrelevant $\exists$

Under the principle of propositions-as-types, existential propositions in logic are compared to $\Sigma$-types, and we have two projection rules $\pi_1$ and $\pi_2$ to make proof extraction. If we ...
34 views

### In what sense is $\Pi x: A.B$ the same as $B[x := a_1] \times B[x := a_2]$ when A is a finite type with two elements $a_1$ and $a_2$

This is in the context of the Type Theory system $\lambda P$ as presented in Chapter 5 of "Type Theory and Formal Proof: An Introduction" by Rob Nederpelt and Herman Guevers. Since I am ...
26 views

### Comparison of type theory based on relations vs logic based on functions

As it has been mentioned in Type Theory article at Stanford Encyclopedia of Philosophy, type theories fall into two classes, one in which functions are not primitive but functional relations which I ...
40 views

### How do you do construct a proof in type theory?

I am reading about Type Theory and trying to understand how proofs work. The idea seems like, to prove something, you build up the type using the semantic construction rules. So I want to prove that 2 ...
49 views

### Propositional truncation and information hiding

I have a question regarding propositional truncation $||$-$||$ in homotopy type theory. According to the introduction rule of $||$-$||$, if $a:A$, then $|a|:||A||$. My question is, if $||A||$ is ...
22 views

### Strongly Dependent-type languages (running on windows)

What are the best dépendent-type programming languages to learn about type-theory ? I heard about coq, agda, epigram and idris; are there any other ? And most importantly: wich one of these can easily ...
25 views

### Proof that the type of homotopy equivalence is not a proposition

I've seen in The HoTT Book that assuming univalence for homotopy equivalences is inconsistent (this is Exercise 4.6). On some page, I've read that this is because without this "qinv-univalence&...
65 views

### Actual and potential truth for neo-verificationists

Neo-verificationists such as Martin-Löf and Prawitz make a distinction between actual and potential truth of a proposition, roughly defined as follows: ... that a proposition A is actually true means ...
49 views

### What are the consequences of alternative type-theoretic definition of homotopy equivalence?

The standard definition of homotopy equivalence in HoTT is a quadruple of: $f: A \rightarrow B$ $g: B \rightarrow A$ $p: \operatorname{id} A = g \circ f$ $q: \operatorname{id} B = f \circ g$ ... ...