6
$\begingroup$

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

The nlab has a stub on externalization (more details are available under small fibration) and the page on internal categories 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.

$\endgroup$
9
  • 2
    $\begingroup$ I don't think such a reference exists. As observed in the abstract of these notes, much of the foundational work of Bénabou on fibred categories is unpublished. But perhaps you might start by reading those notes, and maybe chapter B2 of Sketches of an elephant. $\endgroup$ – Zhen Lin Sep 19 '20 at 0:38
  • $\begingroup$ @ZhenLin Thank you, I’ll take a look at those notes. My uni library is currently closed (and doesn’t have a copy to boot), and I don’t have half a g to drop on Sketches right now — are you aware of anywhere I can access that portion online? $\endgroup$ – Alec Rhea Sep 19 '20 at 0:43
  • 1
    $\begingroup$ I don't think Johnstone has made any part of the Elephant online. Personally I'm holding out for volume 3 (and a corrected edition of the first two volumes) before buying a personal copy... $\endgroup$ – Zhen Lin Sep 19 '20 at 0:48
  • 1
    $\begingroup$ @DavidRoberts Will do, thank you; for any interested parties, the book David mentions can be found here: people.mpi-sws.org/~dreyer/courses/catlogic/jacobs.pdf. $\endgroup$ – Alec Rhea Sep 19 '20 at 1:17
  • 2
    $\begingroup$ @AlecRhea: Johnstone's Sketches of an Elephant is available here: libgen.rs/book/index.php?md5=22AECD1E74BE933CBA966B1396122B77 $\endgroup$ – Dmitri Pavlov Sep 19 '20 at 4:22
7
$\begingroup$

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, publisher page, 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.

$\endgroup$
1
  • 1
    $\begingroup$ This ended up being exactly what I was looking for; I’ll have to learn about the internal logic of fibrations to fully understand what he’s saying, but that topic is also covered earlier on. Thank you! $\endgroup$ – Alec Rhea Sep 20 '20 at 22:05

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.