12

My question is related to the formal presentation of type theory as stated in the context of Homotopy Type Theory. Every formalization is grounded on typing judgements like $$ a: A $$ where mostly it is said that $a$ is an object that can be built due to several formation or term-forming rules and $A$ is a Type. But are types and objects different layers or is every type in some sense also a term. So in conclusion: Is there only one base class of mathematical entities in general?

I'm aware that the objects above are proofs. What confuses me mostly is that for the universe hierarchy postulated one has $$ U_n : U_m $$ for $n<m$. Statements of the form $$A : B$$ with $A$ and $B$ types suggest me to believe that there is no distinction between proofs and Types. Is this the correct point of view?

Addendum, 01.01.2015: I think the "homotopy perspective" is also a clue for that - if one assumes that points of a space can be regarded as spaces itself in some sense.

Update, 02.01.2015

I have found a very nice answer on CS SE. Roughly spoken the answer is: Depending on the type theory used, there is no distinction (or there is). To quote the answer there:

There are type systems that go further and completely mix types and base terms, so that there is no distinction between the two. Such type systems are said to be higher-order.

So my question reduces to: Is it true that in Martin-Löf Type Theory, which HoTT is based on, there is no distinction between terms and types?

Community
  • 1
Robin Stammer
  • 765
  • 2
    Yes, it is true that types are terms – they are terms of type $\mathsf{Type}$ (or $\mathcal{U}$, if you prefer). There is no need to bring in the "homotopy perspective". – Zhen Lin Jan 02 '15 at 01:18
  • 1
    Dear Robin: $+1$ for your interesting question! Did you see the word object in the book? - I'm not sure but I'd say that the words term and type are synonymous, and that an expression of the form $p:a=_Ab$ might be read as "$p$ is a proof of the propositional equality of $a$ and $b$ in $A$", but the book prefers (in such a situation) to use words such as evidence and witness instead of proof. (Note that $a=_Ab$ is a type.) – Pierre-Yves Gaillard Jan 02 '15 at 07:12
  • 1
    Thanks for your helpful comments. You're right, the HoTT book uses consequently term. I'd use it in general, too. It was the sentence on page 538 in Appendix A that left me unsure about the situation: "The objects and types of our type theory may be written as terms". Because of that formulation I used "object". Second, this sentence clarifies that types are presented as terms, alright. So to answer the question I had: Every entity is presented as term. Conversely, every term is of some type, whereas its type is presented as a term, too. So there are only types in general.Do you agree? – Robin Stammer Jan 02 '15 at 12:05
  • @RobinNeumann: You're welcome! (Please insert an @Pierre-Yves when writing to me. I found your comment by chance.) I interpret the sentence you quoted as meaning "the objects of our theory are called terms or types". If $t$ and $u$ are terms, I'd say that $t:u$ is a proposition, and, if $\Gamma$ is a context, that $\Gamma\vdash t:u$ is a judgment. I'd also say that a formula is a term, a proposition or a judgment. (Of course, there are other propositions and judgments.) Again, I'm not sure at all... – Pierre-Yves Gaillard Jan 02 '15 at 12:51

1 Answers1

10

"Martin-Lof type theory" is, unfortunately, not a completely unambiguous designator of a type theory. However, in the type theory used in the HoTT book, it is true that types are particular terms, namely terms whose type is a universe. (Of course, not every term is a type.) In other closely related type theories, types are not particular terms; instead there is an operation "El" (for "elements of") which maps terms-whose-type-is-a-universe to types. The first version is sometimes referred to as a "universe a la Russell", and the second (with "El") as a "universe a la Tarski". Russell universes are often more convenient to use, but Tarski universes have some formal advantages, due to the fact that they don't "mix levels" between types and terms.

Mike Shulman
  • 4,794