Questions tagged [type-theory]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
8 votes
4 answers

Is there anything more fundamental than quantification?

In the prevailing view of the concept of "Existence," it is well-known that it isn't a property of individual objects, but rather a property of properties. As Frege would put it: It is a ...
Johnathan Green's user avatar
4 votes
1 answer

Demonstrate that a term cannot be well-typed?

This problem is coming from Exercise 3.3 in Bacon's A Philosophical Introduction to Higher-order Logics. I am trying to do my due-diligence here and not skip problems, but this one stuck out to me. ...
C D's user avatar
  • 61
0 votes
2 answers

Internal vs External Statement in Homotopy Type Theory

I would like to clarify the precise difference between the phrases "statement inside/ internal the theory" and "statement about the theory" in context of Homotopy Type Theory. A ...
user267839's user avatar
3 votes
1 answer

Can abstract concepts be represented by types in mathematics?

I am reading about type theory along with abstraction and am wondering how they relate. Am i right in thinking that an abstract concept (from the result of abstraction) can be represented by a type in ...
Richard Bamford's user avatar
15 votes
7 answers

Why do universities not teach constructive mathematics to CS undergraduates?

I had a conversation with a user on the Internet. And it did indeed wake my interest regarding something that I had also been asking myself long ago. Why do so many universities still teach beginners ...
Tetragrammaton's user avatar
0 votes
2 answers

Are mathematical objects a type according to type-theory?

I've been thinking about mathematical objects as a metaphysical trope, and the idea of them existing as a type has a few issues for me. Mainly the response to this question is similar to what I've ...
Confused's user avatar
  • 1,123