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.
134
questions
3
votes
0
answers
134
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 ...
11
votes
2
answers
1k
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 ...
5
votes
1
answer
252
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
303
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
67
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
51
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
274
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
720
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
166
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
157
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
129
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
737
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
233
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
73
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
411
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
322
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
83
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
439
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
624
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
142
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
387
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
533
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
477
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
66
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
264
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
201
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
179
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
229
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
223
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
250
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
327
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
632
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
355
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
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
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
862
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
911
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
733
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
904
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
766
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
415
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
624
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
480
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
220
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
266
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
400
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
159
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
406
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
336
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 ...