# Questions tagged [type-theory]

The tag has no usage guidance.

109 questions
Filter by
Sorted by
Tagged with
283 views

### Uniqueness principle for functions types in the HoTT book

Chapter 1.2 of the HoTT book says this about eta-conversion: $$f \equiv (\lambda x . f(x)).$$ This equality is the uniqueness principle for function types, because it shows that $f$ is uniquely ...
130 views

### Categorical semantics of the identity type

In Appendix B of the article Simplicial Model of Univ. Foundations, Definition B.1.3 specifies the structure for identity types in a contextual category $\mathcal{C}$ (which in particular is equipped ...
170 views

### Are any formal systems based upon the idea of “iterated characterization pushing” currently in existence? If not, is anyone working on them?

I had an idea in regards to the design of formal systems with foundational aspirations. To convey the idea, let's talk a bit about the second-order Peano axioms. The way these axioms work, we have a ...
193 views

### A sequence in the hierarchy of universes

The HoTT Book states in the first chapter that universes are cumulative and that every universe is in some other universe. Obviously, there needs to be an infinite number of universes then, but ...
128 views

### An equation involving multisets

For finite multisets $A, B, C, A', B', C'$, if $A \uplus B \uplus \{B \uplus C\} \uplus \{A \uplus \{C\}\}$ = $A' \uplus B' \uplus \{B' \uplus C'\} \uplus \{A' \uplus \{C'\}\}$, must $A=A',B=B',C=C'$, ...
2k views

### Good introductory book to type theory?

I don't know anything about type theory and I would like to learn it. I'm interested to know how we can found mathematics on it. So, I would be interested by any text about type theory whose angle ...
204 views

151 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 ...
66 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) ...
789 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 ...
238 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 ...
781 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 ...
166 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 ...
98 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, ...
129 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 ...
277 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 ...
381 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 ...
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 ...
143 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 ...
739 views

From the formula $$\forall f\colon A\to A\,\exists x\colon A\,(f(x)=x)$$ we can get the scheme $$\forall x\colon A\,(\phi(x)\vee\neg\phi(x))\Rightarrow\forall x\colon A\,\phi(x)\vee\forall x\colon A\,\... 3answers 372 views ### Homotopy type theory: Are the hierarchy of Type_k universes isomorphic? In homotopy type theory, or dependent type theories more generally, there is a "top-level" type called the universe, generally denoted \newcommand{\type}{\mathtt{Type}}\type. So for a concrete ... 1answer 273 views ### Why are types in type theory unordered collections? Please excuse my naïveté, I have no higher math education, just a curious observer. In type theories, types are treated as set-like because they're unordered collections. Yet, the putative motive in ... 5answers 2k views ### How do we construct the Gödel’s sentence in Martin-Löf type theory? In Martin-Löf dependent type theory (MLTT), under the proposition-as-types correspondence, we sometimes say that a proposition A is true if the type A is inhabited. However, there is no doubt that ... 1answer 193 views ### Substructural types, the lambda calculus, and CCCs It's well known that the simply-typed lambda calculus corresponds to a cartesian closed category. How would substructural type systems be characterized in category theory? For example, linear type ... 2answers 922 views ### Is simply typed lambda calculus with fixed-point combinator Turing-complete? There are many sources cite that simply typed lambda calculus extended with fixed-point combinator is Turing complete. For example, Does there exist a Turing complete typed lambda calculus? or the ... 0answers 174 views ### Ends and parametricity It is well known that a set of natural transformations can be expressed as an end:$$\int_{A \in \mathcal{A}} \mathcal{B}(FA, GA) =_{\operatorname{Set}} \operatorname{Nat}(F, G) This holds for ...
This question is probably really naive. And, I hope the title doesn't come off as too combative. I think that topoi of $\mathbf{Set}$-valued sheaves provide an excellent motivation for higher-order ...