On Sunday, May 10, 2020 at 4:27:30 PM UTC+2, Nicolai Kraus wrote:
>
> I agree with Mike - sorry Ulrik :-)
> For me, "everything is based on sets" would mean that every fibrant type 
> can be written as the realization of a (semi-) simplicial type, or 
> something like this. 
>

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