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 :-)
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.
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.
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.
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.
--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.