# Tagged Questions

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

1answer
41 views

### Are the 1 dimensional loop spaces in homotopy type theory commutative?

Theorem 2.1.6 of the Homotopy Type Theory book proves that $\Omega^{2}A$ is always commutative, using a similar argument to the one used for loop spaces in algebraic topology. Isn't it also the case (...
1answer
83 views

### Categorical semantics explained – what is an interpretation?

I’ve been really having a hard time trying to understand categorical semantics. In fact, I am confused to the point I am afraid I don't know how to ask this question! I’ve been reading textbooks like ...
2answers
83 views

1answer
78 views

### Is there a sense in which a formal theory can be more or less “metamathematically aware”?

For example, in classical logic, because of the law of the excluded middle, all propositions must be true or false, so in order to prove that a proposition is actually independent of the theory, we ...
2answers
113 views

### Definition of “set” in HoTT

In the homotopy type theory book (https://hott.github.io/book/nightly/hott-online-1007-ga1d0d9d.pdf) "set" is defined as follows (see chapter 3): Definition 3.1.1. A type A is a set if for all x, y : ...
1answer
69 views

### Is the 1-tuple (x) = x?

Based on following sentence In type theory, commonly used in programming languages, a tuple has a product type; this fixes not only the length, but also the underlying types of each component. ...
0answers
53 views

0answers
88 views

### Turning ZFC into a free typed algebra

The standard way of using ZFC to encode the rest of mathematics is sometimes criticized because it introduces unnecessary, strange properties such as, for example $1\in 2$ if we encode integers by ...
1answer
66 views

### The sections of the projection $\bigsqcup_{i:I} X_i \rightarrow I.$

I just noticed something funky. Let $X$ denote an $I$-indexed family of sets. There is a projection $$\pi_X: \bigsqcup_{i:I} X_i \rightarrow I.$$ It isn't necessarily surjective, of course, because ...
0answers
34 views

### Structural induction over types that accept functions, in Coq

If you define an inductive type in Coq with a constructor that accepts a function mapping to that type, you get a somewhat odd induction rule. ...
1answer
56 views

### Why is the rule “If x has type σ in the context, we know that x has type σ” needed?

I am trying to get a deeper understanding of why the rules in logic and type theories exist, and am now looking at the simply typed lambda calculus, the typing rules on Wikipedia. The first one is ...
0answers
33 views

### Disequality in Type Theory [duplicate]

Is it possible to prove $0 \neq 1$ in (non-univalent) Martin-Löf type theory, where $0$ and $1$ are natural numbers (defined using the usual inductive type $0 : \mathbb{N}$, \$S : \mathbb{N} \to \...