# Questions tagged [type-theory]

The type-theory tag has no usage guidance.

**8**

votes

**0**answers

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

**6**

votes

**2**answers

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

**6**

votes

**2**answers

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

**43**

votes

**7**answers

8k views

### How true are theorems proved by Coq?

Less tongue in cheek, is it known what the relative consistency is for theorems proved with an automatic theorem prover? Of course this depends somewhat on what assumptions one makes with respect to ...

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

**6**

votes

**1**answer

366 views

### $\Pi$, $\Sigma$, and identity types without $\eta$ in comprehension categories

In comprehension categories, dependent sums are defined as a choice of left adjoints for all reindexing functors along display maps, satisfying a Beck-Chevalley condition. Dependent products are ...

**3**

votes

**0**answers

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

**12**

votes

**1**answer

518 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

288 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

318 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

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

**10**

votes

**4**answers

928 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

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

**2**

votes

**1**answer

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

**13**

votes

**2**answers

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

**2**

votes

**0**answers

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

**2**

votes

**0**answers

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

**3**

votes

**2**answers

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

**12**

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

**6**

votes

**1**answer

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

**16**

votes

**1**answer

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

**1**

vote

**1**answer

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

**11**

votes

**3**answers

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

**3**

votes

**0**answers

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

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

**5**

votes

**1**answer

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

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

**5**

votes

**0**answers

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

**7**

votes

**3**answers

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

**7**

votes

**0**answers

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

**6**

votes

**1**answer

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

**7**

votes

**2**answers

616 views

### Identity types: What makes Intuitionistic Type Theory *intuitionistic*?

In the opening passage of Martin-Löf's (1975) he famously says that
"the theory of types with which we shall be concerned is intended to be a full scale system for formalizing intuitionistic ...

**4**

votes

**3**answers

352 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

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

**18**

votes

**1**answer

3k views

### What is the most transparent, rigorous definition of the Univalence Axiom?

I've been studying homotopy type theory and trying to grasp the Univalence Axiom. I have yet to find a concise, accessible, rigorous definition of Univalence. I have several excellent survey papers ...

**3**

votes

**1**answer

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

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

**18**

votes

**3**answers

1k views

### How do we express measurable spaces using type theory?

A measurable space $(X,\mathcal X)$ consists of a set $X$ equipped with a $\sigma$-algebra of subsets $\mathcal X$. I would like to write computer programs involving measurable spaces, but to the best ...

**8**

votes

**0**answers

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

**6**

votes

**2**answers

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

**6**

votes

**1**answer

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

**5**

votes

**2**answers

713 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

445 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

226 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

398 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

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

**5**

votes

**1**answer

341 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

193 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

133 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

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