A Syntactical Approach to Weak ?-Groupoids, LIPIcs-Leibniz International Proceedings in Informatics, vol.16, 2012. ,
Sur les ?-groupoïdes de Grothendieck et une variante ?-catégorique, 2010. ,
Monoidal Globular Categories As a Natural Environment for the Theory of Weak n-Categories, Advances in Mathematics, vol.136, issue.1, pp.39-103, 1998. ,
A cellular nerve for higher categories, Advances in Mathematics, vol.169, issue.1, pp.118-175, 2002. ,
On the homotopy groups of spheres in homotopy type theory, 2016. ,
URL : https://hal.archives-ouvertes.fr/tel-01333601
Generalised algebraic theories and contextual categories, Annals of Pure and Applied Logic, vol.32, pp.209-243, 1986. ,
Internal type theory, International Workshop on Types for Proofs and Programs, pp.120-134, 1995. ,
Opetopic ,
Pursuing stacks, 1983. ,
Disks, duality and ?-categories, 1997. ,
Weak ?-categories from intensional type theory, International Conference on Typed Lambda Calculi and Applications, pp.172-187, 2009. ,
Sheaves in geometry and logic: A first introduction to topos theory, 2012. ,
Grothendieck ?-groupoids, and still another definition of ?-categories, 2010. ,
Simply connected limits, Canadian Journal of Mathematics, vol.42, issue.4, pp.731-746, 1990. ,
Parity complexes, Cahiers de topologie et géométrie différentielle catégoriques, vol.32, pp.315-343, 1991. ,
, Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study, 2013.
Types are weak ?-groupoids, Proceedings of the London Mathematical Society, vol.102, issue.2, pp.370-394, 2011. ,
Globular: an online proof assistant for higher-dimensional rewriting, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016), vol.52, pp.1-11, 2016. ,