# Questions tagged [type-theory]

The tag has no usage guidance.

9 questions
Filter by
Sorted by
Tagged with
1 vote
130 views

### Can set elements be predicated of objects?

If we define a set as a cartesian product of properties, do you think that the cartesian product can be predicated of an object? For example if we define: Set of names of Captials N = { The name ...
• 1,143
52 views

### Definite description in homotopy type theory

In a paper by David Corfield, we have an account of definite description in homotopy type theory. The author gives the following rule: Then we can describe the rule of what we might call the ...
• 131
80 views

### Theory build on the top of a Logic

Could somebody elaborate the meaning of following statement from wikipedia concerning intrinsical differences between set theory and type theory: Unlike set theories, type theories are not built on ...
• 161
1k views

### 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 ...
104 views

### 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. ...
• 61
130 views

### 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 ...
• 161
225 views

### 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 ...
• 1,143