History of the pullback corner notation

Where/when did the convention originate of marking pullback (and/or pushout) squares by that little right-angle symbol in the corner?

The earliest instance I’ve been able to find is in Paul Taylor’s diagrams package, from ≤1994, as mentioned in e.g. the changelog notes for v3.81 at http://www.paultaylor.eu/diagrams/ . But it seems more likely that this was to meet the demand for a notation that was already established, rather than being the origin? But looking at various well-known category theory textbooks from before 2000 (Mac Lane Categories for the Working Mathematician; Mac Lane and Moerdijk Sheaves in Geometry and Logic; Borceux Handbook of Categorical Algebra; Johnstone Topos Theory), none of them seem to use it, as far as I can find.

• @ToddTrimble I strongly suspect it has been invented by him. I've seen it in several papers of Peter Freyd, as well as in Cats and Allegators. The latter is full of notation I wish would become standard, like puncture sign for non-commuting diagrams. – მამუკა ჯიბლაძე Mar 26 '17 at 19:09
• Indeed, the Freyd-Scedrov book from 1990 has the notation: books.google.com/… – Todd Trimble Mar 26 '17 at 19:11
• While we're at it maybe we can standardize this notation too? I've seen that right angle all over the place and pointing in several different directions. – Jonathan Beardsley Mar 27 '17 at 4:49
• In Freyd's notation the corner is actually attached to the arrows. He also seems to use a similar cross notation for products, and several other notations for (co)equalizers etc. – Dmitri Pavlov Mar 27 '17 at 9:41
• @მამუკაჯიბლაძე: That's one point of view (i.e., a corner is an arrowhead). Another point of view states that a corner is meant to represent the two newly constructed arrows; in the case of a pushout these two arrows give you ⌟. And a third point of view states that a corner is meant to represent the two old arrows, which would give you ⌜ for a pushout. – Dmitri Pavlov Mar 29 '17 at 11:20