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.
134
questions
80
votes
2
answers
7k
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 ...
66
votes
4
answers
5k
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 ...
44
votes
9
answers
3k
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 ...
44
votes
1
answer
8k
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:
...
38
votes
3
answers
3k
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 ...
35
votes
3
answers
2k
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$-...
32
votes
1
answer
2k
views
Deligne's doubt about Voevodsky's Univalent Foundations
In a recent lecture at the Vladimir Voevodsky's Memorial Conference, Deligne wondered whether "the axioms used are strong enough for the intended purpose." (See his remark from roughly minute 40 in ...
25
votes
1
answer
1k
views
Coinduction for all?
Every undergraduate in mathematics learns about proofs by mathematical induction. Moreover, every undergraduate taking a course in theoretical computer science or logic learns about inductive ...
25
votes
0
answers
4k
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 ...
24
votes
3
answers
2k
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 ...
23
votes
2
answers
2k
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 (...
23
votes
1
answer
4k
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 ...
21
votes
2
answers
1k
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 ...
20
votes
2
answers
2k
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 ...
20
votes
2
answers
739
views
Small complete categories in HoTT+LEM
Freyd's theorem in classical category theory says that any small category $\mathcal{C}$ admitting products indexed by the set $\mathcal{C}_1$ of all its arrows is a preorder. I'm interested in whether ...
19
votes
5
answers
2k
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?
...
19
votes
3
answers
1k
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 ...
17
votes
4
answers
2k
views
Practical example in using (homotopy) type theory
I have just read Grayson's introduction on homotopy type theory as a possible foundation for mathematics. It is very enlightening about what all the fuss is about, but I am left with some doubts. ...
17
votes
2
answers
1k
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 ...
17
votes
2
answers
1k
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 ...
17
votes
1
answer
3k
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? ...
17
votes
1
answer
1k
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 ...
16
votes
2
answers
796
views
Appearance of proof relevance in "ordinary mathematics?"
I've been wondering recently what—if any—applications proof theory has to ordinary mathematics (by which I mean algebra, analysis, topology, and so on). In particular, I'd be fascinated to see a proof ...
15
votes
3
answers
911
views
Role of univalence in homotopy group calculations
This book has a section with proofs of the fact $\pi_1(S^1)=\mathbb Z$ using the univalence axiom. They are a bit too technical for me at the moment to read, but I want to understand the following (...
15
votes
2
answers
2k
views
Formal definition of homotopy type theory
The HoTT community is quite friendly, and produces many motivational introductions to HoTT. The blog and the HoTT book are quite helpful. However, I want to get my hands directly onto that, and am ...
15
votes
2
answers
2k
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 ...
15
votes
2
answers
633
views
How to formulate the univalence axiom without universes?
The standard formulation of the univalence axiom for a universe type $U$ is that, for all $X : U$ and $Y : U$, the canonical map $(X =_U Y) \to (X \simeq Y)$ is an equivalence.
As we (usually) cannot ...
14
votes
1
answer
614
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$...
13
votes
4
answers
839
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
633
views
What is meant by a computational interpretation of univalence?
In homotopy type theory the univalence axiom implies function extensionality.
Suppose we have a recursive set we are not sure is empty (e.g. the set of even integers$\geq 4$ that are not a sum of two ...
13
votes
1
answer
1k
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 ...
12
votes
1
answer
643
views
3 questions about basics of Martin-Löf type theory
I started to read the HoTT book. I'm now on chapter 1 and I have several questions concerning not even homotopical, but "regular" type theory.
On page 24, where the universes are introduced,...
12
votes
1
answer
867
views
Are the “topologies” arising from constructive type theories with quotients actually condensed sets?
This is the second in a pair of questions. For the other see Are representations in computable analysis the equivalent to countably-generated condensed sets?.
Dustin Clausen and Peter Scholze have a ...
11
votes
3
answers
906
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 ...
11
votes
3
answers
1k
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 ...
11
votes
1
answer
728
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)
$$
...
11
votes
3
answers
692
views
natural metrics for proof length
I am trying to make my way into Homotopy Type Theory(HoTT) where a mathematician may view proofs as paths. Intuitively, this leads me to the idea of a metric on the space of mathematical propositions. ...
11
votes
2
answers
1k
views
Soft question: Deep learning and higher categories
Recently, I have stumbled upon certain articles and lecture videos that use category theory to explain certain aspects of machine learning or deep learning (e.g. Cats for AI and the paper An enriched ...
11
votes
1
answer
811
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 (...
10
votes
2
answers
991
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 ...
10
votes
1
answer
1k
views
Why are W-types called "W"?
Why are W-types called "W"?
Probably "W" means either "wellordered" or "wellfounded". (Martin-Löf uses the term "wellorder".) But these are notions ...
10
votes
1
answer
573
views
How to proceed with a type-theoretic proof that $\Sigma \mathbb{S}^1 \simeq \mathbb{S}^2$?
The circle in homotopy type theory $\mathbb{S}^1$ is a higher inductive type freely generated by the following constructors:
$\mathsf{b} : \mathbb{S}^1$ and $\mathsf{loop} : \mathsf{b} = \mathsf{b}$.
...
10
votes
0
answers
309
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 ...
9
votes
2
answers
2k
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 space)....
9
votes
1
answer
769
views
Practical Benefits of HTT/univalent foundations for assisted proofs
I'm trying to understand what the claimed practical benefits of HTT/univalent foundations are for doing computer assisted proofs and while I've seen a lot of claims of benefits they all seem to be ...
9
votes
2
answers
785
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 ...
9
votes
2
answers
1k
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 ...
9
votes
1
answer
442
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$ ...
8
votes
2
answers
1k
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 ...
8
votes
1
answer
619
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 ...