\def\cprime{$'$}
\begin{thebibliography}{10}

\bibitem{RezkCompletion}
Benedikt Ahrens, Chris Kapulkin, and Michael Shulman.
\newblock Univalent categories and {R}ezk completion.
\newblock {\em To appear in Mathematical Structures in Computer Science
  (arXiv:1303.0584)}, 2011.

\bibitem{Coquand}
Thierry Coquand and G{\'e}rard Huet.
\newblock The calculus of constructions.
\newblock {\em Inform. and Comput.}, 76(2-3):95--120, 1988.

\bibitem{Esquisse}
Alexandre Grothendieck.
\newblock Esquisse d'un programme.
\newblock In {\em Geometric {G}alois actions, 1}, volume 242 of {\em London
  Math. Soc. Lecture Note Ser.}, pages 5--48. Cambridge Univ. Press, Cambridge,
  1997.
\newblock With an English translation on pp. 243--283.

\bibitem{KLV1}
Chris Kapulkin, Peter~LeFanu Lumsdaine, and Vladimir Voevodsky.
\newblock The simplicial model of univalent foundations.
\newblock {\em Preprint, arXiv:1211.2851}, 2012.

\bibitem{Luo}
Zhaohui Luo.
\newblock {\em Computation and reasoning}, volume~11 of {\em International
  Series of Monographs on Computer Science}.
\newblock The Clarendon Press, Oxford University Press, New York, 1994.
\newblock A type theory for computer science.

\bibitem{Makkai}
M.~Makkai.
\newblock First order logic with dependent sorts, with applications to category
  theory.
\newblock {\em Preprint, Available on the web}, Nov. 6, 1995.

\bibitem{Mohring1}
Christine Paulin-Mohring.
\newblock Inductive definitions in the system {C}oq; rules and properties.
\newblock In {\em Typed lambda calculi and applications ({U}trecht, 1993)},
  volume 664 of {\em Lecture Notes in Comput. Sci.}, pages 328--345. Springer,
  Berlin, 1993.

\bibitem{PVW1}
A.~Pelayo, V.~Voevodsky, and M.~A. Warren.
\newblock A preliminary univalent formalization of the p-adic numbers.
\newblock {\em Submitted to Mathematical Structures in Computer Science
  (arXiv:1302.1207)}, 2013.

\bibitem{hottbook}
{Univalent Foundations Project}.
\newblock {\em Homotopy Type Theory: Univalent Foundations for Mathematics}.
\newblock \url{http://homotopytypetheory.org/book}, Institute for Advanced
  Study, 2013.

\bibitem{VUFresizingslides}
Vladimir Voevodsky.
\newblock Resizing rules, slides from a talk at {TYPES2011}.
\newblock {\em At author's webpage}, 2011.

\end{thebibliography}