In any category $\mathcal{C}$ with pullbacks, we can define an internal category $\mathscr{C}$ in $\mathcal{C}$ as an object ${\bf Ob}_\mathscr{C}$ of objects and an object ${\bf Hom}_\mathscr{C}$ of arrows, together with arrows $${\sf dom},{\sf cod}:{\bf Hom}_\mathscr{C}\rightrightarrows{\bf Ob}_\mathscr{C},$$ $$1^\mathscr{C}:{\bf Ob}_\mathscr{C}\to{\bf Hom}_\mathscr{C},$$ $$\circ^\mathscr{C}:{\bf Hom}_\mathscr{C}\times_{{\bf Ob}_\mathscr{C}}{\bf Hom}_\mathscr{C}\to{\bf Hom}_\mathscr{C}$$ satisfying the expected commutative diagrams. Where I'm slightly confused is the associativity axiom, since the 'object of composable triples' can be taken as either one of the two isomorphic options below

I have no problem showing that they're isomorphic and I understand that pullbacks are usually only defined up to isomorphism anyway, but when expressing the associativity axiom we technically need both to appear in the diagram:

I haven't seen mention of this on the nlab page linked above, or the introductions to internal categories in Jacob's fibered category theory book, or Borceux/Janelidze's Galois theories book, which makes me wonder if this is just overly pedantic, but when I went to construct an example of an internal category and prove it satisfied the axioms I ran into this issue in the proof.

Is there some well-known trick for sweeping things like this under the rug in computations, or do we need to keep track of isomorphisms between internal data for computations to shake out correctly?

11more comments