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.
137
questions
2
votes
0
answers
204
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 ...
user507115
5
votes
1
answer
415
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 ...
- 183
1
vote
0
answers
125
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 ...
- 1,351
3
votes
0
answers
186
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 ...
- 1,351
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 ...
- 231
6
votes
1
answer
294
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,298
6
votes
1
answer
323
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 ...
- 6,684
2
votes
0
answers
71
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}$, ...
- 21
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 ...
- 2,574
6
votes
1
answer
295
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. ...
- 6,684
5
votes
2
answers
780
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 ...
- 119
7
votes
0
answers
174
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,876
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 ...
- 2,574
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, ...
- 119
20
votes
2
answers
762
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 ...
- 302