Timeline for Are monomorphisms in an $\infty$-topos preserved by $0$-truncation?
Current License: CC BY-SA 4.0
12 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jul 10 at 19:49 | comment | added | aws | It might be more useful to directly give a direct proof by informally following the HoTT proof rather than formally writing out the details of the interpretation. | |
| Jul 10 at 19:49 | comment | added | aws | There are generally speaking a lot of details that are not spelt out in the paper. These things would be covered better in a textbook, but as yet there is no such textbook as far as I know. I think showing the two definitions of (-1)-truncation are equivalent should be fairly straightforward as these things go - you can show internally in type theory that a map is (-1)-truncated when the diagonal $X \to X \times X$ is an equivalence which I think is known to be equivalent to the $\infty$-topos version. | |
| Jul 10 at 19:43 | answer | added | Naïm Favier | timeline score: 2 | |
| Jul 10 at 19:36 | comment | added | Jonathan Beardsley | Great! Does he show that, e.g., being (-1)-truncated in the HoTT sense agrees with being (-1)-truncated in the HTT sense? | |
| Jul 10 at 19:34 | comment | added | aws | It's a result of Mike Shulman arxiv.org/abs/1904.07004. | |
| Jul 10 at 19:32 | comment | added | Jonathan Beardsley | Sure, sure, I know that it's supposed to be that, I just don't see it in, e.g. the HoTT book. | |
| Jul 10 at 19:30 | comment | added | Naïm Favier | HoTT is supposed to be an internal language for $(\infty, 1)$-topoi. | |
| Jul 10 at 19:29 | comment | added | Jonathan Beardsley | I see, that sounds correct then. But this would need to happen in an arbitrary $\infty$-topos though. Does homotopy type theory work in the same way there? | |
| Jul 10 at 19:22 | comment | added | Naïm Favier | An embedding is a function with propositional fibres, which sounds a lot like your definition. They're also called $(-1)$-truncated maps in the HoTT book. An embedding between h-sets is just an injective function (in the sense that $f(x) = f(y) \to x = y$). | |
| Jul 10 at 19:19 | comment | added | Jonathan Beardsley | @NaïmFavier I don't know. What's an embedding in homotopy type theory? | |
| Jul 10 at 19:06 | comment | added | Naïm Favier | Would it suffice to prove, in homotopy type theory, that the 0-truncation of an embedding is an embedding? Because that should definitely be provable. | |
| Jul 10 at 18:54 | history | asked | Jonathan Beardsley | CC BY-SA 4.0 |