?. A. If, if ? a = b : A, then

. Aczel, On Relating Type Theories and Set Theories, Types for Proofs and Programs, pp.1-18, 1999.
DOI : 10.1007/3-540-48167-2_1

. Altenkirch, Extensional equality in intensional type theory, Proceedings. 14th Symposium on Logic in Computer Science (Cat. No. PR00158), pp.412-420, 1999.
DOI : 10.1109/LICS.1999.782636

T. Bezem, S. Coquand, and . Huber, A Model of Type Theory in Cubical Sets, 19th International Conference on Types for Proofs and Programs of Leibniz International Proceedings in Informatics (LIPIcs), pp.107-128, 2013.

P. J. Brown, R. Higgins, and . Sivera, Nonabelian Algebraic Topology: Filtered Spaces, Crossed Complexes, Cubical Homotopy Groupoids, volume 15 of EMS tracts in mathematics, 2011.
DOI : 10.4171/083

-. Cisinski, Univalent universes for elegant models of homotopy types, 2014.

. Dybjer, Internal type theory, In Lecture Notes in Computer Science, pp.120-134
DOI : 10.1007/3-540-61780-9_66

D. Fourman and . Scott, Sheaves and logic, Applications of Sheaves Gambino and C. Sattler. Uniform Fibrations and the Frobenius Condition, pp.302-401, 1979.
DOI : 10.1007/BFb0061296

. Hofmann, Syntax and semantics of dependent types, Semantics and logics of computation, pp.79-130, 1997.

M. Kan, ABSTRACT HOMOTOPY, Proceedings of the National Academy of Sciences of the United States of America, pp.1092-1096, 1955.
DOI : 10.1073/pnas.41.12.1092

P. Kapulkin, V. Lefanu-lumsdaine, and . Voevodsky, The Simplicial Model of Univalent Foundations, 2012.

R. Licata and G. Brunerie, A Cubical Approach to Synthetic Homotopy Theory, 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science, pp.92-103, 2015.
DOI : 10.1109/LICS.2015.19
URL : https://hal.archives-ouvertes.fr/hal-01322397

. Martin-löf, An Intuitionistic Theory of Types: Predicative Part, Logic Colloquium '73, pp.73-118, 1973.
DOI : 10.1016/S0049-237X(08)71945-1

. Martin-löf, An intuitionistic theory of types, Twenty-five years of constructive type theory of Oxford Logic Guides, pp.127-172, 1995.

M. Pitts, Nominal Sets: Names and Symmetry in Computer Science
DOI : 10.1017/CBO9781139084673

M. Pitts, Nominal Presentation of Cubical Sets Models of Type Theory, 20th International Conference on Types for Proofs and Programs of Leibniz International Proceedings in Informatics (LIPIcs) Schloss Dagstuhl ? Leibniz-Zentrum fuer Informatik, pp.202-220, 2014.

. Streicher, Semantics of Type Theory, Progress in Theoretical Computer Science. Birkhäuser Basel, 1991.
DOI : 10.1007/978-1-4612-0433-6

. Swan, An Algebraic Weak Factorisation System on 01-Substitution Sets: A Constructive Proof. arXiv:1409.1829, 2013.

. Voevodsky, The equivalence axiom and univalent models of type theory. (Talk at CMU on, 2010.