# Questions tagged [type-theory]

The type-theory tag has no usage guidance.

**8**

votes

**0**answers

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

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

**7**

votes

**0**answers

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

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

**7**

votes

**0**answers

238 views

### Feasible Type Theories

I am looking for references about efficient type theories,
efficiency in the sense of computational complexity,
and type theory in the sense of Martin-Lof's type theories.
Has there been any studies ...

**6**

votes

**0**answers

150 views

### Preservation of universes in presheaves

In Lifting Grothendieck universes Hofmann and Streicher construct a universe in the category of presheaves over a small category given a Grothendieck universe in $\mathbf{Set}$.
Suppose now I have ...

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

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

**4**

votes

**0**answers

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

**4**

votes

**0**answers

115 views

### Problem with a proof in Wellfounded trees in categories

I'm reading the paper Wellfounded trees in categories by Moerdijk and Palmgren. I'm having trouble understanding the proof of Theorem 7.2 (page 216), i.e. that in $\mathbf{ML}_{< \omega} \mathbf{W}$...

**3**

votes

**0**answers

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

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

146 views

### Logical framework for type theories like ML and CIC

I'm looking for a logical framework in which it is possible to easily present both intensional and extensional theories of dependent types with a partially ordered set of universes à la Russell ...

**3**

votes

**0**answers

201 views

### An elegant formulation for typed sets

Fix a poset $T$, which we'll think of as a set of "types," interpreting $a \leq b$ as "$a$ is more general than $b$." Construct a category of TSet as follows.
Objects: Pairs ($X$, $\tau : X \...

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

**2**

votes

**0**answers

163 views

### Type theory: can multiple elimination rules be defined, in principle?

I'd like to ask a question on type theory:
Consider the usual type theoretical definition of the natural numbers. We could give an elimination rule in the form:
or in the form:
I called the ...

**1**

vote

**0**answers

81 views

### Natural relations between substitutions

Consider two contexts $\Gamma,\Delta$ (from some background type theory), and substitutions $s_1,s_2:\Gamma\rightarrow \Delta$. In the case of $1$-element contexts, we get that a substitution is ...