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

573 questions
Filter by
Sorted by
Tagged with
85 views

65 views

### In homotopy type theory, what is this "mechanical way to create a new expression F' now depending on t' and an equivalence between F(T) and F'(T')"? [closed]

I've read a few slides on the topic citing the following quotation from an email, which, according to these slides, defines the biggest advantage of homotopy lambda calculus over other caculi of ...
84 views

### λP2, the Calculus of Constructions, and quantifying over propositions

In $\lambda P2$, we can write polymorphic functions like $\Lambda A. \lambda x. x: \Pi A. A \to A$. By Curry–Howard, this corresponds to the proposition "for all propositions $A$, $A$ implies $A$&...
57 views

22 views

### Functors in List Reversal Natural Transformation

A common example of a natural transformation as it relates to CS/programming languages is list reversal. List is a functor from ...
78 views

### Reference request: is axiom of choice motivated along type-set lines?

Language: bi-sorted first order logic with equality and its axiom and additionally the extra-logical primitives: $\tau, < , \in"$, the first is a total unary function on sets denoting is the ...
34 views

### Product type in Type theory

I am new to type theory. It was explained that $\Pi$-type is like cartesian product of types. Firstly, in set theoretic formalization of mathematics, a function $f$ from $\mathbb{N}$ to $\mathbb{R}$ ...
30 views

### Some observations about third-order functionals: any relationships between them?

Let $X'$ denote $X \to X$. Here are some observations about third-order functionals over $\mathbb{N}$: They are the natural home of ordinal notations. In general, $f \in \mathbb{N}'$ can only be ...
70 views

### $\lambda$-calculus: find $F$ such that $FI = x$ and $FK = y$

I'm learning some $\lambda$-calculus using the following book: http://www.cse.chalmers.se/research/group/logic/TypesSS05/Extra/geuvers.pdf I'm having some trouble with exercise 2.12 (iii) on page 15. ...
42 views

53 views

### Truncation and fixed finite domain

Let $P$ be a type, $||P||$ denotes a mere proposition obtained by truncating $P$. Let $D$ be a type and $A:D\rightarrow\textsf{U}$, then $\Pi x:D.A(x)$ is a well-formed type. Assuming that we are ...
98 views

### How to go from Category Theory to Geometry?

I want to connect my knowledge of category theory and type theory to geometry, and I am wondering which theories I should learn. I know category/topos/type theory, but little other abstract algebra. I ...
1k views

### Function "evaluation" just means "composition"?

I am self-studying and have a basic or naive question that follows from a simple observation. I have also included tags for type theory, etc because "evaluation" probably has a different ...
104 views

### Why is the interval not a type but a pretype?

In Section 3.3 of Naive cubical type theory (Bruno Bentzen): We suggested above that every type is Kan. In fact, the interval is the only exception to this rule, since we have been implicitly ...
789 views

### Hierarchy in logical systems

I had an informal conversation in which I was told that logical systems could be intuitively drawn in a hierarchy according to their expressive power, i.e. the amount of things we can prove with them. ...
51 views

### Functions which are provably total in second order peano arithmetic

Girard has a representation theorem claiming: The functions representable in $F$ are exactly those which are provably total in second-order peano arithmetic $PA_2$. I believe the usual way to prove ...
55 views

In MLTT, by identifying propositions as types (and vice versa), a proposition carries the information regarding how a proof of the proposition is constructed. My question is related to this. Let $P:\... 1answer 56 views ### Truncation and$\Pi$-types (ii) I just read Ximei's post Truncation and$\Pi$-types. Can anyone explain in simple terms why ($\star$) implies ($\star\star$) but not vice versa. In other words, I wonder why ($\star$) is stronger than ... 1answer 83 views ### In homotopy type theory, prove that law of excluded middle implies reduction ad absurdum It's about Excercise 2 from here: While the principle of excluded middle$P\vee\neg P$( tertium non datur) is not provable, prove its double negation using the propositions as types translation:$\...
I am playing with impredicative type theories (CC and UTT). I am not quite familiar with the distinction between $\textsf{Prop}$ and $\textsf{Type}$ as it is not available in MLTT. Here is my question....
### Truncation and $\Pi$-types
Truncated types or bracket types are used to recover traditional logic within type theory. I have a question about truncating $\Pi$-types. The question is very basic. Let $A:\textsf{U}$ and \$B:A\...