Skip to main content
1 of 2
Andrej Bauer
  • 48.8k
  • 11
  • 131
  • 239

Let us first consider a slightly simpler situation. The cartesian product of sets $A$ and $B$ is a set $C$ with two maps $p_1 : C \to A$ and $p_2 : C \to B$ such that ... (familiar condition inserted here). All cartesian products of $A$ and $B$ are canonically isomorphic, and among them there is a particular one, denoted $A \times B$, which is specifically defined as $A \times B = \lbrace\lbrace\lbrace x,y \rbrace, \lbrace y\rbrace\rbrace \mid x \in A \land y \in B\rbrace$.

This is a familiar situation. Often a construction is determined up to canonical isomorphism, but we have a specific one that we can use as an operation, like $(A,B) \mapsto A \times B$ above.

Awodey does the same thing in his book. "Being a pullback" is a property, but we can turn it into structure, i.e., an operation which takes a pair of arrows $f : A \to C$ and $g : B \to C$ and gives a pullback square. You may wonder whether there always is such an operation. If you believe in the axiom of choice then the answer is positive, because we may always choose particular pullbacks among the canonically isomorphic ones. In concrete examples you will usually find chosen pullbacks easily, so this is not problematic.

But there is a catch. Awodey says that pullbacks form a functor. For this to be the case a certain coherence condition has to hold, and it is not obvious that we can always choose the pullback operation so that the condition holds. It is a good exercise to work this out by yourself.

Andrej Bauer
  • 48.8k
  • 11
  • 131
  • 239