# Questions tagged [homotopy-type-theory]

The homotopy interpretation of constructive dependent type theory, the univalence axiom, higher inductive types, internal languages of higher toposes, univalent foundations for mathematics, and implementations of such theories in proof assistants.

**5**

votes

**1**answer

255 views

### Progress towards a computational interpretation of the univalence axiom?

I will preface this by saying that I am not an expert on type theory. I am just a curious outsider slowly making my way through the HoTT book when I (rarely) have some spare time.
I am just curious ...

**55**

votes

**4**answers

3k views

### Why did Voevodsky consider categories “posets in the next dimension”, and groupoids the correct generalisation of sets?

Earlier today, I stumbled upon this article written by V. Voevodsky about the "philosophy" behind the Univalent Foundations program. I had read it before around the time of his passing, and one ...

**7**

votes

**0**answers

307 views

### what's the point of cubical type theory?

I have been following through the development of homotopy type theory since 2013 because I was really interested in the foundation of mathematics. The novel idea of combining programming with homotopy ...

**3**

votes

**1**answer

209 views

### Definition of $(\infty,1)$-category in HoTT [duplicate]

Reading Lurie's Higher topos theory got me thinking, if we can think of $(\infty,1)-$categories as (1-)categories enriched over $\infty$-groupoid, then wouldn't the internal definition of an $(\infty,...

**4**

votes

**1**answer

285 views

### How much homotopy type theory should be modeled by the unstable motivic category?

It's often said that homotopy type theory should be interpretable in any $\infty$-topos. But really it should be interpretable in any "predicative $\infty$-topos". I'm not quite sure what this means, ...

**13**

votes

**2**answers

656 views

### What kind of category is generated by Cubical type theory?

What kind of ‘category’ is Cubical type theory the internal language of?
Its known that Martin-Löf type theories are the internal language of Locally cartesian closed categories, adding higher ...

**35**

votes

**2**answers

1k views

### Defining $SU(n)$ in HoTT

From a recent answer by Mike Shulman, I read:
"HoTT is (among other things) a foundational theory, on roughly the same ontological level as ZFC, whose basic objects can be regarded as $\infty$-...

**5**

votes

**3**answers

304 views

### (Co)limits of locally cartesian closed categories

Do locally cartesian closed $\infty$-categories form a presentable $\infty$-category? It seems like they should, and that the inclusion $\text{LCC}\rightarrow\text{Cat}$ preserves limits and maybe ...

**14**

votes

**1**answer

423 views

### Constructive homological algebra in HoTT

I'm curious how much of homological algebra carries over to a constructive setting, like say HoTT (or some other variety of intensional type theory) without AC or excluded middle. There doesn't seem ...

**10**

votes

**3**answers

600 views

### Can Homotopy Type Theory or algebraic geometry deal with homotopy fibers in terms of families?

((In conclusion)
It was hard to choose which answer to accept. I decided for the one which addressed most of the various aspects of the question.
)
(Later addon)
I now decided to put a bounty on ...

**5**

votes

**1**answer

126 views

### Models for Higher Inductive Types in Homotopy Type Theory

Ordinary inductive types is initial algebras for free monads. However, HITs are not initial algebras for endofunctors but presented monads.
From nLab, initial algebra of a presentable (infinity,1)-...

**17**

votes

**2**answers

739 views

### Stable homotopy type theory?

This is a combined question, strictly speaking I am asking three questions concerning, respectively, homotopy type theory, stable homotopy theory and Yetter-Drinfeld modules. But I believe in the ...

**1**

vote

**0**answers

99 views

### Synthetic type theory for virtual double category and its higher categories

For some monad T on a virtual equipment, the paper A unified framework for generalized multicategories by Cruttwell and Shulman (arXiv:0907.2460) proposes the normalized T-monoid.
Another paper, by ...

**77**

votes

**2**answers

5k views

### Vladimir Voevodsky's works

Vladimir Voevodsky has made several contributions in abstract algebraic geometry, focused on the homotopy theory of schemes, algebraic K-theory, and interrelations between algebraic geometry, and ...

**11**

votes

**1**answer

528 views

### The role of univalence in the homotopy interpretation of type theory

In Martin-Löf type theory with identity eliminator
$$
J :
\prod_{B:\prod_{x,y:A}(x=y)\to\mathcal{U}}\left(
\prod_{x:A}B(x,x,\mathrm{refl}_x)\to
\prod_{x,y:A}\prod_{p:x=y}B(x,y,p)
\right)
$$
...

**5**

votes

**2**answers

285 views

### Type Theory to Study $(\infty,n)$-Categories and $(r,n)$-Categories

The recent paper "A Type Theory for Synthetic $\infty$-Categories" proposes the syntax as the theory of the strict interval. In principle, any other suitable theory could be used instead. For instance,...

**1**

vote

**0**answers

484 views

### How can one define “punctured torus” in Homotopy Type Theory? Is its fundamental group the free product of the integers with themselves?

Questions.
Has the beautiful old idea, in part already known to Gauß, of a punctured torus surface (take, if you will, the classical set-theoretic definition as the meaning of the latter three words)...

**1**

vote

**1**answer

227 views

### Problems for a Homotopy excursion in HoTT

I would like to know some open problems in HoTT for Homotopy theorist (without knowledge of logic). With such a Homotopy theorist I mean someone who takes a serious reading ("at the level") of ...

**4**

votes

**3**answers

341 views

### Homotopy type theory: Are the hierarchy of Type_k universes isomorphic?

In homotopy type theory, or dependent type theories more generally, there is a "top-level" type called the universe, generally denoted $\newcommand{\type}{\mathtt{Type}}\type$. So for a concrete ...

**2**

votes

**1**answer

255 views

### Why are types in type theory unordered collections?

Please excuse my naïveté, I have no higher math education, just a curious observer. In type theories, types are treated as set-like because they're unordered collections. Yet, the putative motive in ...

**2**

votes

**1**answer

126 views

### Is the univalence of the canonical family over a universe small?

Working in Martin-Löf intensional type theory, $\mathsf{ITT}$, with a universe $U$ within the theory closed under all the usual constructors, the univalence of the canonical family $\mathsf{EI}$ over $...

**4**

votes

**1**answer

168 views

### The axiom $\Xi : \prod_{A:\mathcal{U}} \|A\| \to A$ and the $n$-truncation of a type

My question is whether the following has been considered as an axiom, and if so, where I may find a discussion of it:
$\Xi : \prod_{A : \mathcal{U}} \|A\| \to A$.
For example, using this axiom, we ...

**1**

vote

**1**answer

234 views

### Univalent Foundations and canonicity property are compatible?

I'm interested in HoTT, especially its application to foundations of mathematics.
I believe strongly that Univalent Foundations is the very foundation of mathematics.
So,I have a question.
(Q) ...

**1**

vote

**1**answer

205 views

### Help with simple homotopy type theory proof [closed]

I'm having some beginner problems understanding / proving simple facts about higher inductive type paths.
If you take this higher inductive type for natural numbers modulo 1:
...

**3**

votes

**1**answer

220 views

### Are there types with nontrivial paths in all dimensions? (HoTT)

I'm trying to construct a model of homotopy type theory, and in my development it seems like it would be helpful to assume that all types only have trivial paths below a given level (forgive my ...

**0**

votes

**0**answers

178 views

### The homotopy pullback of a point along itself is the loop space

I have seen on the nLab that we can view the loop space as a particular homotopy pullback, and that it is even the way a "loop space object" is defined in general (when it exists).
Can someone give ...

**3**

votes

**0**answers

387 views

### New foundation in homotopy type theory

Is there any model of NF (New Foundations) on HoTT (homotopy type theory)?
Because there is a model of ZF(C) on HoTT (The HoTT book, Section 10.5) and NF on ZFC (by this Wikipedia articile), I think ...

**4**

votes

**1**answer

434 views

### HoTT without Funext, Univalence

Are there any models of Martin-Löf's intensional type theory in which univalence or function extensionality fails?
In the HoTT book, axioms like $\mathsf{LEM}_{\infty}$ (in Section 3.4) are proved to ...

**5**

votes

**1**answer

369 views

### Uniqueness Principle for function types

I am currently trying to understand the first chapter of the HoTT book and for 1.2 Functions Types of the book,
Since it is by definition ``the function that applies $f$ to its argument'' we ...

**2**

votes

**1**answer

175 views

### Set truncations in homotopy type theory

We can define set truncation as a higher inductive type with the following constructors:
$|-|_0 : A \to ||A||_0$
trunc : $(a\ a' : ||A||_0)\ (p\ p' : a = a') \to p = p'$
If we replace the type of ...

**-2**

votes

**1**answer

274 views

### What constitutes “a path” in HoTT? [closed]

($I$ is the interval [0..1], the domain of all paths in HoTT.)
($2$ is the type of two elements, named here as $0_2$ and $1_2$.)
Define a map $p : I \rightarrow 2$ by $p(0) = 0_2$ and $p(x) = 1_2$ ...

**14**

votes

**1**answer

458 views

### Why the reflection rule trivializes higher paths in Martin-Löf Extensional Type theory?

Martin-Löf Extensional Type theory differs from its intensional counterpart in that it contains the so-called reflection rule that says that if $p : x = y$, then actually $x \equiv y$ (i.e. $x$ and $y$...

**0**

votes

**1**answer

142 views

### Construction of the necklace by homotopy type theory [closed]

The necklace can be obtained from a circle by attaching $n$ 2-spheres $S^2$ along arcs, so the necklace $N(n,S^1,a_i)$ is homotopy equivalent to the space obtained by attaching $n$ 2-spheres $S^2$ to ...

**10**

votes

**1**answer

581 views

### What is an Elementary “Homotopy, Model” Topos?

Context:
Def (Rezk): A (Grothendieck) homotopy topos is a homotopy left exact Bousfield localization of the model category of simplicial presheaves sPsh(C) on a small simplicial category C.
Thm (...

**13**

votes

**1**answer

689 views

### Practical advantages of univalent foundations

I'm interested in the machine translation of mathematics from informal to formal (a la Ganesalingam in The Language of Mathematics). As a first step, I am designing a computer language for expressing ...

**9**

votes

**0**answers

241 views

### Is there a definition of an $\infty$-groupoid in HoTT whose terms are $n$-manifolds and whose higher morphisms are diffeomorphisms/isotopies/etc?

Suppose you want to work with TQFTs in homotopy type theory (HoTT). Working with $(\infty,n)$-categories, or even $(\infty,1)$-categories, is something that I gather is too difficult for HoTT at the ...

**3**

votes

**1**answer

246 views

### Defining equivalence of equivalences without assuming extensionality

In homotopy type theory, we say that a function $f$ is an equivalence between two types $A$ and $B$, if the inverse image of all points is contractible (as per say the n-lab or Paolo's Capriotti's ...

**23**

votes

**3**answers

1k views

### What technical and/or theoretical challenges are involved in automatically extracting proofs from books and papers into Coq code?

Over the years, advances in machine learning has allowed us to communicate and interact, using the same natural language, more and more semantically with computers, e.g. Google, Siri, Watson, etc. On ...

**16**

votes

**1**answer

3k views

### What is the most transparent, rigorous definition of the Univalence Axiom?

I've been studying homotopy type theory and trying to grasp the Univalence Axiom. I have yet to find a concise, accessible, rigorous definition of Univalence. I have several excellent survey papers ...

**1**

vote

**1**answer

369 views

### Functional programing and intensional type theory

I know very little about how computers work, so please excuse my ignorance!
I think of the Glasgow Haskell Compiler as a program that eats up extensional type theory and spits out a program which ...

**4**

votes

**1**answer

321 views

### Is the infinity-groupoid of a finite CW complex finitely-presented?

An infinity-groupoid is finitely-presented when it is equivalent to the free infinity-groupoid on a finite family of generators, possibly of different dimensions.
Is the infinity-groupoid of a finite ...

**30**

votes

**1**answer

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

**8**

votes

**1**answer

284 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} : \mathsf{...

**13**

votes

**4**answers

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

**13**

votes

**1**answer

828 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

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

**7**

votes

**3**answers

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

**4**

votes

**1**answer

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

**5**

votes

**2**answers

466 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.
http://www....

**9**

votes

**2**answers

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