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

139
questions

7
votes

1
answer

606
views

### Do higher types in HoTT provide mathematical structures beyond ZFC?

I've been reading Andrej Bauer's blog post on "Univalent foundations subsume classical mathematics," which explains how Univalent Foundations and Homotopy Type Theory (HoTT) extend classical ...

6
votes

0
answers

128
views

### Constructive mathematics with different computational models

I am interested in understanding how the capabilities of constructive mathematics evolve when different computational models are considered. Specifically, if constructive mathematics traditionally ...

2
votes

0
answers

209
views

### Is there a computable model of HoTT?

Among the various models of homotopy type theory (simplicial sets, cubical sets, etc.), is there a computable one?
Can the negative follow from the Gödel-Rosser incompleteness theorem?
If there is no ...

5
votes

1
answer

425
views

### Large cardinals approached through $\infty$-categories

I am an undergraduate student (rising junior) majoring in philosophy and mathematics. For some time, I have been interested in homotopy type theory and so-called "univalent foundations". On ...

1
vote

0
answers

126
views

### Monads for proof relevance in type theory

I am just getting started with homotopy type theory. After watching an introductory lecture, I was attracted to the concept of proof relevance. In my understanding, the core idea here is to elevate ...

3
votes

0
answers

190
views

### Homotopy type theory for semantics

It looks like I have been building up a theory that might require looking closely at Homotopy Type Theory vs. Category Theory with respect to semantics. I am considering two types of semantics that ...

12
votes

2
answers

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

6
votes

1
answer

297
views

### Is univalence equivalent to every type function being a functor over equivalence?

Introduce a rule in type theory that if $\Gamma \vdash f : \text{Type} \to \text{Type}$ and $\Gamma \vdash e : A \simeq B$ then $\Gamma \vdash f[e] : f(A) \simeq f(B)$.
It may seem like such a rule is ...

6
votes

1
answer

325
views

### $\infty$-topos as an internal $\infty$-category in itself

I'm interested (both autonomously and directly related to my work) in the natural internalization of $\infty$-topos sheaves in it (as usual, assuming Grothendieck universes). Is there any literature ...

2
votes

0
answers

72
views

### Relation of top and bottom types given multiple universes

This is something that I haven't seen mentioned in any literature.
In a type theory (extensional, intuitionistic, Martin Lof variant), given two ordered Tarski Universes such that $U_i < U_{i+1}$, ...

1
vote

1
answer

69
views

### Constructing set-truncations of types from universes

This is a follow-up question from my previous question titled Constructing coproduct types and boolean types from universes, where I showed how every basic operation in set theory/topos theory could ...

6
votes

1
answer

297
views

### In HoTT with LEM, are sets and pointed sets the same thing?

The operations of adding and removing a point (where removing is a consideration of a subset of elements x such that $(x = *) \to 0$) implements the equivalence of these 1-types, as far as I can see. ...

5
votes

2
answers

795
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

180
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

167
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

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

20
votes

2
answers

766
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

258
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

76
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

424
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

342
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

88
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

452
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

726
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

151
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

449
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

555
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

535
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

73
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

274
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

234
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

186
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

249
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

236
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

257
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

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

15
votes

2
answers

659
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

382
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

2k
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

207
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

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

13
votes

1
answer

944
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

924
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

779
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

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

9
votes

1
answer

817
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

475
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

690
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

515
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

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