I'm looking for a reference on internal categories and externalization of internally defined notions.


The nlab has a stub on [externalization](https://ncatlab.org/nlab/show/externalization) (more details are available under [small fibration](https://ncatlab.org/nlab/show/small+fibration)) and the page on [internal categories](https://ncatlab.org/nlab/show/internal+category) gives enough of an introduction that I can sketch most internal notions, but I could really use a concise introduction to internal categories and externalization, and if possible the relationship between internalization and externalization. Are they adjoint in some sense?


I'm fine assuming a background of $2$-category theory, so talking about the $2$-category of internal categories in a category with pullbacks etc. would make sense, but ideally the reference would assume no familiarity with internal category theory or externalization. Any assistance is appreciated.



Reference on internal categories and externalization
For what it's worth, I should add my comment as an answer. Chapter 1 of Bart Jacobs' book *Categorical logic and type theory* (Studies in Logic and the Foundations of Mathematics **141** (1999), ([author's page](http://www.cs.ru.nl/B.Jacobs/CLT/bookinfo.html), [publisher page](https://www.elsevier.com/books/categorical-logic-and-type-theory/jacobs/978-0-444-50170-7), [pdf](https://people.mpi-sws.org/%7Edreyer/courses/catlogic/jacobs.pdf))) is a good intro to fibred category theory, and chapter 7 has an intro to internal category theory, and it links the two. Chapter 9 does some more advanced fibred category theory.


