I am writing a book on equational logic and theorem proving for final year undergraduates, and want to include a formal treatment of commutative diagrams. Actually, I have never seen a formal treatment for pasting commutative diagrams, though I would be surprised if none existed. The following is my attempt to find an approach which is both elementary and sufficiently general for the usual applications. (A diagram is of course a consistent labelling of a graph by sets on nodes and functions on edges; set theoretically it is a function, so it makes sense to take unions and intersections of diagrams, although I admit this is excessively concrete.) \bdfn A ?\bf bipath? is a diagram $P$ with given nodes $s,t$ called its ?\bf source? and ?\bf target?, and given paths $p,q$ from $s$ to $t$, such that $P$ is the union of $p,q$ and $p,q$ intersect only at $s$ and $t$. \edfn \blemma Let $P_0$ and $P_1$ be commutative bipaths that intersect in just one path (possibly empty or one point). Then $P = P_0 \cup P_1$ is a commutative diagram. \elemma We can use this in proving the following more general result, by induction on the number of commutative bipaths which intersect $p$ and $q$: \bprop Given a collection $P_i$ for $i \in I$ of commutative bipaths such that each pair intersects in one path (possibly empty or one point), then any two paths $p,q$ in $P = \bigcup_?i \in I? P_i$ which start at the same source and end at the same target form a commutative bipath. \eprop Given the lemma, the proposition has a reasonably nice proof. Unfortunately, I have no way to prove the lemma except by an exhausting case analysis. Thus I would be grateful to hear about an alternative approach; a ``reduction'' to some advanced topic (such as 2-categories) would be interesting to me, but not actually useful for the purpose at hand. With many thanks, Joseph &&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&& Joseph A. Goguen, Professor of Computing Science, Programming Research Group, University of Oxford, 11 Keble Road, Oxford OX1 3QD, United Kingdom. email: goguen@prg.ox.ac.uk ?on the internet -- should also work in the U.K. on janet, but if not, try goguen@uk.ac.ox.prg -- Joseph.Goguen@... also works? phone: 272567 ?my office?; 272568 ?secy?; 273838 ?PRG office?; 272839 ?FAX? from USA, dial 011-44-865-...; from UK, dial (0865)-...