# Questions tagged [type-theory]

The tag has no usage guidance.

103 questions
511 views

### What's the point of cubical type theory?

I have been following through the development of homotopy type theory since 2013 because I was really interested in the foundation of mathematics. The novel idea of combining programming with homotopy ...
184 views

676 views

### What kind of category is generated by Cubical type theory?

What kind of ‘category’ is Cubical type theory the internal language of? Its known that Martin-Löf type theories are the internal language of Locally cartesian closed categories, adding higher ...
137 views

### What is the consistency limit of accumulative typing below $\omega_1^{CK}$?

Let $Th_\zeta$ be a Mono-sorted first order theory with $\zeta$ representing some recursive ordinal notation system. Primitives: =, $\in$, $T_0, T_1, ..,T_i,..$ where i is an $\zeta$ ordinal, and ...
61 views

### What is the relation of total functions in second order arithmetic and fast growing hierarchies?

Answer to this questions shows that fast growing hierarchies can grow arbitrarily fast for some definition of 'arbitrary'. Can second order arithmetic define all these functions (for any ordinal) ...
204 views

### Stability and complete types (in Model Theory)

I read the following statement in these slides of Saharon Shelah: "$K$ is stable iff for every $M \in K$ there are only "few" complete types over $M$." About the notation: here $K$ consists of all ...
2k views

### History of the notation for substitution

One of the very common notations for syntactic substitution is $[\ /\ ]$. However, there seems to be an inconsistency in the literature about its usage. Many write $[t/x]$ for "substitute $t$ for $x$...
292 views

### Easier Girard's paradox in a circular pure type system (PTS)

System U is an inconsistent PTS in that one has a term of type $\bot = \forall p\colon \ast \ldotp p$, and such a term is explicitly constructed in Hurkens' A Simplification of Girard's Paradox. One-...
760 views

### New articles by Errett Bishop on constructive type theory?

Recently two formerly unknown articles by Errett Bishop (1928-1983) were posted online by Martín Escardó. One is entitled "A general language", deals with constructive type theory, and ...
143 views

### Is Calculus of Constructions type inhabitance semi-decideable?

I'm wondering if type inhabitance for the calculus of constructions is semi-decideable. I know the following: System F inhabitance and, correspondingly, second-order unification are semi-decideable ...
1k views

### Equivalent form of the Univalence Axiom

I'm reading the new HoTT book and I'm wondering about a potential equivalent form of the Univalence Axiom: $(A \simeq B) \simeq (A = B)$. For simplicity, I'm tacitly working in a fixed universe. It ...
87 views

### Was Martin-Löf inspired by Peirce when he introduced the dependent sum and dependent product types?

In the following article: https://plato.stanford.edu/entries/peirce-logic/ it is mentioned that Peirce's introduced the use of the symbols $\Sigma$ and $\Pi$ to express logical sums and products, ...
1k views

### Can you have a type theory where there is type of all types?

Normally in a type theory, you can not have a type of all types, due to Girad's paradox. This is somewhat similar to how in set theory, you cannot have a set of all sets. Therefore, usually you just ...
121 views

### Propositional vs Definitional extentionality in type theory

There are essentially two ways to impose extentionality on a type theory (I know, it is not very fashionable to impose extentionality these days, but please, bear with me) you can either have a "...
1k views

### In constructive mathematics, why does the category of abelian groups fail to be abelian?

I was reading the paper Towards Constructive Homological Algebra in Type Theory by Thierry Coquand and Arnaud Spiwack, and they state that constructively, the category of abelian groups fails to be ...
237 views

### What does first-order co-intuitionistic logic look like (and does it have an equivalent type theory)?

So, this is where I'm at so far: Heyting algebras model propositional intuitionistic logic (IL) so do Cartesian closed categories which also model the simply typed lamda calculus co-Heyting algebras ...
308 views

### How to handle sums in Tait's reducibility proof of strong normalisation?

I've been reading Girard et al's 'Proofs and Types', which in Chapter 6 presents a proof of strong normalisation for the simply typed lambda calculus with products and base types. The proof is based ...
141 views

### Generalized (co)-presheaves for Generalized Multicategories?

A $T$-multicategory in the sense of Crutwell-Shulman, where $T$ is a monad on a virtual double category $C$ is a monoid in the "horizontal kleisli category", i.e., an object of objects $O$, a ...
714 views