On Sun, May 10, 2020 at 4:35 PM Ulrik Buchholtz <ulrikbu...@gmail.com> wrote:
No need to apologize: I know I was being slightly provocative by juxtaposing a question about sets cover (SC) and a comment on 2-level type theory in this context, in order to provoke some discussion :-)

It worked :-)
 
Wouldn't you agree, however, that even though basic 2LTT is conservative over HoTT, from a certain point of view, 2LTT privileges the “ground floor” exosets? In your very nice paper, https://arxiv.org/abs/1705.03307, you decorate the inner (fibrant, endo-) types as special, and leave the exotypes undecorated, privileging the latter. While from a user's perspective, however, it's the (inner) types that are standard/mathematical, and the exotypes that are special.

I think I see where you are coming from. But for me, decorating the inner types as special was simply a pragmatic choice, not a philosophical one. Since most/all statements in the paper are "proper" 2LTT, there are more exo- / outer types involved than endo- / inner ones. But as a user, one is interested in the fibrant types (and maybe even assumes that they coincide with the inner theory), and only adds some small exo-sprinkles like "exo-Nat is cofibrant"; then, it makes sense to decorate the exo-types instead, as e.g. in https://arxiv.org/abs/2004.06572
And maybe it would be less confusing if we did the same in the paper that you linked to. I'm not sure.
 
And regardless of the decorations, the mere fact that we bring in the exoset level makes the theory harder to justify from the philosophical position that general homotopy types are not reducible to sets. One can in fact see the conservativity result as foundational reduction (in the sense of https://math.stanford.edu/~feferman/papers/reductive.pdf section 5) from a system justified by the principle that everything is based on sets to a system justified by a framework where that isn't the case.

That's interesting, thanks for the link!
 
Another connection is that it seems it should be easier to find an axiom, which might imply SC, that would allow us to construct the type of semi-simplicial types, rather than such an axiom that doesn't imply SC. But I don't know any such axiom statable in book HoTT either way.

Good question.
 
BTW, you probably meant “simplicial set” above. And yes, that kind of axiom would be the strongest expression of “everything is based sets”, and it currently needs 2LTT to even be stated.

You're right, I meant "set". (Otherwise it'd be silly, a type X is the realization of the [fibrant replacement of] the constant presheaf X.)
 
Nicolai


Cheers,
Ulrik

--
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyT...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/7b9eb7c9-040a-46e8-b470-28958f8d7713%40googlegroups.com.