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$ (and therefore $\Phi 0 = \Delta_{1}$ and $\Phi 1 = \mathrm{Type}$). Does this require fancy universe magic to avoid size issues? I'd like to play with this thing in familiar homotopy theory, rather than discard favorable universe axioms. Has anyone written on this?
$\begingroup$
$\endgroup$
2
-
4$\begingroup$ In order for this to be possible you would need $\textrm{Type} : \textrm{Type}$. Do you intend to allow the (unwritten) subscripts to be different? $\endgroup$– Zhen LinCommented Oct 19, 2021 at 23:40
-
$\begingroup$ Yes, I figured if I couldn't avoid this then there may be some way to "cheese" it using Grothendieck universes. But then I don't think this gets fixed by its self-reference; you have freedom in how fast limit cardinals grow or something to that tune, right? $\endgroup$– MathemologistCommented Oct 20, 2021 at 9:19
Add a comment
|