6
$\begingroup$

In a sense this is a followup to my earlier question Does the (1-)topos structure on simplicial sets have any homotopy-theoretic significance?.

In the topos of simplicial sets, the subobject classifier $\Omega$ is injective, hence it is a contractible Kan complex.

So we can view $\Omega$ as an $\infty$-connected $\infty$-groupoid, in particular its two objects $\mathbf{true},\mathbf{false}:1\to\Omega$ are isomorphic.

Does this fact have any significance for the internal logic of simplicial sets? For a logician it must look somehow disconcerting...

Improve this question
$\endgroup$
20
  • 2
    $\begingroup$ I find this question unclear, as it asks us to answer something that is placed in derision quotes (in the title), while the first paragraph asks for homotopy-theoretic significance (very close to asking for an opinion). What would an answer possibly constitute? $\endgroup$
    – Andrej Bauer
    Commented Oct 12 at 11:02
  • 4
    $\begingroup$ This is the same point as Zhen Lin, but just to emphasis it, this is not in any way problematic and it is very misleading to say simplicial sets is "contradictory up to homotopy" because the subobject classifier for the 1-topos has very little to do with the subobject classifier of the $\infty$-topos. When we're working with a model category, I would refer to the latter as "homotopy subobject classifier," but I'm not sure how standard that is. Simplicial sets is boolean as an $\infty$-topos, so the homotopy subobject classifier is 2, which is not connected. $\endgroup$
    – aws
    Commented Oct 12 at 11:19
  • 1
    $\begingroup$ Yes. But it is contractible, as you noted, hence not very interesting… $\endgroup$
    – Zhen Lin
    Commented Oct 12 at 12:43
  • 1
    $\begingroup$ These properties are not really visible in the ∞-topos. They rely on strict equality, which is not homotopy-invariant. $\endgroup$
    – Zhen Lin
    Commented Oct 12 at 13:07
  • 1
    $\begingroup$ @მამუკაჯიბლაძე: You’re right — my previous comment was mistaken. The resolution instead is that retract-inclusions are not generally ∞-monos; for instance, the basepoint inclusion $1 \to S^1$ is not an ∞-mono (its homotopy fibre is $\mathbb{Z}$). And it’s just ∞-monos (i.e. –1-connected maps) which will be classified by $1 \to 2$ (i.e. represented homotopically-uniquely as ∞-pullbacks thereof). $\endgroup$
    – Peter LeFanu Lumsdaine
    Commented Oct 12 at 16:31

2 Answers 2

Reset to default
13
$\begingroup$

No, it’s not “inconsistent up to homotopy” — by combining the (strict) subobject classifier with the idea that contractible=trivial, you’re mixing two different logical languages for simplicial sets, in a way that doesn’t really make sense.

The subobject classifier is the “object of truth-values” of $\newcommand{\S}{\mathrm{sSet}}\S$ as a (strict 1-)topos — logically this can be seen as part of the interpretation of higher-order logic (IHOL) (see e.g. the Lambek–Scott book), or any of various forms of dependent type theory with a universe of propositions; but crucially, in all of these, arbitrary morphisms can be used to interpret “dependent types”, and equality is interpreted using a strict equaliser. In this logic, $\Omega$ is an object of truth-values, but is not trivial.

On the other hand, the idea that “contractible $\Rightarrow$ all elements equal” comes from the homotopy-theoretic interpretations of type theory (see e.g. Kapulkin–Lumsdaine 2012/2021, JEMS/arXiv), or from viewing $\S$ as an $\infty$-topos. There, only fibrations are taken to interpret dependent types, or (roughly equivalently) reindexing is modelled by homotopy pullbacks — and this is what makes it possible to interpret equality to as homotopy. But the canonical map $\top : 1 \to \Omega$ which 1-categorically classifies subobjects is not a fibration (indeed, it’s an equivalence); so in this logic, the classifying property of $\Omega$ isn’t visible. In this logic, $\Omega$ is indeed trivial, but it’s not an object of truth-values — in fact the object of truth-values is simply $2$, since up to homotopy, LEM holds (Kapulkin–Lumsdaine 2020, TAC/arXiv); stated $\infty$-categorically, $\top : 1 \to 2$ classifies $\infty$-monomorphisms (that is, $(-1)$-connected maps).

There are various reasonable ways to give a type theory combining these two interpretations (“2-level type theory” and “strict equality”, “strict propositions” are good keywords for this). Under such a language, both the above views of $\Omega$ will be visible together — but it can’t allow combining them to derive any kind of contradiction, since we know $\S$ is consistent in each of these languages. In particular, the universal family of propositions over $\Omega$ will be a “strict type/predicate”, and universal among strict proposition-valued predicates; and its elements will indeed be equal up to “weak equality”/“homotopy”; but strict predicates will not generally respect weak equality, so no inconsistency or triviality results.

Improve this answer
$\endgroup$
2
$\begingroup$

After much hesitation I came to the conclusion that I have to accept the answer by Peter LeFanu Lumsdaine. Still, I decided to add something that helps me more to understand it.

It seems that the key is in the very notion of monomorphism. "Without homotopies" it is just that $m:A\to B$ is a monomorphism if $mx=my$ implies $x=y$ for any $x,y:X\to A$. Whereas "with homotopies" it has to be refined to this: any proof of the fact that $mx$ and $my$ are equal must be liftable to a proof that $x$ is equal to $y$. So we get something like $m:A\to m(A)$ being also onto to some extent. That is, some things in $m(A)$ must be liftable to certain things in $A$. This at least shows that one needs some more restrictive conditions on $m$ than just being a monomorphism.

Improve this answer
$\endgroup$
2
  • 2
    $\begingroup$ Yes. I’d phrase your refinement as “any equality $mx=my$ can be lifted to an equality $x=y$,” and also this lifting must be continuous/functorial in $x$, $y$, and $m$. It’s a good intuition, but often technically awkward (it’s simple in the internal language, but unwieldy when working diagrammatically); fortunately there are many equivalent conditions for $m : X \to A$ to be ∞-mono, which are nice in different contexts: (1) the (∞-)diagonal $\Delta : X \to X \times^\infty_A X$ is an equivalence; (1') (when $m$ is a fibration) the 1-categorical diagonal is an equivalence; [cont’d] $\endgroup$
    – Peter LeFanu Lumsdaine
    Commented Oct 14 at 8:22
  • 1
    $\begingroup$ (2) the square $(\mathrm{id},m) : (\mathrm{id} : X \to X) \to (m : X \to A)$ is a homotopy pullback; (3) every homotopy-fiber of $m$ is either empty or contractible; (3') (when $m$ is a fibration) every fiber of $m$ is either empty or contractible; (4) over each connected component of $A$, $m$ is either empty or an equivalence. // The main thing throughout is to be careful how you mix strict and ∞-categorical notions. A priori, they can be totally independent; some good interactions hold, especially with fibrations, but don’t expect an interaction to work until it’s proven. $\endgroup$
    – Peter LeFanu Lumsdaine
    Commented Oct 14 at 8:22

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .