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

605 questions
Filter by
Sorted by
Tagged with
65 views

### 2-categorical universal property of the classifying category of a type theory

For example let us say we are in the setting of cartesian closed categories and the simply typed $\lambda$-calculus. Let $\mathtt{strCCCat}$ denote the $2$-category of strict cartesian closed ...
• 1,368
61 views

### Proofs and Types: Girard's remarks on Theoretical Computing

In the first chapter of Girard's Proofs and Types (1989) one finds the following remarks: Theoretical Computing is not yet a science. Many basic concepts have not been clarified, and current work in ...
• 1,707
46 views

### Type Theory: solution to paradoxes?

It’s my understanding this causes Russell paradox: $L = \{x : \lnot( x \in x)\}$ ZFC solution is to restrict comprehension. I also understand that Russel created Type Theory to solve the paradox. How ...
• 939
56 views

### Isomorphism vs. equivalence of types and homotopy vs. equality of functions

I am trying to build an understanding of the Univalence Axiom in HoTT and I am slightly confused about some definitions. If I was asked after reading of Chapter 1 of the HoTT book to formulate a ...
• 2,688
1 vote
61 views

### $\omega$ incompleteness of $\lambda$ calculus

In Plotkin's 'The $\lambda$-Calculus is $\omega$-Incomplete' (The Journal of Symbolic Logic Vol. 39, No. 2 (Jun., 1974), pp. 313-317), an example is given of two (untyped) $\lambda$-terms $M$ and $N$ ...
• 473
1 vote
65 views

### Using the Calculus of Constructions as a metalogic

Usually the Calculus of Construction is used via the Curry-Howard isomorphism, which makes it equivalent to intuitionistic first order logic. But what I am interested in is to use CoC as a metalogic ...
64 views

### Is type theory complete by definition?

From my understanding, type theory is its own deductive system, meaning that types have propositional meanings. Therefore, an element of a type appears to be an evidence of the truth of the ...
• 23
75 views

### Lean and inacessible cardinals

Here it is claimed that Lean's type theory is equiconsistent with ZFC + existence of $n$ inacessible cardinals for every natural $n$. This is a bit worrying if you just want to work with pure ZFC: how ...
• 41
97 views

### The double negation of excluded middle in type theory

Context The following question concerns plain Martin-Löf type theory, under a propositions-as-types interpretation: in particular, proposition simply means type and not mere proposition, and ...
• 5,917
138 views

### Is there a distinction between rules of inference and axioms in Homotopy Type Theory (HoTT)?

I'm taking rules of inference to be metalinguistic and to describe when you can write down a certain syntactic expression in the object-language given that you already have others written down (e.g. &...
40 views

• 23
1 vote
72 views

### Recursor and induction functions in dependent type theory

I'm reading HoTT book and I'm not sure if I really understand how the recursor function is related to the induction function. It is stated that product types are said to be : a degenerate example of ...
• 23
326 views

### Elimination rule for identity types in Martin-Lof Type Theory

The rule for identity type elimination still mystifies me, and I have not been able to find anything that satisfies me in any book. Consider, for example, the form of the rule on p. 112 of Thompson: \...
• 473
70 views

### If Cartesian product of sets becomes an internal hom in Rel what do functions become?

The category of relations between sets has an internal hom (Cartesian product). You have an isomorphism $$\textbf{Rel}(A, B \times C) \sim \textbf{Rel}(A \times B, C)$$ However, Rel is closed ...
92 views

### theorem for free: relation cartesian product

I am digging through a paper Theorems for free and a bit confused on the source of some conjectures (page 5): Is it an axiom or it can be implied from some other axioms? UPD Question is about ...
1 vote
121 views

### Type Theory: we cannot prove double negation, but can we prove it is unprovable?

I'm currently trying to learn type theory from the first chapter of HoTT. It is remarked that we cannot prove $\neg\neg A \rightarrow A$, when $A$ is interpreted as a proposition, or, equivalently, we ...
1 vote
66 views

### Propositional Uniqueness for Coproduct Types?

I'm working through the HoTT book and have just finished the section on coproducts. In short, I am wondering if there is a uniqueness principle for coproduct types. I can not find mention of one in ...
232 views

### Object Classifier implies Univalence in Type Theory?

There is a correspondence between univalence in Type Theory and object classifiers in $\infty$-toposes. This, for example, is suggested in the article Univalent Foundations for Mathematics on nlab. ...
• 73
304 views

### Impredicative Definitions (CZF)

CZF is touted as the predicative and constructive variant of ZF. This is because CZF avoids the fully impredicative axioms of powerset and full separation and alternatively because CZF has an ...
• 131
3k views

### Under the Curry-Howard correspondence or loosely "proofs-as-programs", do we also have "programs-as-proofs" and what would some arb. program prove?

Curry-Howard Correspondence Now, pick any 5-30 line algorithm in some programming language of choice. What is the program proving? Or, do we not also have "programs-as-proofs"? Take the ...
• 19.5k
81 views

### Is there a category-theoretic version of Girard's paradox?

Suppose, to approximate Girard's paradox, that we have a category whose collection of objects includes itself. Can we conclude that such a category has no initial object, or something similar? I don't ...
• 323
1 vote
97 views

### How to justify claims on the complexity of formal proofs without definitions, as described in "Type Theory and Formal Proof" by Nederpelt and Geuvers

In the chapter Definitions of "Type Theory and Formal Proof" by Nederpelt and Geuvers, they start with some motivating examples and then state (with my emphasis added) [T]here is also a ...
1 vote
67 views

### What does this typed lambda-calculus notation mean?

In Definition 3.2 (page 12) of Gallier's 'Constructive Logics Part I: A Tutorial on Proof Systems and Typed Lambda-Calculi' he sets out the rules for his typed $\lambda^{\to, +, \times, \perp}$-...
55 views

### What is a correct way to prove the next propositional logic statement using Curry–Howard correspondence?

I am studying Curry–Howard correspondence. Given propositional logic statement: (¬p -> q) -> ((¬p -> ¬q) -> p). I need to define a type (as proposition) ...
• 387
56 views

### Definition of ZFC2 (second order logic)

ZFC with 1st order logic is known. My question may be formulated either way What is the definition of ZFC2 (ZFC+second order logic)? (I assume that formulas also have quantifications of two kind over ...
• 704
94 views

### Can you define functions which are not primitive recursive, yet total, in Type Theory? [closed]

Ackermann's function is total but not primitive recursive. Can one define Ackermann's function in Type Theory, ie: Can you define functions which are not primitive recursive, yet total, in Type Theory?...
• 143
1 vote
161 views

### Ordinary mathematical uses of Axiom K

Context. In what follows, we work in Martin-Löf type theory (MLTT). We denote dependent product types by $\forall$, the identity type over a type $T$ by $\equiv_T$, and let $U$ stand in for arbitrary ...
• 5,917