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

127
questions

5
votes

2
answers

478
views

### Why isn't $S^1$ contractible in homotopy type theory?

$\newcommand\base{\mathit{base}}\newcommand\unique{\mathit{unique}}\DeclareMathOperator\transport{transport}\newcommand\loop{\mathit{loop}}\DeclareMathOperator\refl{refl}$In the context of homotopy ...

7
votes

0
answers

156
views

### How does nullification of $K(\mathbb{Z}, 2)$ compare to 1-truncation?

Let $B$ be a type (or space). A type (or space) is $B$-null if the canonical map $X \to X^B$ is an equivalence. The $B$-nullification of an arbitrary type $X$ is a $B$-null type $\bigcirc_B X$ ...

5
votes

1
answer

141
views

### Are lists in homotopy type theory free $A_\infty$-spaces?

Traditionally in dependent type theory with axiom K or uniqueness of identity proofs, every type $A$ is 0-truncated, and thus the type of lists on $A$, $\mathrm{List}(A)$, is 0-truncated and the free ...

1
vote

1
answer

124
views

### Computation over non-reflexivity

The principle of induction over identity families, do not prohibit instances different from refl: x == x but its computation rule is only defined for this instance, ...

19
votes

2
answers

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

7
votes

0
answers

197
views

### New Foundations in a Homotopy/Intuitionistic Type Theory form?

New Foundations is a famously odd set theory suggested by Quine in the 1930s which:
Features a universal set.
Disproves the axiom of choice.
Proves the existence of an infinite set by a trivial ...

1
vote

0
answers

71
views

### Directly proving the extensionality principle for product types without quasi-inverses

In section 2.6 of the Univalent Foundations Project's Homotopy Type Theory book, the extensionality principle of product types is proven by showing that for all elements $a:A$, $a':A$, $b:A$, $b':A$, ...

3
votes

1
answer

377
views

### Does the concept of a $\infty$-category have a natural definition in the $\infty$-world?

I start with a thesis: the natural notion of equality is additional data (paths/morphisms), not a binary relation (the fact that they exist). So, in particular, with such a constructivization (...

2
votes

1
answer

296
views

### Undecidable statements in type theory

In type theory, proving a statement means to exhibit an instance/element of a type corresponding to the statement. But if the statement is undecidable, no element of the type A nor its negation A → ⊥ ...

0
votes

0
answers

76
views

### Univalence and higher inductive types in the lambda calculus model of type theory

In appendix A1 of the homotopy type theory book by the Univalent Foundations Project, the authors give a formal presentation of Martin-Löf type theory in lambda calculus. However, they did not give ...

5
votes

3
answers

406
views

### Homotopy type theory: why are $0:\mathbb N$ and $\mathrm{succ}(0):\mathbb N$ not judgementally equal?

This question is related to Homotopy type theory : how to disprove that $0=\mathrm{succ}(0)$
in the type $\mathbb N$.
Section 2.13 in The HoTT Book uses "the encode-decode method to characterize ...

7
votes

1
answer

468
views

### Open problems in type theory

I am only a beginner in the field of type theory, and I'm wondering if the community could point me out a few open problems in the field. I have a good background in logic, in particular, proof theory ...

6
votes

1
answer

130
views

### Univalence for weakly Tarski universes

In Martin-Löf type theory, a weakly Tarski universe is a type $\mathcal{U}$ with a type family $\mathcal{T}(A)$ indexed by terms $A:\mathcal{U}$, which is closed under identity types, dependent ...

2
votes

1
answer

290
views

### Path types and identity types in dependent type theory

There's been some debate at the nLab recently over the names of "identity type" and "path type" in certain dependent type theories.
One user wrote that
Many cubical type theorists ...

7
votes

1
answer

466
views

### Long exact sequences for parametrized cohomology

I'm reading Michael Shulman's articles on cohomology in HoTT here and here, as well as Floris van Doorn's thesis here.
Given $E: Z \to \mathsf{Spectrum}$ a family of spectra over a homotopy type $Z$, ...

2
votes

1
answer

397
views

### Higher inductive types in higher observational type theory

Mike Shulman gave the following set of talks on higher observational type theory earlier this year (part 1, part 2, part 3). However, while he talked about how the identity types are defined and ...

3
votes

0
answers

63
views

### Discreteness of the higher inductive-inductive Cauchy real numbers in real cohesive homotopy type theory

We work in cohesive homotopy type theory with propositional resizing, so that there is only one type of Dedekind real numbers $\mathbb{R}$ up to equivalence, and Mike Shulman's axiom $\mathbb{R}\flat$,...

3
votes

0
answers

244
views

### Principle of unique choice in homotopy type theory

In the MathOverflow thread Mathematics without the principle of unique choice, Mike Shulman defines the principle of unique choice to be
if $R$ is a relation between two sets $A$, $B$, and for every $...

0
votes

1
answer

159
views

### Construct higher inductive types with only generalized algebraic data types and non-truncated quotients?

Higher inductive types are a useful concept in homotopy type theory. However, considering its general syntax is a bit of a challenge. Is it possible to implement all higher inductive types with just ...

4
votes

1
answer

166
views

### Predicativity and axiom $\mathbb{R}\flat$ in real cohesive homotopy type theory

In Mike Shulman's article Brouwer’s fixed-point theorem in real-cohesive homotopy type theory, the fundamental axiom adopted for his real-cohesive homotopy type theory (axiom $\mathbb{R}\flat$), which ...

1
vote

0
answers

197
views

### Understanding the double negation modality under the "propositions as types" paradigm

$\DeclareMathOperator\Hom{Hom}$I'm trying to understand the double negation modality under the "propositions as types" paradigm, but I'm running into an apparent contradiction: let $T$ be a ...

2
votes

1
answer

209
views

### Well-behaved monad quotients

Reading through Modular specification of monads through higher-order presentations, this paper includes the following lemma within set-truncated homotopy type theory:
Given a monad $R$ (they work on ...

2
votes

1
answer

228
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\...

4
votes

1
answer

300
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, ...

14
votes

2
answers

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

3
votes

0
answers

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

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

2
votes

0
answers

206
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$ (...

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

12
votes

1
answer

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

15
votes

3
answers

903
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 (...

5
votes

1
answer

632
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)$...

6
votes

2
answers

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

8
votes

1
answer

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

4
votes

1
answer

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

13
votes

1
answer

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

5
votes

2
answers

417
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}(...

1
vote

0
answers

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

3
votes

0
answers

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

5
votes

1
answer

377
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, ...

3
votes

1
answer

150
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)-...

7
votes

2
answers

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

7
votes

2
answers

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

12
votes

1
answer

590
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
vote

1
answer

247
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?
...

2
votes

1
answer

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

3
votes

1
answer

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

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
votes

1
answer

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

11
votes

3
answers

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