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.

oldarrows, which would give you ⌜ for a pushout. $\endgroup$ – Dmitri Pavlov Mar 29 '17 at 11:20