# Questions tagged [type-theory]

The type-theory tag has no usage guidance.

109
questions

**4**

votes

**1**answer

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 ...

**2**

votes

**0**answers

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 ...

**5**

votes

**0**answers

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 ...

**0**

votes

**1**answer

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 ...

**0**

votes

**0**answers

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'$, ...

**21**

votes

**8**answers

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 ...

**6**

votes

**2**answers

204 views

### When is a fold monomorphic/epimorphic

Given a functor $F : \mathcal C \to \mathcal C$ with initial algebra $\alpha : FA \to A$, and another algebra $\xi : FX \to X$, we obtain a unique morphism $\mathsf{fold}~\xi : A \to X$ such that $\...

**5**

votes

**2**answers

696 views

### How can the simply typed lambda calculus be Turing-incomplete, yet stronger than second-order logic?

It is well-known that the simply typed lambda calculus is strongly normalizing (for instance, Wikipedia). Hence, it is not strong enough to be Turing-complete, as also mentioned on the Wikipedia page ...

**3**

votes

**0**answers

249 views

### Formal foundations done properly [closed]

I would want to do mathematics properly, so that the proofs of results can be trusted on instead of them being just suggestions on which results could perhaps apply. This means formulating the math in ...

**13**

votes

**1**answer

545 views

### A peculiarity of Henkin's 1950 proof of completeness for higher order logic

My question concerns Henkin's original (1950) completeness proof https://projecteuclid.org/euclid.jsl/1183730860 for classical higher order logic and type theory relative to so-called general models.
...

**5**

votes

**1**answer

380 views

### Progress towards a computational interpretation of the univalence axiom?

I will preface this by saying that I am not an expert on type theory. I am just a curious outsider slowly making my way through the HoTT book when I (rarely) have some spare time.
I am just curious ...

**6**

votes

**1**answer

340 views

### Proof of ¬(¬1 ⊗ ¬1) in tensorial logic

I believe I once had a proof of this proposition, but it's been lost to the mists of time and old hard drives, so who knows if it was correct, and try as I might I can't seem to reproduce it.
Is it ...

**3**

votes

**1**answer

108 views

### Internal equality for Eq-fibrations' morphisms

I have posted this question here on M.SE but since it received little attention and since it seems difficult to find helpfule references I reposting it here.
In Jacob's Categorical logic and Type ...

**12**

votes

**4**answers

1k views

### Formalizations of the idea that something is a function of something else?

I'll state my questions upfront and attempt to motivate/explain them afterwards.
Q1: Is there a direct way of expressing the relation "$y$ is a function of $x$" inside set theory?
More ...

**8**

votes

**0**answers

258 views

### What metatheory proves cut elimination for Simple Type Theory?

Gaisi Takeuti's book Proof Theory proves cut elimination for Simple Type Theory (a combined result of several researchers). Thus it proves consistency of Simple Type Theory with full comprehension in ...

**13**

votes

**0**answers

977 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 ...

**2**

votes

**1**answer

184 views

### Can a type in a lower universe be formed from types in higher universes?

A type universe is a type of small types that is closed under the basic type formation operations (dependent product, sum, coproduct etc.), that is to say for example that from
$A \colon U_i$ and
$x \...

**2**

votes

**0**answers

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 ...

**2**

votes

**0**answers

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) ...

**15**

votes

**2**answers

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 ...

**3**

votes

**2**answers

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 ...

**16**

votes

**1**answer

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 ...

**1**

vote

**1**answer

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
...

**3**

votes

**0**answers

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, ...

**5**

votes

**1**answer

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 "...

**15**

votes

**1**answer

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 ...

**6**

votes

**0**answers

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 ...

**7**

votes

**3**answers

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 ...

**19**

votes

**1**answer

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 ...

**7**

votes

**0**answers

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 ...

**6**

votes

**1**answer

739 views

### Rice's theorem in type theory

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\,\...

**4**

votes

**3**answers

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 ...

**2**

votes

**1**answer

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 ...

**23**

votes

**5**answers

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 ...

**3**

votes

**1**answer

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 ...

**7**

votes

**2**answers

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 ...

**8**

votes

**0**answers

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 ...

**19**

votes

**3**answers

1k views

### Why would the category of sets be intuitionistic?

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 ...

**6**

votes

**1**answer

268 views

### Pure first order logic formulations of Markov's principle

Markov's principle is a statement of constructive arithmetic that allows classical reasoning on formulas of the shape $\exists x P$ when $P$ is a recursive predicate:
$\neg \neg \exists x P \to \...

**6**

votes

**2**answers

859 views

### What exactly is a judgement?

Before formulating my question, let me briefly sum up what I know about the topic (feel free to correct me if something I claimed is false!). This is for you good to see what my state of knowledge is, ...

**8**

votes

**3**answers

482 views

### What is the definition of computational content?

I am interested in type theory and proof theory. I have read a lot of papers and books that use the term "computational content" (For example: https://scholar.google.com/scholar?hl=en&q=%...

**3**

votes

**1**answer

235 views

### Are there types with nontrivial paths in all dimensions? (HoTT)

I'm trying to construct a model of homotopy type theory, and in my development it seems like it would be helpful to assume that all types only have trivial paths below a given level (forgive my ...

**4**

votes

**0**answers

421 views

### New foundation in homotopy type theory

Is there any model of NF (New Foundations) on HoTT (homotopy type theory)?
Because there is a model of ZF(C) on HoTT (The HoTT book, Section 10.5) and NF on ZFC (by this Wikipedia articile), I think ...

**5**

votes

**1**answer

459 views

### Uniqueness Principle for function types

I am currently trying to understand the first chapter of the HoTT book and for 1.2 Functions Types of the book,
Since it is by definition ``the function that applies $f$ to its argument'' we ...

**14**

votes

**3**answers

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$...

**5**

votes

**1**answer

351 views

### What do we call this quantifier (“binder”)?

There's a quantifier ("binder", whatever), call it $\alpha$, defined as follows: $\alpha x.\tau$ is the (usually infinite) expression obtained by applying the substitution $\{x \mapsto \tau\}$ to the ...

**5**

votes

**0**answers

195 views

### Proper full submodels of full models of type theory

Let $N$ be the standard full model of the simply typed lambda calculus with infinite base type $o$ and let $X$ be an infinite and coinfinite subset of $N(o)$. I want to know if there's a full ...

**3**

votes

**0**answers

144 views

### Internal language type of power objects

It is a basic fact that in a category with finite limits the following are equivalent
Each object $X$ has a (membership relation to a) power object $PX\times X\hookleftarrow\ni_X$ subject to the ...

**3**

votes

**0**answers

202 views

### Understanding Strong Normalization for Identity Types in Martin-Löf Intensional Type Theory [closed]

Roughly, the strong normalization property for Martin-Löf Intensional Type Theory (MITT) tells us that every closed term $t$ of type $M$ will eventually reach a canonical normal form $t’$ such that it ...

**7**

votes

**1**answer

339 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-...