**22**

votes

**1**answer

554 views

### Homotopy Type Theory: What is it?

My question is, broadly, what is the main project of Homotopy Type Theory (HoTT). I asked a professor who is likely to be correct and he say the following:
There are three directions:
...

**2**

votes

**0**answers

104 views

### Can someone elaborate on a categorical/homotopical point made in the proof that $\Sigma 2 = S^1$, given in the HoTT book? [migrated]

In chapter 6, specifically in the section about suspensions a proof is given that $∑2 = S^1$.
The book says that $\mathrm{transport}^{x \mapsto g(f(x)) = x}(\mathrm{refl}_N, \mathrm{merid}(y)) = ...

**7**

votes

**1**answer

165 views

### How to proceed with a type-theoretic proof that $\Sigma \mathbb{S}^1 \simeq \mathbb{S}^2$?

The circle can be define with a higher inductive type as follows:
The space $\mathbb{S}^1$ is freely generated by the following constructors:
$\mathsf{b} : \mathbb{S}^1$ and $\mathsf{loop} : ...

**10**

votes

**4**answers

472 views

### The groupoid of algebraic expressions and proofs

Fix a set of variables $V$, and suppose we're given a presentation of a monosorted algebraic theory, with variable symbols taken from $V$. For the sake of example, suppose the presentation consists of ...

**10**

votes

**1**answer

230 views

### What would be an infinity-groupoid analogue of the duality between sets and complete atomic boolean algebras?

Consider the object classifier of the $\infty$-topos of $\infty$-groupoids. For the role it plays in homotopy type theory as the type of types, let’s denote it as $Type = \coprod_{[F]} B Aut(F)$, the ...

**8**

votes

**1**answer

181 views

### Base change in homotopy type theory

Recall that with the internal language of 1-toposes, we have the nice, basic, and useful result that geometric sequents are stable under base change along geometric morphisms: If $\varphi$ and $\psi$ ...

**6**

votes

**3**answers

369 views

### Extensionality in HoTT versus extensionality in internal language of a category

What's the extension of judgmental identity in HoTT (homotopy type theory)?
The Martin-Löf intensional dependent type theory with identity types is called (definitionally) extensional if the ...

**3**

votes

**1**answer

468 views

### Delooping in homotopy type theory

In algebraic topology, it is a theorem of Stasheff that every A-$\infty$ space has the homotopy type of a loop space.
Question: Is this true in homotopy type theory?
Let me be a little more ...

**4**

votes

**2**answers

209 views

### Question about higher inductive types and computational rules

I have been trying to make my way through the homotopy type theory book, slowly but surely, and I just finished reading this introductory series of 3 articles on hott on ScienceForAll.
...

**8**

votes

**2**answers

239 views

### How should I be thinking about object classifiers / universal fibrations / universes?

I have been learning about homotopy type theory this summer. I am not a homotopy theorist but I am more comfortable with homotopy theory than I am with type theory, so the way I rationalize many of ...

**1**

vote

**1**answer

197 views

### Analogy between variable substitution and the moving lemma

While reading the HoTT book, I came up with the following (very) vague analogy:
Consider $f(x) :\equiv \lambda y.x+y$ of type, say, $f: \mathbb{N} \to \mathbb{N} \to \mathbb{N}$. Also assume you ...

**6**

votes

**2**answers

391 views

### A pointless circle in HoTT

In the beginning of chapter two in The HoTT Book there is a discussion about synthetic vs. analytic geometry:
An important difference between homotopy type theory and classical homotopy theory is ...

**1**

vote

**0**answers

197 views

### A potential definition of weak $\omega$-categories

This question was inspired by the Homotopy Type Theory Book.
Might we define a weak $\omega$-category as described below?
Is any similar approach already considered in the literature?
Let ...

**6**

votes

**3**answers

504 views

### Are paths in HoTT perhaps just “cost-free” paths?

