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.
135
questions
7
votes
2
answers
339
views
Explicit different proofs of the same identity type in MLTT
This question is similar to (but more specific than) this one: When are two proofs of the same theorem really different proofs
I do not know very much about homotopy type theory, but I am trying to ...
- 173
12
votes
1
answer
644
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,...
- 1,294
1
vote
1
answer
265
views
Cohomology with local coefficients in homotopy type theory
I was just reading Mike Shulman's blog post on how to define cohomology in homotopy type theory (HoTT), and I was curious if we can similarly define cohomology with local coefficients in HoTT as well?
...
- 5,933
2
votes
1
answer
889
views
What do UF and ZF do to each other?
(By request from a comment: UF stands for Univalent Foundations)
Correct me if I'm wrong, but in a model $M$ of ZF each element $x$ of $M$ should produce a directed-graph-with-a-marked-sink $G_x$ ...
- 17.5k
3
votes
1
answer
399
views
Applications of opetopes
I've been reading about coherence problems in homotopy type theory (regarding semisimplicial sets and a raw syntax interpreter), and I've seen a remark about higher-dimensional operads perhaps being ...
- 165
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 ...
- 5,038
5
votes
1
answer
446
views
Defining (infinity,1)-categories in HoTT using only an interval type
In this article, Emily Riehl and Michael Shulman describe a type theory in which one can do $\infty$-category theory synthetically. Their framework allows them to define simplices $\Delta^n$, and a ...
- 556
11
votes
3
answers
693
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. ...
- 3,827
16
votes
2
answers
801
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 ...
- 177
6
votes
0
answers
156
views
Inductive type constructors with the defined type appearing in non-strictly positive position
In the HoTT book §5.6 ‘The general syntax of inductive definitions’ there is a proof that the existence of an inductive type $T$ with a constructor $t : ((T \to \mathsf{Prop}) \to \mathsf{Prop}) \to T$...
- 192
5
votes
1
answer
125
views
Considering each half of factorization of weak equivalence separately
I have been working through the proof of Theorem 3.4.1 in the article https://arxiv.org/pdf/1211.2851.pdf (pages 35-6), but there is one technical detail still unclear to me.
Specifically, we have ...
- 317
1
vote
1
answer
171
views
Showing that a certain simplicial set has levelwise small cardinality
My question concerns Section 2 of the article "The Simplicial Model of Univalent Foundations (after Voevodsky)" (https://arxiv.org/pdf/1211.2851.pdf).
Let $\alpha$ be a strongly inaccessible cardinal....
- 317
0
votes
0
answers
213
views
Is there a foundational approach that takes "structure" as primitive?
As per the title, I'd be curious to know if there have been attempts at constructing a foundation of mathematics taking, somehow, purely the notion of "structure" as primitive, maybe via a system of ...
- 22.7k
4
votes
1
answer
289
views
Checking the functoriality of an expression involving dependent sum and product
I'm unsure if my question is advanced enough for this site, but let's see.
Let $\mathcal{C}$ be a locally cartesian closed category, so that it always has dependent products $\Pi_f$, i.e., right ...
- 317
4
votes
1
answer
500
views
Uniqueness principle for functions types in the HoTT book
Chapter 1.2 of the HoTT book says this about eta-conversion:
$$
f \equiv (\lambda x . f(x)).
$$
This equality is the uniqueness principle for function types, because it shows that $f$ is uniquely ...
- 143
2
votes
0
answers
210
views
Categorical semantics of the identity type
In Appendix B of the article Simplicial Model of Univ. Foundations, Definition B.1.3 specifies the structure for identity types in a contextual category $\mathcal{C}$ (which in particular is equipped ...
- 317
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. ...
- 14.5k
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 ...
- 4,353
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 ...
- 5,933
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 ...
- 755
25
votes
0
answers
5k
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 ...
- 411
5
votes
1
answer
740
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,...
- 51
5
votes
1
answer
390
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, ...
- 61.5k
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 ...
- 1,185
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$-...
- 42.5k
6
votes
3
answers
550
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 ...
- 889
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 ...
- 5,933
11
votes
3
answers
908
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 ...
- 17.5k
5
votes
1
answer
172
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)-...
- 79
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 ...
- 17.5k
1
vote
0
answers
179
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 ...
- 79
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 ...
11
votes
1
answer
731
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)
$$
...
- 213
7
votes
2
answers
455
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,...
- 179
2
votes
0
answers
2k
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)...
- 6,001
1
vote
1
answer
278
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 ...
- 1,700
4
votes
3
answers
599
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 ...
- 233
2
votes
1
answer
308
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 ...
- 233
3
votes
1
answer
152
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 $...
user94803
4
votes
1
answer
195
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 ...
- 801
2
votes
1
answer
363
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) ...
- 33
1
vote
1
answer
234
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:
...
- 173
3
votes
1
answer
297
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 ...
- 585
3
votes
2
answers
736
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 ...
- 2,129
5
votes
1
answer
896
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 ...
- 369
4
votes
1
answer
665
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 ...
- 369
5
votes
1
answer
729
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 ...
- 53
2
votes
1
answer
264
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 ...
- 4,410
14
votes
1
answer
615
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$...
- 765
0
votes
1
answer
161
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 ...
- 179