T. Altenkirch, C. Mcbride, and W. Swierstra, Observational Equality , Now! In PLPV'07: Proceedings of the Programming Languages meets Program Verification Workshop, 2007.

T. Altenkirch and O. Rypacek, A Syntactical Approach to Weak omega- Groupoids, pp.16-30

A. Bauer and P. L. Lumsdaine, A Coq proof that Univalence Axioms implies Functional Extensionality, 2011.

P. Cégielski and A. Durand, Computer Science Logic (CSL'12) -26th International Workshop/21st Annual Conference of the EACSL, CSL 2012, of LIPIcs. Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, 2012.

R. Harper and R. Pollack, Type checking with universes, Theoretical Computer Science, vol.89, issue.1, pp.107-136, 1991.
DOI : 10.1016/0304-3975(90)90108-T

M. Hofmann and T. Streicher, The Groupoid Interpretation of Type Theory In Twenty-five years of constructive type theory, Oxford Logic Guides, vol.36, pp.83-111, 1995.

G. Jaber, N. Tabareau, and M. Sozeau, Extending Type Theory with Forcing, 2012 27th Annual IEEE Symposium on Logic in Computer Science, 2012.
DOI : 10.1109/LICS.2012.49
URL : https://hal.archives-ouvertes.fr/hal-00685150

C. Keller and M. Lasson, Parametricity in an Impredicative Sort, Cégielski and Durand [4], pp.381-395
URL : https://hal.archives-ouvertes.fr/hal-00730913

R. Daniel, R. Licata, and . Harper, Canonicity for 2-dimensional type theory, POPL, pp.337-348, 2012.

P. Lefanu-lumsdaine, A. Pelayo, and M. A. Warren, Weak omega-categories from intensional type theory Homotopy type theory and Voevodsky's univalent foundations, Logical Methods in Computer Science, vol.6, issue.3 11, 2010.

M. Sozeau, Program-ing Finger Trees in Coq, ICFP'07: Proceedings of the 2007 ACM SIGPLAN International Conference on Functional Programming, pp.13-24, 2007.

M. Sozeau and N. Oury, First-Class Type Classes, Theorem Proving in Higher Order Logics, 21th International Conference, pp.278-293, 2008.
DOI : 10.1007/11542384_8
URL : https://hal.archives-ouvertes.fr/inria-00628864