Questions tagged [type-theory]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
2
votes
0answers
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
0answers
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
1answer
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
0answers
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
1answer
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
1answer
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
1answer
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
0answers
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
5answers
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 ...