Textbooks are usually supposed to be accessible to a wide audience so it makes sense when discussing foundations to start from a (hopefully) familiar set theory

Textbooks are usually supposed to be accessible to a wide audience so it makes sense when discussing foundations to start from a (hopefully) familiar set theory. It's usually a trade-off, since you end up repeating yourself when it comes to "internalized" constructions. "Sketches of an Elephant" is a good example of a textbook that pretty much presents everything twice. Once in an ambient set theory and once internally. What I meant specifically is work such as the following: Internal Universes in Models of Homotopy Type Theory - https://arxiv.org/abs/1801.07664 which explicitly works in an extensional type theory with some axioms to simplify and generalize a complicated model construction. > For example is there a full, unrestricted formalisation of category theory in HoTT? You can formalize category theory in HoTT as presented in the book. This has some advantages over a presentation in extensional type theory or set theory (being able to work up-to equivalence) and some disadvantages (universes in categories have to be constructed explicitly, since the ambient universe is not truncated). In my opinion, it's not the case that one is strictly superior - in the end it always depends on what you want to do.