# Questions tagged [type-theory]

The type-theory tag has no usage guidance.

109
questions

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

**2**

votes

**0**answers

180 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

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

**1**

vote

**0**answers

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

**0**

votes

**1**answer

276 views

### Does “Church's Law” really fail in Extensional Type Theory?

Last year Bob Harper wrote a blog post about the failure of "Church's Law" in Extensional Type Theory[1]. However his statement of the law looks to me more like an internal version of the statement "...

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

**1**answer

467 views

### prod and sig in COQ

Hello,
Apparently in COQ the type prod (with one constructor pair) corresponds to cartesian product and the type sig (with one constructor exist) to dependent sum but how is described the fact that ...

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

**-1**

votes

**5**answers

853 views

### finding cutting edge papers and books

Hi all,
what are the best strategies to find cutting edge papers and books on a field of mathematics?
..
Example:
2-3 years ago I had to analyze a time series. I found a paper and showed that to ...