Homotopy type theory (HoTT) doesn't seem to say anything about "mutations" of values in type $T$, an important concept in computer science. Mutations occur when you "change a value" of some variable ...

**23**

votes

**2**answers

795 views

### How do you define (infinity,1) categories in Homotopy Type Theory?

One of the major motivations of Homotopy Type Theory is that it naturally builds in higher coherences from the beginning. One important setting where higher coherence requirements get annoying is ...

**12**

votes

**2**answers

801 views

### What is the status of (universal) algebra in type theory?

With the recent interest in homotopy type theory as a foundation for mathematics, it seems natural to develop algebra within the framework of type theory. So far, I can't find much literature ...

**11**

votes

**4**answers

787 views

### How do you define the strict infinity groupoids in Homotopy Type Theory?

In the setting of Homotopy Type Theory, how would you construct $\mathrm{isStrict} : U \rightarrow U$ which is inhabited exactly when the first type is (equivalent to?) a strict $\infty$-groupoid?
...

**6**

votes

**1**answer

301 views

### The independence of path induction

In §1.12 of the Homotopy type theory book, it is mentioned that indiscernibility of identicals is a consequence of path induction. More precisely, for each type $C$ dependent over a type $A$, there is ...

**2**

votes

**1**answer

119 views

### Does the induction principle of the type of booleans imply its recursion principle?

The type of booleans, denoted by ${\mathbf{2}}$, has two terms $0_{\mathbf{2}}:{\mathbf{2}}$ and $1_{\mathbf{2}}:{\mathbf{2}}$. The induction principle of ${\mathbf{2}}$ states that, given a dependent ...

**8**

votes

**2**answers

992 views

### A (very naive) question about Homotopy Type Theory

In homotopy type theory, homotopy types can be viewed as logical types and it is possible to prove some theorems about them without using any underlying space (no simplicial set, no topological ...

**13**

votes

**2**answers

637 views

### $\infty$-categorical interpretation of type theory

One can read at several places that Martin-löf type theory should be the internal language of a locally Cartesian closed infinity category, and that the univalence axiom should distinguished infinity ...

**13**

votes

**3**answers

616 views

### What are finite homotopy types?

Starting from an ordinary 1-categorical point of view, there are various obvious candidate definitions for ‘finite homotopy type’:
The homotopy type of a simplicial set that has only finitely many ...

**34**

votes

**9**answers

2k views

### Homotopy as a general organizing principle

One of the realizations that led to the development of Homotopy Type Theory (HoTT) is that the ideas of homotopy theory have very broad applicability in mathematics. Indeed, Quillen model categories ...

**10**

votes

**2**answers

523 views

### Are simplicial sets the intended model of HoTT?

While thinking about Jason Rute's question, I wondered if there was an intended model for HoTT. The main candidate for the intended model are simplicial sets, where Vladimir Voevodsky first observed ...

**16**

votes

**2**answers

995 views

### Prospects for reverse mathematics in Homotopy Type Theory

Reverse mathematics, as I mean here, is the study of which theorems/axioms can be used to prove other theorems/axioms over a weak base theory. Examples include
Subsystems of Second Order Arithmetic ...

**8**

votes

**2**answers

784 views

### Equivalent form of the Univalence Axiom

I'm reading the new HoTT book and I'm wondering about a potential equivalent form of the Univalence Axiom: $(A \simeq B) \simeq (A = B)$.
For simplicity, I'm tacitly working in a fixed universe. It ...

**10**

votes

**1**answer

1k views

### Forcing in Homotopy Type Theory

I apologize if this question doesn't make any sense. I'll just go ahead and delete it if that's the case. But the question is just the title. Is there a notion of forcing in homotopy type theory? ...

**5**

votes

**1**answer

939 views

### categorifying induction in homotopy type theory

In trying to understand homotopy type theory, I stumbled upon the following silly question, which is likely to be trivial for the experts.
Let $B=\sqcup_{n\in\Bbb N} BS_n$, which I'd like to think of ...