[1]:http://groupoids.org.uk/topgpds.html [2]:http://mathoverflow.net/questions/130116/130156#130156 [3]:http://www.tac.mta.ca/tac/volumes/10/2/10-02abs.html [4]:http://groupoids.org.uk/nonab-a-t.html [5]:http://ncatlab.org/nlab/show/homological+perturbation+theory [6]:http://hamilton.nuigalway.ie/Hap/www/ [7]:http://www.intlpress.com/HHA/v1/n1/a4/ [8]:http://groupoids.org.uk/images/rotations.jpg @Harry Gindi: I had the same problem in the 1960s when writing the first 1968 edition of my book now [Topology and Groupoids][1]. Then I was looking at papers of Puppe, and found I had no idea how to construct some of their "diagrammatic" homotopies. with different formulae in each bit. This was part of the motivation for finding the gluing theorem for homotopy equivalences, which is now a standard result in abstract homotopy. My [answer][2] to another question illustrates how one gets by the methods there explicit homotopies. There was the same motivation for using double groupoids in homotopy theory. Using the double groupoid defined [here][3] one can enrich the category of Hausdorff spaces over the category of these double groupoids with connection (though this has not been written up in detail) and this can be applied to construct homotopies. For some calculations in double groupoids with connections, see Chapter 6 of [Nonabelian Algebraic Topology][4], particularly on rotations (p.169). One can also enrich the category of filtered spaces over the symmetric monoidal closed category of crossed complexes, and this again enables calculations of homotopies. As said on p.322 of [Nonabelian Algebraic Topology][4], this requires further study. I am not so sure that the work on model categories helps so directly with the calculation of homotopies, unles the cylinder object is used explicit;ly. The use of homotopies is central to [Homological Perturbation Theory][5], and they are used in Graham Ellis' [Homological Algebra Programs][6], in particular for constructing resolutions by induction with a contracting homotopy. This [paper][7] uses higher homotopy groupoids to discuss Toda brackets. My own work has largely used cubical methods as a background for conjectures and proofs, because of the ease of describing multiple compositions, and homotopies. June, 2014 I remember a comment of Raoul Bott which I overheard at the 1958 ICM: "Grothendieck was prepared to work very hard to make things tautological!" March 2016 The following picture ![rotations][8] is part of the argument for proving a formula $\sigma (u +_2 v)= \sigma u +_1 \sigma v$ where $u,v$ are homotopy classes rel vertices of maps $I^2 \to X$ which take the edges to a subspace $A$ and the vertices to a set $C$ of base points, $+_1, +_2$ denote respectively compositions in the vertical and horizontal directions, and $\sigma$ is what is called a "rotation". The diagram is reinterpreted by using the interchange law and rules among the peculiar symbols called "connections". The formula implies the existence of a homotopy and in principal gives it explicitly, but that would be very difficult to write out in terms of the usual type of formulae.