S. Awodey and M. A. Warren, Homotopy theoretic models of identity types, Mathematical Proceedings of the Cambridge Philosophical Society, vol.19, issue.01, pp.45-55, 2009.
DOI : 10.1016/0022-4049(77)90067-6

G. Gonthier, A. Asperti, J. Avigad, Y. Bertot, C. Cohen et al., A Machine-Checked Proof of the Odd Order Theorem, ITP 2013, 4th Conference on Interactive Theorem Proving, pp.163-179, 2013.
DOI : 10.1007/978-3-642-39634-2_14
URL : https://hal.archives-ouvertes.fr/hal-00816699

C. Thomas and . Hales, Cannonballs and honeycombs, Notices of the AMS, vol.47, issue.4, pp.440-449, 2000.

M. Hedberg, A coherence theorem for Martin-L??f's type theory, Journal of Functional Programming, vol.8, issue.4, pp.413-436, 1998.
DOI : 10.1017/S0956796898003153

M. Hofmann and T. Streicher, The groupoid interpretation of type theory In Twentyfive years of constructive type theory, Oxford Logic Guides, vol.36, pp.83-111, 1995.

P. Martin-löf, Intuitionistic type theories, Bibliopolis, 1984.

V. Voevodsky, Univalent foundations project, 2010.