7
$\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.

Improve this question
$\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
    Commented Sep 19, 2020 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
    Commented Sep 19, 2020 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
    Commented Sep 19, 2020 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
    Commented Sep 19, 2020 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
    Commented Sep 19, 2020 at 4:22

1 Answer 1

Reset to default
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.

Improve this answer
$\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
    Commented Sep 20, 2020 at 22:05

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .