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 ...
- 111
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$ ...
- 3,601
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,826
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, ...
- 111
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 ...
- 193
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 ...
- 4,732
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$, ...
- 1,826
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 (...
- 5,627
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 → ⊥ ...
- 111
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 ...
- 1,826
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 ...
- 53
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 ...
- 1,826
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 ...
- 1,826
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$, ...
- 5,753
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 ...
- 1,826
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$,...
- 1,826
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 $...
- 1,826
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 ...
- 323
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,826
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 ...
- 399
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\...
- 23
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, ...
user173426
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 ...
- 14.7k
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. ...
- 4,648
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 ...
- 551
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$ (...
- 703
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 ...
- 111
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 ...
- 6,127
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 (...
- 261
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)$...
- 121
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 ...
user173426
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 ...
- 2,419
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 ...
- 570
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 ...
- 131
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}(...
- 51
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.
- 11
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 ...
- 1,070
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, ...
- 5,753
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)-...
- 308
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 ...
user173426
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 ...
- 173
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,070
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?
...
- 5,753
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$ ...
- 17.1k
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 ...
- 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 ...
- 4,648
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 ...
- 549
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. ...
- 3,739