All Questions
Tagged with infinity-topos-theory homotopy-type-theory
12
questions
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
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
3
votes
1
answer
422
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 (...
- 6,684
1
vote
0
answers
246
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 ...
15
votes
2
answers
656
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 ...
- 15k
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$ (...
- 713
11
votes
1
answer
814
views
What is an Elementary "Homotopy, Model" Topos?
Context:
Def (Rezk): A (Grothendieck) homotopy topos is a homotopy left exact Bousfield localization of the model category of simplicial presheaves sPsh(C) on a small simplicial category C.
Thm (...
- 1,700
4
votes
1
answer
431
views
Is the infinity-groupoid of a finite CW complex finitely-presented?
An infinity-groupoid is finitely-presented when it is equivalent to the free infinity-groupoid on a finite family of generators, possibly of different dimensions.
Is the infinity-groupoid of a finite ...
- 2,453
18
votes
1
answer
1k
views
What would be an infinity-groupoid analogue of the duality between sets and complete atomic boolean algebras?
Consider the object classifier of the $\infty$-topos of $\infty$-groupoids. For the role it plays in homotopy type theory as the type of types, let’s denote it as $Type = \coprod_{[F]} B Aut(F)$, the ...
- 5,009
9
votes
1
answer
448
views
Base change in homotopy type theory
Recall that with the internal language of 1-toposes, we have the nice, basic, and useful result that geometric sequents are stable under base change along geometric morphisms: If $\varphi$ and $\psi$ ...
- 3,262
21
votes
2
answers
1k
views
$\infty$-categorical interpretation of type theory
One can read at several places that Martin-löf type theory should be the internal language of a locally Cartesian closed infinity category, and that the univalence axiom should distinguished infinity ...
- 40.8k
16
votes
1
answer
3k
views
Forcing in Homotopy Type Theory
I apologize if this question doesn't make any sense. I'll just go ahead and delete it if that's the case. But the question is just the title. Is there a notion of forcing in homotopy type theory? ...
- 10.3k