For the left diagram see Fibre products and coproducts in Top.
Now suppose (๐บ,๐1,๐2) fits into the following diagram.
%0A%20%20%20%20..%20controls%20(%24(%5Ctikztostart)!%5Cpv%7Bpos%7D!(%5Ctikztotarget)!%5Cpv%7Bheight%7D!270%3A(%5Ctikztotarget)%24)%0A%20%20%20%20and%20(%24(%5Ctikztostart)!1-%5Cpv%7Bpos%7D!(%5Ctikztotarget)!%5Cpv%7Bheight%7D!270%3A(%5Ctikztotarget)%24)%0A%20%20%20%20..%20(%5Ctikztotarget)%5Ctikztonodes%7D%7D%2C%0A%20%20%20%20settings%2F.code%3D%7B%5Ctikzset%7Bquiver%2F.cd%2C%231%7D%0A%20%20%20%20%20%20%20%20%5Cdef%5Cpv%23%231%7B%5Cpgfkeysvalueof%7B%2Ftikz%2Fquiver%2F%23%231%7D%7D%7D%2C%0A%20%20%20%20quiver%2F.cd%2Cpos%2F.initial%3D0.35%2Cheight%2F.initial%3D0%7D%0A%5Ctikzset%7Btail%20reversed%2F.code%3D%7B%5Cpgfsetarrowsstart%7Btikzcd%20to%7D%7D%7D%0A%5Ctikzset%7B2tail%2F.code%3D%7B%5Cpgfsetarrowsstart%7BImplies%5Breversed%5D%7D%7D%7D%0A%5Ctikzset%7B2tail%20reversed%2F.code%3D%7B%5Cpgfsetarrowsstart%7BImplies%7D%7D%7D%0A%5Ctikzset%7Bno%20body%2F.style%3D%7B%2Ftikz%2Fdash%20pattern%3Don%200%20off%201mm%7D%7D%0A%25%20https%3A%2F%2Fq.uiver.app%2F%23q%3DWzAsNSxbMCwwLCJcXHBpXzEoVSBcXGNhcCBWKSJdLFswLDIsIlxccGlfMShVKSJdLFsyLDIsIlxccGlfMShYKSJdLFsyLDAsIlxccGlfMShWKSJdLFs0LDQsIkciXSxbMCwzLCJcXHBpXzEgaV8yIl0sWzAsMSwiXFxwaV8xaV8xIiwyXSxbMSwyLCJcXHBpXzFqXzEiLDJdLFszLDIsIlxccGlfMmpfMiJdLFsyLDAsIiIsMSx7InN0eWxlIjp7Im5hbWUiOiJjb3JuZXIifX1dLFsxLDQsImZfMSIsMix7ImN1cnZlIjoxfV0sWzMsNCwiZl8yIiwwLHsiY3VydmUiOi0xfV0sWzIsNCwiZiIsMSx7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dXQ%3D%3D%0A%5Cbegin%7Btikzcd%7D%5Bampersand%20replacement%3D%5C%26%5D%0A%09%7B%5Cpi_1(U%20%5Ccap%20V)%7D%20%5C%26%5C%26%20%7B%5Cpi_1(V)%7D%20%5C%5C%0A%09%5C%5C%0A%09%7B%5Cpi_1(U)%7D%20%5C%26%5C%26%20%7B%5Cpi_1(X)%7D%20%5C%5C%0A%09%5C%5C%0A%09%5C%26%5C%26%5C%26%5C%26%20G%0A%09%5Carrow%5B%22%7B%5Cpi_1%20i_2%7D%22%2C%20from%3D1-1%2C%20to%3D1-3%5D%0A%09%5Carrow%5B%22%7B%5Cpi_1i_1%7D%22'%2C%20from%3D1-1%2C%20to%3D3-1%5D%0A%09%5Carrow%5B%22%7B%5Cpi_1j_1%7D%22'%2C%20from%3D3-1%2C%20to%3D3-3%5D%0A%09%5Carrow%5B%22%7B%5Cpi_2j_2%7D%22%2C%20from%3D1-3%2C%20to%3D3-3%5D%0A%09%5Carrow%5B%22%5Clrcorner%22%7Banchor%3Dcenter%2C%20pos%3D0.125%2C%20rotate%3D180%7D%2C%20draw%3Dnone%2C%20from%3D3-3%2C%20to%3D1-1%5D%0A%09%5Carrow%5B%22%7Bf_1%7D%22'%2C%20curve%3D%7Bheight%3D6pt%7D%2C%20from%3D3-1%2C%20to%3D5-5%5D%0A%09%5Carrow%5B%22%7Bf_2%7D%22%2C%20curve%3D%7Bheight%3D-6pt%7D%2C%20from%3D1-3%2C%20to%3D5-5%5D%0A%09%5Carrow%5B%22f%22%7Bdescription%7D%2C%20dashed%2C%20from%3D3-3%2C%20to%3D5-5%5D%0A%5Cend%7Btikzcd%7D%0A#invert)
We must show the existence of a unique ๐ such that the diagram commutes.
Uniqueness is the easier part to prove:
For objects (points), if ๐ฅ โ๐ then ๐๐ฅ =๐1๐ฅ;
if ๐ฅ โ๐ then ๐๐ฅ =๐2๐ฅ;
and if ๐ฅ โ๐ โฉ๐ the assignments agree.
For a homotopy path [๐พ] โ๐1๐(๐ฅ,๐ฆ) uniqueness follows from a representative ๐พ :๐ โ๐.
Using a Lebesgue number, ๐ may be evenly subdivided into sections either entirely in either ๐พโ1๐ or ๐พโ1๐,
giving paths ๐พ1,โฆ,๐พ๐ where ๐พ โ๐พ1โฏ๐พ๐
Thus ๐[๐พ] must agree with applying ๐1 and ๐2 to each component path,
which is clearly invariant under refinement and therefore independent of the precise decomposition.
For existence, we need to show that ๐ is independent of the representative ๐พ.
Let ๐พ0 โ๐พ1 by virtue of a homotopy of paths ๐ป :(๐ก,๐ ) โฆ๐พ๐ (๐ก).
Once again a Lebesgue number may be used to divide ๐2 into a ๐ ร๐ grid
such that each box is entirely in either ฮโ1๐ or ฮโ1๐.
Assign to the box with bottom-left corner at (๐๐,๐๐) the paths ๐๐,๐,๐๐+1,๐ :๐ โ๐2 rightwards along its top and bottom edges respectively,
and ๐๐,๐,๐๐,๐+1 :๐ โ๐2 upwards along its left and right edges respectively.
Clearly ๐๐,๐ โ
๐๐+1,๐ โ๐๐,๐ โ
๐๐+1,๐ as paths,
and ๐๐,๐ โ๐๐,๐ โ
๐๐+1,๐ โ
โโโโ๐๐+1,๐.
Since ฮ๐0,๐/๐ and ฮ๐1,๐/๐ are constant paths in either ๐ or ๐,
applying ฮ to get paths in ๐ for each ๐ =0,โฆ,๐
๐๐พ๐/๐=๐โจ๐=0๐โปฮ๐๐/๐,๐/๐=๐โจ๐=0๐โปฮ๐๐/๐,๐/๐โ๐โปฮ๐(๐+1)/๐,๐/๐โ๐โปฮโโโโโโ๐(๐+1)/๐,๐/๐=๐โปฮ๐0,๐/๐โ(๐โจ๐=0๐โปฮ๐(๐+1)/๐,๐/๐)โ๐โปฮโโโโ๐1,๐/๐=๐โจ๐=0๐โปฮ๐(๐+1)/๐,๐/๐=๐๐พ(๐+1)/๐where ๐โป denotes applying ๐1 or ๐2 depending on whether a path is in ๐ or ๐.
It follows from ๐ iterations that ๐๐พ0 =๐๐พ1.