pullbacks and cartesian arrows

Question

$B$ is a category with pullbacks. For a fibration $P \colon E \to B$, the following are true

1. a commutative square of cartesian arrows in $E$ over a pullback in $B$ is always a pullback in $E$

2. A commuting square

   squre

in $E$ with $\varphi_i$ cartesian and $\alpha$ and $\beta$ vertical is always a pullback in $E$.

It seems to me that 2. follows from the cartesiannes of the top arrow, for any $\theta_1 \colon H \to B$ there is a unique $k_1 \colon C \to A$, also there is a unique $k_2 \colon H \to C$ for $\theta_2 \colon H \to D$ such that $\beta \circ k_1 = k_2$. And this a pullback in $E$.

and 1. would essentially use the one $k$. Is this correct?

• Naïm Camille Favier: 2 is essentially a generalisation of the pasting law for pullbacks from the codomain fibration to arbitrary fibrations, while 1 is a similar lemma about cubes all whose faces except one are pullbacks. Does this answer your question? I can't quite tell what you're asking.
• Nash: @NaïmCamilleFavier I was asking about the idea of the proof. I am not sure if I follow your statements.
• Naïm Camille Favier: Well, I can't make sense of your proof. You have not established the universal property of the pullback here. As for my statements, just draw your diagram in the codomain fibration: it looks like this. You are then saying that the top square is a pullback if the bottom and outer squares are...
• Naïm Camille Favier: ...which is the pasting law for pullbacks. The statement in 2 is then a straightforward generalisation of this with some pullback squares replaced with cartesian lifts.
• Emil Jeřábek: This question does not seem to have anything particular to do with computer science, it is pure category theory. So it would be more suitable for math.stackexchange.com .

Answer 1

If we consider a cone $Q$ over the cospan $B \rightarrow D \leftarrow C$ since $\varphi_1$ is cartesian there is a unique $Q \rightarrow A$. We also have a unique arrows $Q \to C$ and $Q \to A \to C$ obtained from the fact that $\varphi_2$ is cartesian. Thus these unique arrows must be equal. Meaning that $Q \to A$ is the unique cone morphism and is unique. Hence the square is a pullback. As it can be seen below

enter image description here

• Nash: This is Lemma 1.3.3 in Peter Johnstone's Sketches of an Elephant – A Topos Theory Compendium.