**10**

votes

**1**answer

182 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

163 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$ ...

**5**

votes

**3**answers

351 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

445 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

199 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

206 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

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

**5**

votes

**2**answers

372 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

193 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

478 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

772 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

776 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

775 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

283 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

112 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

926 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

620 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

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

**33**

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

511 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

955 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

766 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

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