On Sun, May 10, 2020 at 4:35 PM Ulrik Buchholtz 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 > > . >