Timeline for Defining (infinity,1)-categories in HoTT using only an interval type
Current License: CC BY-SA 4.0
8 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Aug 13, 2020 at 20:18 | vote | accept | Bastiaan Cnossen | ||
| Aug 13, 2020 at 15:39 | answer | added | Mike Shulman | timeline score: 7 | |
| Aug 12, 2020 at 14:01 | comment | added | Simon Henry | And there are an infinite number of maps you might want to consider extention type along. The role of the first two layer of their type theory is to determine which maps you are allowed to consider extention type along (basically, all inclusion between finite simplicial sets).... Of course I'm not saying that these extention type are neccessary, maybe what you are proposing can also works and extention type are just things that are there to make our lives easier. | |
| Aug 12, 2020 at 13:59 | comment | added | Simon Henry | So what you are describing is basically the definition of an extention type. Now, the thing is we don't want to be able to consider just the extention type corresponding to $hom_A(x,y)$, i.e. to the boundary inclusion $\Delta[0] \coprod \Delta[0] \to \Delta[1]$, but also these corresponding to more general simplicial maps. For e.g. the extention type along $\Lambda^1[2] \to \Delta[2]$ give you the type of arrows which are a composite of $f,g$ (a type which is contractible in a Segal type, but maybe not in general). | |
| Aug 12, 2020 at 13:37 | comment | added | Bastiaan Cnossen | Yeah I think to my unexperienced eye it seems like a lot of complexity for turning some propositional equalities into judgmental equalities. What would happen if one introduces $\text{hom}_A(x,y)$ as a formal type family, satisfying the rule that every $f: \mathbb{I} \to A$ gives a term $f': \text{hom}_A(f(0),f(1))$ and conversely every $f': \text{hom}_A(x,y)$ gives a map $f: \mathbb{I} \to A$ with judgmental equalities $f(0) \equiv a$ and $f(1)\equiv b$? Where does one run into problems? | |
| Aug 12, 2020 at 13:16 | comment | added | Simon Henry | I think you are over estimating the complexcity of this (shape,tope) layer and so one. At the end of the day "all they do" is to add an object $I$ endowed with an order relation making $I$ an internal (i.e. it has top and bottom elements $0$ and $1$ and $x \leqslant y $ or $y \leqslant x$ for all $x,y$) exactly in the same way that you propose to add an object $I$. The reason why they single-out this type $I$ in a different layer of type theory is in order do define the notion of "extention type", which allows to actually define $hom_A(x,y)$ without using identity type. | |
| Aug 12, 2020 at 13:15 | history | edited | Bastiaan Cnossen | CC BY-SA 4.0 |
added 15 characters in body
|
| Aug 12, 2020 at 12:47 | history | asked | Bastiaan Cnossen | CC BY-SA 4.0 |