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.

Filter by
Sorted by
Tagged with
2 votes
0 answers
87 views

Homotopy type theory : how to disprove that $0=\operatorname{succ}(0)$ in the type $\mathbb{N}$

$\newcommand{\suc}{\operatorname{succ}}\newcommand{\IsPrime}{\operatorname{IsPrime}}$I'm self learning Homotopy type theory reading the HoTT book. I understand that if $A+B$ and $\neg A :\equiv A\...
user avatar
3 votes
0 answers
107 views

Consistency of Generalised Continuum Hypothesis and univalence in HoTT

In homotopy type theory, propositional excluded middle and the axiom of choice sets are both consistent with univalence, both of which yields type theoretic models for classical mathematics. However, ...
user avatar
11 votes
2 answers
409 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 ...
user avatar
  • 13.2k
3 votes
0 answers
185 views

Conversion of proofs between HoTT and ZFC

HoTT provides a foundation of math that remains mysterious for many mathematicians including me. Hence this question. There are several implementations of math based on ZFC, an example being MetaMath. ...
user avatar
  • 4,005
24 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 ...
user avatar
2 votes
0 answers
198 views

A map that names itself

Call the walking arrow $\Delta_{1}$, containing exactly one nontrivial 1-cell $[0<1] : 0 \to 1$. I am interested in a map $\Phi : \Delta_{1} \to \mathrm{Type}$, such that $\Phi [0<1] = \Phi$ (...
user avatar
10 votes
1 answer
879 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 ...
user avatar
11 votes
1 answer
588 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 ...
user avatar
  • 5,759
15 votes
3 answers
875 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 (...
user avatar
5 votes
1 answer
466 views

Construction of the universal covering space of the etale homotopy type $Et(X)$

Let $X$ be a nice scheme (additional assumptions could be added), and let $Et(X)$ be its (Artin-Mazur) etale homotopy type. I am looking for a/the scheme $Y$ over $X$ whose etale homotopy type $Et(Y)$...
user avatar
6 votes
2 answers
851 views

Defining rational numbers without using quotients or 0-truncations

Most definitions of the rational numbers as a higher inductive type in univalent homotopy type theory (such as those in the cubical Agda library for example) require either the use of a quotient set ...
user avatar
7 votes
1 answer
558 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 ...
user avatar
  • 1,515
3 votes
1 answer
222 views

In cubical type theory, can we insist that "constant" compositions are the identity?

$\DeclareMathOperator{\comp}{comp}\DeclareMathOperator{\refl}{refl}\DeclareMathOperator{\transp}{transp}$I've been reading about Cubical Type Theory and playing around with the Agda implementation of ...
user avatar
12 votes
1 answer
416 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 ...
user avatar
  • 121
5 votes
2 answers
281 views

Assuming decidable equality but not LEM in HoTT

The law of excluded middle in homotopy type theory is a term of $$\prod_{A:\mathcal{U}}\Big(\mathrm{isProp}(A)\to(A+\neg A)\Big).$$What if we assume a term of$$\prod_{A:\mathcal{U}}\Big(\mathrm{isSet}(...
user avatar
  • 51
1 vote
0 answers
129 views

The difference between Agda and Idris for programming using Homotopy type theory [closed]

Which is better for programming benifiting by Homotopy type theory(HoTT),Idris or Agda.compare them.
user avatar
  • 11
3 votes
0 answers
244 views

Intuitive (topological) explanation of a proof from the HoTT book [closed]

My friends and I are struggling with understanding intuitively the proof of equivalence between based and free path inductions (HoTT book 1.12.2) The first major problem is understanding the meaning ...
user avatar
5 votes
1 answer
333 views

Using HoTT, why is twisted cohomology of BG group cohomology?

I've been reading Michael Shulman's blog posts defining cohomology in homotopy type theory, and I'd like to understand (using HoTT) why cohomology of BG is group cohomology. if I understand correctly, ...
user avatar
  • 5,301
3 votes
1 answer
137 views

Higher-dimensional paths as parametrizations of 1-dimensional paths

Sect. 6.7 of the HoTT Book establishes in the context of CW complexes that "we can obtain an n-dimensional path as a continuous family of 1-dimensional paths parametrized by an (n − 1)-...
user avatar
7 votes
2 answers
334 views

Construction of Dedekind reals using higher inductive-inductive types

In the textbook Homotopy Type Theory: Univalent Foundations of Mathematics, the authors give a predicative constructive construction of the initial Cauchy complete reals $\mathbb{R}_C$ in terms of a ...
user avatar
7 votes
2 answers
264 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 ...
user avatar
11 votes
1 answer
508 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,...
user avatar
1 vote
1 answer
214 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? ...
user avatar
  • 5,301
2 votes
1 answer
366 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$ ...
user avatar
3 votes
1 answer
241 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 ...
user avatar
15 votes
2 answers
1k 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 ...
user avatar
  • 4,005
4 votes
1 answer
322 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 ...
user avatar
9 votes
2 answers
521 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. ...
user avatar
  • 3,203
14 votes
2 answers
683 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 ...
user avatar
  • 157
6 votes
0 answers
114 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$...
user avatar
5 votes
1 answer
120 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 ...
user avatar
1 vote
1 answer
161 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....
user avatar
0 votes
0 answers
202 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 ...
user avatar
  • 21.6k
4 votes
1 answer
263 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 ...
user avatar
4 votes
1 answer
409 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 ...
user avatar
  • 143
2 votes
0 answers
172 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 ...
user avatar
15 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. ...
user avatar
29 votes
1 answer
1k 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 ...
user avatar
  • 3,067
8 votes
2 answers
929 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 ...
user avatar
  • 5,301
63 votes
4 answers
4k 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 ...
user avatar
21 votes
0 answers
3k 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 ...
user avatar
  • 371
3 votes
1 answer
460 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,...
user avatar
4 votes
1 answer
356 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, ...
user avatar
  • 49.2k
15 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 ...
user avatar
  • 1,055
34 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$-...
user avatar
6 votes
3 answers
451 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 ...
user avatar
14 votes
1 answer
744 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 ...
user avatar
  • 5,301
11 votes
3 answers
825 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 ...
user avatar
5 votes
1 answer
146 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)-...
user avatar
  • 79
19 votes
2 answers
1k 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 ...
user avatar