# Questions tagged [type-theory]

For questions about type theory, including normalization, dependent types, identity types, inductive types, universe types, functional programming languages, proofs as programs in simply-typed lambda-calculi, Martin-Löf's intuitionistic type theory or related.Consider using one of the following tags: (lambda-calculus), (logic), (constructive-mathematics),(homotopy-type-theory) if related.

655 questions
Filter by
Sorted by
Tagged with
723 views

### Approaching Type theory and Category Theory as a starting point in the study of mathematics?

I'm a Computer Engineering student, with interest in Type Theory and Category Theory and i have a more pedagogical/philosophical question about these areas. It seems that many researchers in Type ...
1 vote
47 views

### Typed logic vs many-sorted logic

I am confused as to what is the difference between many-sorted logic and typed logic. Are they the same thing? If not, what are the differences?
• 82
78 views

### Textbook of logic and sets based on type theory [closed]

Are there any textbooks on logic and sets at the level of prior knowledge to calculus that are based on type theory?
• 82
1 vote
27 views

34 views

### What do you call a function that maps within a type (or: space)

This question came up when I was trying to comment some code, but I think the language I'm looking for comes from category theory. Suppose I have f: X -> X, ...
• 11
78 views

### Why is $p$ a proof of $A$?

How do I see that "the logical proposition $A$ in (3) can be proved by the term $p$ in (4)"? What does it even mean that the term $p$ proves $A$ ? (Source of the screenshot: https://www.cs....
57 views

### Need help understanding $\alpha$-equivalence.

I am currently reading through Type Theory and Formal Proof. I see that there is some variation in the literature in the fine details on the discussion on how $\alpha$-equivalence is developed, such ...
• 1,041
36 views

### Universe CN and interpretation of "some"

From https://www.wiley.com/en-us/Formal+Semantics+in+Modern+Type+Theories-p-9781119489214 (pages 35-36): [...] CN is the universe of all (interpretations of) common nouns. As such, CN is the type ...
44 views

### Notational questions about rules in type theory

Definition of contexts from here. The first rule says that the empty tuple (or sequence) is a context. The second and third ones I don't exactly understand. I think the second has the premise "if ...
1 vote
122 views

### Proving that W-algebra homomorphisms are contractible

I don't understand the conclusion of the proof of Theorem 5.4.7 of the Homotopy Type Theory text and would like a more detailed explanation of how it works. Here's my attempt at divining an answer. ...
• 45
1 vote
119 views

### Category theory and types..?

I am reading "A Gentle Introduction to Category Theory - The calculational approach" , Marten M. Fokkinga. In the book often a word mentioned is of "typing" and if an expressio ...
• 9,988
43 views

### Foundations for learning LEAN

I am interested in learning LEAN. Visiting some forums and archives it seems that this uses type theory. Specifically, the "calculus of inductive constructions" is mentioned. I have ...
• 1,060
162 views

### If a type is an object and a function is a morphism. How to interpret a value in programming?

I've been reading Bartoz's "Category Theory for Programmers", and one question came to mind. In programming, types are objects and functions are morphisms. A functor is then a way to ...
• 2,752
170 views

### The first-order metatheory of HoTT

Does there exist a (say, simply typed) first-order theory which axiomatizes a universe of $\infty$-groupoids, in a similar manner to how ZFC can be considered as an axiomatization of the universe of ...
• 41
77 views

• 355