Definition Let E,B be categories. Let p:E⇒B be a functor. A morphism α:E[X,Y] is Cartesian over f:B[pX,pY] iff ∀g:E[Z,Y]∀h:B[pZ,pX]pg=f∘h⟹∃!g~:E[Z,X]g=α∘g~∧pg~=h See also Used as part of Grothendieck Fibration.