On Sun, May 10, 2020 at 5:53 AM Ulrik Buchholtz
<ulrikbu...@gmail.com> wrote:
> The 2-level type theories can be viewed as another way of making a type theory that is faithful to the idea that everything is based on sets.

While I kind of see how one could say this, I think it's misleading
especially in light of the above dichotomy, becuase 2LTT doesn't imply
any of the *internal* "types are based on sets" axioms for the fibrant
layer.  As you know, 2LTT without additional axioms is conservative
over HoTT, while even with stronger axioms it can still be modeled in
many or all higher toposes.