On Sun, May 10, 2020 at 3:01 PM Michael Shulman wrote: > On Sun, May 10, 2020 at 5:53 AM Ulrik Buchholtz > 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. > 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.