> > Why is there no LOG in this? It's a little messy to write out the actual details, but it is possible for each map f : X -> Y to use the subobject classifier and dependent products to construct a "universal lifting problem" for f, where universal means that every other lifting problem against a pushout product of monomorphism and i-endpoint inclusion factors uniquely as a pullback followed by the universal lifting problem. Then, once a filler for the universal lifting problem has been chosen, it can be used to construct a filler for all the other lifting problems. (This can also be seen as an instance of a general result that holds in any locally small fibration with finitely complete base).