[solomonb]

Yeah I understand that the existence of the commutative diagram implies that it typechecks. I was trying to give OP a basic intuition for them. I should have said something like:

If you follow the two paths around the square you will find that everything typechecks correctly and both paths get you to the same result. This shows how the two paths are equal in some sense.