Thanks for the responses to my question concerning Pfn. Barry Jay asked for a "real problem". Here is one from computer science. The following diagram is used in Abstract Interpretation, where a program is modelled extensionally, i.e. V and V' are sets of stores, f is a transition function with dom(f) being a possibly proper subset of V (e.g. a transition function corresponding to one of the branches of an if-statement.) Furthermore a and a' are abstraction functions, and we're interested in the pushout, to get a best possible abstract approximation f' to f. V ---f----> V' | | | | a a' | | | | A---f'---> A' Lars Birkedal (birkedal@diku.dk) ===================================================================