\documentclass[12pt,titlepage]{article}

\usepackage{amsmath}
\usepackage{mathrsfs}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{mathtools}
\usepackage{graphicx}
\usepackage{color}
\usepackage{ucs}
\usepackage[utf8x]{inputenc}
\usepackage{xparse}
\usepackage{hyperref}

%----Macros----------
%
% Unresolved issues:
%
%  \righttoleftarrow
%  \lefttorightarrow
%
%  \color{} with HTML colorspec
%  \bgcolor
%  \array with options (without options, it's equivalent to the matrix environment)

% Of the standard HTML named colors, white, black, red, green, blue and yellow
% are predefined in the color package. Here are the rest.
\definecolor{aqua}{rgb}{0, 1.0, 1.0}
\definecolor{fuschia}{rgb}{1.0, 0, 1.0}
\definecolor{gray}{rgb}{0.502, 0.502, 0.502}
\definecolor{lime}{rgb}{0, 1.0, 0}
\definecolor{maroon}{rgb}{0.502, 0, 0}
\definecolor{navy}{rgb}{0, 0, 0.502}
\definecolor{olive}{rgb}{0.502, 0.502, 0}
\definecolor{purple}{rgb}{0.502, 0, 0.502}
\definecolor{silver}{rgb}{0.753, 0.753, 0.753}
\definecolor{teal}{rgb}{0, 0.502, 0.502}

% Because of conflicts, \space and \mathop are converted to
% \itexspace and \operatorname during preprocessing.

% itex: \space{ht}{dp}{wd}
%
% Height and baseline depth measurements are in units of tenths of an ex while
% the width is measured in tenths of an em.
\makeatletter
\newdimen\itex@wd%
\newdimen\itex@dp%
\newdimen\itex@thd%
\def\itexspace#1#2#3{\itex@wd=#3em%
\itex@wd=0.1\itex@wd%
\itex@dp=#2ex%
\itex@dp=0.1\itex@dp%
\itex@thd=#1ex%
\itex@thd=0.1\itex@thd%
\advance\itex@thd\the\itex@dp%
\makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}}
\makeatother

% \tensor and \multiscript
\makeatletter
\newif\if@sup
\newtoks\@sups
\def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}%
\def\reset@sup{\@supfalse\@sups={}}%
\def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else%
  \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}%
  \else \append@sup#2 \@suptrue \fi%
  \expandafter\mk@scripts\fi}
\def\tensor#1#2{\reset@sup#1\mk@scripts#2_/}
\def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2%
  \reset@sup\mk@scripts#3_/}
\makeatother

% \slash
\makeatletter
\newbox\slashbox \setbox\slashbox=\hbox{$/$}
\def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$}
  \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa
  \copy\slashbox \kern-\@tempdima \box\@tempboxa}
\def\slash{\protect\itex@pslash}
\makeatother

% math-mode versions of \rlap, etc
% from Alexander Perlis, "A complement to \smash, \llap, and lap"
%   http://math.arizona.edu/~aprl/publications/mathclap/
\def\clap#1{\hbox to 0pt{\hss#1\hss}}
\def\mathllap{\mathpalette\mathllapinternal}
\def\mathrlap{\mathpalette\mathrlapinternal}
\def\mathclap{\mathpalette\mathclapinternal}
\def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}}
\def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}}
\def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}}

% Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2}
\let\oldroot\root
\def\root#1#2{\oldroot #1 \of{#2}}
\renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}}

% Manually declare the txfonts symbolsC font
\DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n}
\SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n}
\DeclareFontSubstitution{U}{txsyc}{m}{n}

% Manually declare the stmaryrd font
\DeclareSymbolFont{stmry}{U}{stmry}{m}{n}
\SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n}

% Manually declare the MnSymbolE font
\DeclareFontFamily{OMX}{MnSymbolE}{}
\DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n}
\SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n}
\DeclareFontShape{OMX}{MnSymbolE}{m}{n}{
    <-6>  MnSymbolE5
   <6-7>  MnSymbolE6
   <7-8>  MnSymbolE7
   <8-9>  MnSymbolE8
   <9-10> MnSymbolE9
  <10-12> MnSymbolE10
  <12->   MnSymbolE12}{}

% Declare specific arrows from txfonts without loading the full package
\makeatletter
\def\re@DeclareMathSymbol#1#2#3#4{%
    \let#1=\undefined
    \DeclareMathSymbol{#1}{#2}{#3}{#4}}
\re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46}
\re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12}
\re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64}
\re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6}
\re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77}
\re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77}
\makeatother

% \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE
\makeatletter
\def\Decl@Mn@Delim#1#2#3#4{%
  \if\relax\noexpand#1%
    \let#1\undefined
  \fi
  \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}}
\def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}}
\def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}}
\Decl@Mn@Open{\llangle}{mnomx}{'164}
\Decl@Mn@Close{\rrangle}{mnomx}{'171}
\Decl@Mn@Open{\lmoustache}{mnomx}{'245}
\Decl@Mn@Close{\rmoustache}{mnomx}{'244}
\makeatother

% Widecheck
\makeatletter
\DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}}
\def\@widecheck#1#2{%
    \setbox\z@\hbox{\m@th$#1#2$}%
    \setbox\tw@\hbox{\m@th$#1%
       \widehat{%
          \vrule\@width\z@\@height\ht\z@
          \vrule\@height\z@\@width\wd\z@}$}%
    \dp\tw@-\ht\z@
    \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@
    \setbox\tw@\hbox{%
       \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box
\tw@}}}%
    {\ooalign{\box\tw@ \cr \box\z@}}}
\makeatother

% \mathraisebox{voffset}[height][depth]{something}
\makeatletter
\NewDocumentCommand\mathraisebox{moom}{%
\IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{%
\IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}%
}{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}%
\mathpalette\@temp{#4}}
\makeatletter

% udots (taken from yhmath)
\makeatletter
\def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.}
\mkern2mu\raise4\p@\hbox{.}\mkern1mu
\raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}}
\makeatother

%% Fix array
\newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}}
%% \itexnum is a noop
\newcommand{\itexnum}[1]{#1}

%% Renaming existing commands
\newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}}
\newcommand{\widevec}{\overrightarrow}
\newcommand{\darr}{\downarrow}
\newcommand{\nearr}{\nearrow}
\newcommand{\nwarr}{\nwarrow}
\newcommand{\searr}{\searrow}
\newcommand{\swarr}{\swarrow}
\newcommand{\curvearrowbotright}{\curvearrowright}
\newcommand{\uparr}{\uparrow}
\newcommand{\downuparrow}{\updownarrow}
\newcommand{\duparr}{\updownarrow}
\newcommand{\updarr}{\updownarrow}
\newcommand{\gt}{>}
\newcommand{\lt}{<}
\newcommand{\map}{\mapsto}
\newcommand{\embedsin}{\hookrightarrow}
\newcommand{\Alpha}{A}
\newcommand{\Beta}{B}
\newcommand{\Zeta}{Z}
\newcommand{\Eta}{H}
\newcommand{\Iota}{I}
\newcommand{\Kappa}{K}
\newcommand{\Mu}{M}
\newcommand{\Nu}{N}
\newcommand{\Rho}{P}
\newcommand{\Tau}{T}
\newcommand{\Upsi}{\Upsilon}
\newcommand{\omicron}{o}
\newcommand{\lang}{\langle}
\newcommand{\rang}{\rangle}
\newcommand{\Union}{\bigcup}
\newcommand{\Intersection}{\bigcap}
\newcommand{\Oplus}{\bigoplus}
\newcommand{\Otimes}{\bigotimes}
\newcommand{\Wedge}{\bigwedge}
\newcommand{\Vee}{\bigvee}
\newcommand{\coproduct}{\coprod}
\newcommand{\product}{\prod}
\newcommand{\closure}{\overline}
\newcommand{\integral}{\int}
\newcommand{\doubleintegral}{\iint}
\newcommand{\tripleintegral}{\iiint}
\newcommand{\quadrupleintegral}{\iiiint}
\newcommand{\conint}{\oint}
\newcommand{\contourintegral}{\oint}
\newcommand{\infinity}{\infty}
\newcommand{\bottom}{\bot}
\newcommand{\minusb}{\boxminus}
\newcommand{\plusb}{\boxplus}
\newcommand{\timesb}{\boxtimes}
\newcommand{\intersection}{\cap}
\newcommand{\union}{\cup}
\newcommand{\Del}{\nabla}
\newcommand{\odash}{\circleddash}
\newcommand{\negspace}{\!}
\newcommand{\widebar}{\overline}
\newcommand{\textsize}{\normalsize}
\renewcommand{\scriptsize}{\scriptstyle}
\newcommand{\scriptscriptsize}{\scriptscriptstyle}
\newcommand{\mathfr}{\mathfrak}
\newcommand{\statusline}[2]{#2}
\newcommand{\tooltip}[2]{#2}
\newcommand{\toggle}[2]{#2}

% Theorem Environments
\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{prop}{Proposition}
\newtheorem{cor}{Corollary}
\newtheorem*{utheorem}{Theorem}
\newtheorem*{ulemma}{Lemma}
\newtheorem*{uprop}{Proposition}
\newtheorem*{ucor}{Corollary}
\theoremstyle{definition}
\newtheorem{defn}{Definition}
\newtheorem{example}{Example}
\newtheorem*{udefn}{Definition}
\newtheorem*{uexample}{Example}
\theoremstyle{remark}
\newtheorem{remark}{Remark}
\newtheorem{note}{Note}
\newtheorem*{uremark}{Remark}
\newtheorem*{unote}{Note}

%-------------------------------------------------------------------

\begin{document}

%-------------------------------------------------------------------


\section*{homotopy type theory}

\hypertarget{context}{}\subsubsection*{{Context}}\label{context}

\hypertarget{type_theory}{}\paragraph*{{Type theory}}\label{type_theory}

[[!include type theory - contents]]

\hypertarget{constructivism_realizability_computability}{}\paragraph*{{Constructivism, Realizability, Computability}}\label{constructivism_realizability_computability}

[[!include constructivism - contents]]

\hypertarget{homotopy_theory}{}\paragraph*{{Homotopy theory}}\label{homotopy_theory}

[[!include homotopy - contents]]

\hypertarget{topos_theory}{}\paragraph*{{$(\infty,1)$-Topos Theory}}\label{topos_theory}

[[!include (infinity,1)-topos - contents]]

\hypertarget{foundations}{}\paragraph*{{Foundations}}\label{foundations}

[[!include foundations - contents]]

\hypertarget{contents}{}\section*{{Contents}}\label{contents}

\noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak
\noindent\hyperlink{properties}{Properties}\dotfill \pageref*{properties} \linebreak
\noindent\hyperlink{Advantages}{Advantages}\dotfill \pageref*{Advantages} \linebreak
\noindent\hyperlink{models_in_categories_and_toposes}{Models in $(\infty,1)$-categories and $(\infty,1)$-toposes}\dotfill \pageref*{models_in_categories_and_toposes} \linebreak
\noindent\hyperlink{new_axioms}{New Axioms}\dotfill \pageref*{new_axioms} \linebreak
\noindent\hyperlink{relation_to_representation_theory}{Relation to representation theory}\dotfill \pageref*{relation_to_representation_theory} \linebreak
\noindent\hyperlink{machine_implementation}{Machine implementation}\dotfill \pageref*{machine_implementation} \linebreak
\noindent\hyperlink{DictionaryToCoq}{Dictionary HoTT-Coq / $(\infty,1)$-Category theory}\dotfill \pageref*{DictionaryToCoq} \linebreak
\noindent\hyperlink{related_entries}{Related entries}\dotfill \pageref*{related_entries} \linebreak
\noindent\hyperlink{References}{References}\dotfill \pageref*{References} \linebreak
\noindent\hyperlink{Introductions}{Introductions}\dotfill \pageref*{Introductions} \linebreak
\noindent\hyperlink{general}{General}\dotfill \pageref*{general} \linebreak
\noindent\hyperlink{models_and_categorical_semantics}{Models and categorical semantics}\dotfill \pageref*{models_and_categorical_semantics} \linebreak
\noindent\hyperlink{syntax}{Syntax}\dotfill \pageref*{syntax} \linebreak
\noindent\hyperlink{Code}{Code}\dotfill \pageref*{Code} \linebreak


\hypertarget{idea}{}\subsection*{{Idea}}\label{idea}

\emph{Homotopy type theory} is a flavor of \emph{[[type theory]]} -- specifically of [[intensional type theory|intensional]] ([[Martin-Löf type theory|Martin-Löf]]-)[[dependent type theory]] -- which takes seriously the natural interpretation of \emph{[[identity types]]} as formalizing [[path space objects]] in [[homotopy theory]].

In the [[categorical semantics of homotopy type theory]], [[types]] are interpreted not as [[set]]-like [[objects]], but as [[homotopy type]]- or [[∞-groupoid]]/[[∞-stack]]-like objects. Thus, whereas [[extensional type theory]] can serve as the [[internal language]] of [[1-categories]] (such as [[pretoposes]], [[locally cartesian closed categories]], or [[elementary toposes]]), homotopy type theory can serve as an internal language for various kinds of [[(∞,1)-category]] (such as [[locally cartesian closed (∞,1)-categories]] and [[(∞,1)-toposes]]). At present, such models are usually constructed by way of 1-categorical [[presentable (infinity,1)-category|presentations]] of (∞,1)-categories using [[type-theoretic model categories]] and related structures such as [[weak factorization systems]].

In addition to a viewpoint on identity types and a general class of categorical models, homotopy type theory is characterized by new homotopically motivated axioms and type-theoretic structures. Notable among these are:

\begin{itemize}%
\item Voevodsky's [[univalence axiom]], which represents [[object classifiers]] in (∞,1)-categorical semantics.


\item Strong [[function extensionality]], which is a consequence of univalence.


\item [[higher inductive type|Higher inductive types]], which among other things enable the construction of finite [[(∞,1)-colimits]], [[cell complexes]], [[n-truncated|truncations]], [[localizations]], and other objects which in classical homotopy theory are constructed using the [[small object argument]].



\end{itemize}
With all of these axioms included, homotopy type theory behaves like the [[internal language of an (∞,1)-topos]], and conjecturally should admit actual models in any [[(∞,1)-topos]]. With fewer axioms and type constructors, it is known to admit models in more weakly structured [[(∞,1)-categories]] --- see below.

Many details are still being worked out, but the impression is that homotopy type theory thus should serve as a [[foundation]] for [[mathematics]] that is natively about [[homotopy theory]]/[[(∞,1)-category theory]] --- in other words, a foundation in which \emph{[[homotopy types]]}, rather than [[sets]], are basic objects.

\hypertarget{properties}{}\subsection*{{Properties}}\label{properties}

\hypertarget{Advantages}{}\subsubsection*{{Advantages}}\label{Advantages}

As a [[foundation]] for [[mathematics]], homotopy type theory (also called \textbf{univalent foundations}) has the following advantages. Many of these advantages are shared with some other foundational systems, but no other known system shares all of these, and some are unique to HoTT.

\begin{itemize}%
\item It treats [[homotopy theory]] and [[∞-groupoids]] natively. This is an advantage for doing homotopical and [[higher category theory|higher-categorical]] mathematics, which is spreading slowly into other fields.


\item It inherits the good computational properties of intensional [[Martin-Löf type theory]]. Some of its new axioms, such as [[univalence]] and [[function extensionality]], are not fully understood yet from a computational perspective, but progress is being made. This paragraph should be updated in view of the computational interpretation of univalence by the cubical model.


\item It is [[constructive mathematics|constructive]] by default, but can easily be made [[classical logic|classical]] by adding axioms. This makes it potentially more expressive at essentially no cost. (In fact, it is not entirely clear how possible it is to do homotopy theory constructively in other foundations.)


\item It can (conjecturally) be [[internalization|internalized]] in many categories and higher categories, providing an [[internal logic]] which enables a single [[proof]] to be reinterpreted in many places with many different meanings.


\item It is naturally [[isomorphism]]- and [[equivalence]]-invariant (non-[[evil]]). This is a consequence of the [[univalence axiom]]: any property or structure (even one which speaks only about [[sets]] and makes no reference to homotopy theory) which is expressible in the theory must be invariant under isomorphism/equivalence.


\item Notions such as [[propositions]] and sets are \emph{defined} objects, which inherit good computational properties from the underlying type theory.


\item It treats sets, [[groupoids]], and [[n-groupoid|higher groupoids]] on an equal footing. One can easily remain entirely in the fragment of the theory which talks about sets, not worrying about groupoids or homotopy theory, but as soon as one starts to say something which naturally needs structures of higher [[homotopy level]] (such as talking about some collection of structured sets), the groupoidal and homotopical structure is already there.



\end{itemize}
\hypertarget{models_in_categories_and_toposes}{}\subsubsection*{{Models in $(\infty,1)$-categories and $(\infty,1)$-toposes}}\label{models_in_categories_and_toposes}

It is well known that [[extensional type theory|extensional]] [[dependent type theory]] is an [[internal logic]] for [[locally cartesian closed categories]]. See at \emph{[[relation between type theory and category theory]]}.

The step from extensional to [[intensional type theory]] and the [[identity types]] that this brings with it makes intensional dependent type theory have models in certain [[(∞,1)-categories]]. This connection is usually shown by means of a presentation of the $(\infty,1)$-category using a [[weak factorization system]], a [[category of fibrant objects]], a [[model category]], or other similar structure.

It is conjectured (due to \hyperlink{Awodey09}{Awodey 09}, \hyperlink{Awodey}{Awodey, 2010}, \hyperlink{Joyal11}{Joyal, 2011}, see [[Awodey's conjecture]]) that

\begin{itemize}%
\item intensional dependent type theory with dependent sums and products and [[function extensionality]] (a form of homotopy type theory) is an internal language for [[locally cartesian closed (∞,1)-categories]]; and


\item with the [[univalence axiom]] added, it becomes an internal language for [[(∞,1)-toposes]].



\end{itemize}
Indeed:

\begin{prop}
\label{}\hypertarget{}{}
Every [[presentable (∞,1)-category|presentable]] and [[locally cartesian closed (∞,1)-category]] has a presentation by a [[type-theoretic model category]]. This provides the [[categorical semantics]] for [[homotopy type theory]] (without, possibly, the [[univalence]] [[axiom]]).

\end{prop}
For more on this see at \emph{[[locally cartesian closed (∞,1)-category]]} in the section on internal logic.

With the [[univalence]] axiom included (for a [[type of types]] ``weakly a la Tarski'') then homotopy type theory has categorical semantics in [[(∞,1)-toposes]], with the [[type of types]] interpreted as the [[object classifier]].

\begin{itemize}%
\item [[homotopytypetheory:model of type theory in an (infinity,1)-topos]]

\end{itemize}
See also at \emph{\href{relation+between+type+theory+and+category+theory#HomotopyWithUnivalence}{relation between type theory and category theory -- Univalent homotopy type theory and infinity-toposes}}.

For a short introduction to a simplicial model of homotopy type theory see [[T. Streicher - a model of type theory in simplicial sets - a brief introduction to Voevodsky' s homotopy type theory]].

\hypertarget{new_axioms}{}\subsubsection*{{New Axioms}}\label{new_axioms}

As a foundation for mathematics whose basic objects are higher groupoids, homotopy type theory makes visible new foundational axioms. Most of these axioms are true as statements about classical $\infty$-groupoids, but may be false in ``nonclassical'' models of homotopy type theory such as [[(∞,1)-toposes]].

\begin{itemize}%
\item [[Whitehead's principle]].


\item [[sets cover]], and more generally [[n-types cover]].


\item Several variants of the [[axiom of choice]].



\end{itemize}
Additionally, since homotopy type theory as the internal language of $(\infty, 1)$-toposes is not classical, it is possible to add classically inconsistent axioms, just as, say, the [[Kock-Lawvere axiom]] may be added to ordinary topos theory.

\begin{itemize}%
\item Axiom R (\href{cohesive+homotopy+type+theory#Shulman15}{Shulman 15})

\end{itemize}
\hypertarget{relation_to_representation_theory}{}\subsubsection*{{Relation to representation theory}}\label{relation_to_representation_theory}

[[!include homotopy type representation theory -- table]]

\hypertarget{machine_implementation}{}\subsection*{{Machine implementation}}\label{machine_implementation}

An important aspect of HoTT is the fact that the [[intensional type theory|intensional]] [[Martin-Löf type theory]] on which it is built has a computational implementation in proof assistants like [[Coq]] and [[Agda]].

This forms the basis of the \emph{Univalent Foundations} program (\hyperlink{Voevodsky}{Voevodsky}), which uses Coq to generate and verify proofs with [[homotopy theory|homotopical]] content.

See the \href{http://homotopytypetheory.org/coq/}{code page} at the \hyperlink{HoTTSite}{HoTT site} for more.

\hypertarget{DictionaryToCoq}{}\subsection*{{Dictionary HoTT-Coq / $(\infty,1)$-Category theory}}\label{DictionaryToCoq}

The following list displays some keywords defined in the [[Coq]]-implementation of homotopy type theory together with their meaning in the [[homotopy theory]]/[[(∞,1)-category theory]] that they describe. (See also at \emph{[[categorical semantics]]} and \emph{[[categorical semantics of homotopy type theory]]}.)

Let $C$ be a given ambient [[(∞,1)-category]] which

\begin{itemize}%
\item is [[locally cartesian closed (∞,1)-category|locally cartesian closed]];


\item in addition has [[(∞,1)-colimits]].



\end{itemize}
For instance $C$ could be an [[(∞,1)-topos]] (in which case the homotopy type theory would be the [[internal language of an (∞,1)-topos]]).

Note that while Coq-HoTT is supposed to be the internal language for such $C$, the \emph{strict [[models]]} for it are actually [[homotopical category|homotopical]] [[1-categories]] equipped with extra structure (such as [[model categories]] or [[categories of fibrant objects]]) that make them serve as [[presentable (infinity,1)-categories|presentations]] for $C$.

We then have the following dictionary.

The [[type of types]] [[Type]]

\begin{verbatim}Type\end{verbatim}
denotes an [[object classifier]] in $C$ for a certain size of [[universe]]. Both [[Coq]] and [[Agda]] have systems to manage universe sizes and [[universe enlargement]] automatically; Agda's is more advanced (universe polymorphism), whereas Coq's is good enough for many purposes but tends to produce ``universe inconsistencies'' when working with [[univalence]]. As a stopgap measure until this is improved, some HoTT code must be compiled with a patch to Coq that turns off all universe consistency checks.

A [[term]] of [[type]] Type (in the empty [[context]])

\begin{verbatim}X : Type\end{verbatim}
denotes an [[object]] in the $(\infty,1)$-category $C$. In a presentation of $C$ by a model category or [[weak factorization system]], it denotes a \emph{fibrant} object.

The [[unit type]]

\begin{verbatim}unit : Type\end{verbatim}
is the [[terminal object in an (∞,1)-category|terminal object]].

For $X, Y \in C$ two objects, the [[function type]]

\begin{verbatim}X -> Y : Type\end{verbatim}
denotes the [[internal hom]] $[X,Y] \in C$ (a formal proof of that fact is \href{https://github.com/guillaumebrunerie/HoTT/blob/master/Coq/Limits/AdjunctionProdHom.v}{here}).

A [[dependent type]] (that is, a type in [[context]])

\begin{verbatim}x : X  |-  P x : Type\end{verbatim}
denotes a [[morphism]] $P \to X$ (regarded as a [[fibration]] or [[bundle]]) in $C$. In a [[presentable (∞,1)-category|presentation]] of $C$ by a [[category of fibrant objects]], it literally denotes a [[fibration]] $P \to X$. In this case,

\begin{verbatim}P : X -> Type\end{verbatim}
denotes the corresponding classifying map, via an internal [[(∞,1)-Grothendieck construction]].

The total space object $P$ of this bundle -- the \emph{[[dependent sum type]]} -- is the type equivalently coded as any of the following.

\begin{verbatim}{ x : X  &  P x } : Type
sigT (fun (x : X) => P x) : Type.
sigT P : Type\end{verbatim}
The first one is [[sugaring|syntactic sugar]] for the second. The third is related to the second by [[eta expansion]], which (assuming [[function extensionality]]) is an equivalence in Coq, but not the identity. In the next version of Coq, all three types above will be identical.

One might expect to also call the dependent sum type

\begin{verbatim}exists x : X, P x\end{verbatim}
(see [[existential quantifier]]) but in the current [[Coq]] implementation that keyword is reserved for the corresponding operation on Coq's built-in universe {\colorbox[rgb]{1.00,0.93,1.00}{\tt Prop}}, which is not used by homotopy type theory. In particular, it should not be confused with what HoTT calls [[proposition]]s, which are the [[(-1)-truncated]] types. In fact, arguably in HoTT {\colorbox[rgb]{1.00,0.93,1.00}{\tt exists}} should refer not to the dependent sum itself, but to the (-1)-truncation thereof (its [[bracket type]]).

The type

\begin{verbatim}forall x : X, P x\end{verbatim}
denotes the object of [[homotopy]] [[section]]s of this bundle $P\to X$ --- that is, the \emph{[[dependent product]]} of the bundle. (See the section \emph{\href{http://ncatlab.org/nlab/show/dependent+product#RelationToSpacesOfSections}{relation to spaces of sections}} there). It also denotes the [[universal quantifier]] when acting on (-1)-truncated objects [[propositions]]. A term of this type :

\begin{verbatim}f : forall x : X, P x\end{verbatim}
denotes therefore a particular [[section]] of this bundle

\begin{displaymath}
\itexarray{
     && P
     \\  
     & {}^{\mathllap{f}}\nearrow& \downarrow
     \\ 
     X &= & X
  }
  \,.
\end{displaymath}
Given a type $X$, its [[identity type]], denoted

\begin{verbatim}paths X : X -> X -> Type
Id X : X -> X -> Type\end{verbatim}
corresponds to the [[diagonal morphism]] $X\to X\times X$ in $C$, regarded as a bundle over $X\times X$. In a [[presentable (infinity,1)-category|presentation]] of $C$ by a [[category of fibrant objects]], this means the [[path space object]] $X^I$, since dependent types must always be fibrations.

The fact that there is a [[weak equivalence]] $X \stackrel{\simeq}{\to} X^I$ given by the inclusion of [[identity]] [[morphisms]] is reflected in the [[inductive type]]-definition of , which says that any proposition about terms in the path type is already determined by its value on all identity paths.

Then for  two [[terms]] regarded as morphisms $1\to X$, the application of the identity type $x$ and $y$ (also called the [[identity type]]) denoted variously

\begin{verbatim}paths X x y : Type
x ~~> y : Type
x == y : Type\end{verbatim}
(the latter two make use of Coq's ability to define new notations), denotes the [[homotopy pullback]] of the form

\begin{displaymath}
\itexarray{
    x \times_X y &\to& {*}
    \\
    \downarrow && \downarrow^{\mathrlap{x}}
    \\
    {*} &\stackrel{y}{\to}&  X
  }
\end{displaymath}
which in a presentation by a [[category of fibrant objects]] is given (see [[factorization lemma]]) by the ordinary pullback

\begin{displaymath}
\itexarray{
    P_{x,y} X &\to& &\to& {*}
    \\
    \downarrow && && \downarrow^{\mathrlap{x}}
    \\
    \downarrow && X^{\Delta[1]} &\to& X
    \\  
    \downarrow && \downarrow
    \\
    {*} &\stackrel{y}{\to}& X
  }
  \,.
\end{displaymath}
Beware that the [[identity type|path induction rule]] applies to  not to . Where for the former a proposition is fixed by what it does on identity paths, for the latter this is not the case anymore.

More generally, we can define arbitrary pullbacks. If {\colorbox[rgb]{1.00,0.93,1.00}{\tt f\char32\char58\char32A\char32\char45\char62\char32C}} and {\colorbox[rgb]{1.00,0.93,1.00}{\tt g\char32\char58\char32B\char32\char45\char62\char32C}}, the [[homotopy pullback]] of {\colorbox[rgb]{1.00,0.93,1.00}{\tt f}} and {\colorbox[rgb]{1.00,0.93,1.00}{\tt g}} is defined by

\begin{verbatim}{a : A & {b : B & f a ~~> g b}}\end{verbatim}
together with the obvious projections to {\colorbox[rgb]{1.00,0.93,1.00}{\tt A}} and {\colorbox[rgb]{1.00,0.93,1.00}{\tt B}} and the homotopy between the composites. (a proof can be found \href{https://github.com/guillaumebrunerie/HoTT/blob/master/Coq/Limits/Pullbacks.v}{here})

Using [[higher inductive types]], we can also define [[homotopy pushouts]]. If {\colorbox[rgb]{1.00,0.93,1.00}{\tt g\char32\char58\char32C\char32\char45\char62\char32A}} and {\colorbox[rgb]{1.00,0.93,1.00}{\tt f\char32\char58\char32C\char32\char45\char62\char32B}}, the [[homotopy pushout]] of {\colorbox[rgb]{1.00,0.93,1.00}{\tt f}} and {\colorbox[rgb]{1.00,0.93,1.00}{\tt g}} is defined by

\begin{verbatim}Inductive hopushout :=
  | inl : A -> hopushout
  | inr : B -> hopushout
  | glue : forall x : C, inl (g x) ~~> inr (f x).\end{verbatim}
together with the map {\colorbox[rgb]{1.00,0.93,1.00}{\tt inl}}, {\colorbox[rgb]{1.00,0.93,1.00}{\tt inr}} and the homotopy {\colorbox[rgb]{1.00,0.93,1.00}{\tt glue}}. (see \href{https://github.com/guillaumebrunerie/HoTT/blob/master/Coq/Limits/Pushout.v}{here} for the proof)

\hypertarget{related_entries}{}\subsection*{{Related entries}}\label{related_entries}

\begin{itemize}%
\item [[homotopy type theory FAQ]]


\item [[intensional type theory]], [[observational type theory]], [[extensional type theory]]


\item [[cubical type theory]]


\item [[type-theoretic model category]], [[fibrant type]]


\item [[synthetic homotopy theory]]


\item [[HoTT methods for homotopy theorists]]


\item [[internal category in homotopy type theory]]


\item [[Homotopy Type System]]


\item [[modal homotopy type theory]]


\item [[geometric homotopy type theory]]


\item [[cohesive homotopy type theory]]


\item [[directed homotopy type theory]]

[[opetopic type theory]]



\end{itemize}
$\backslash$linebreak

[[!include homotopy n-types - table]]

$\backslash$linebreak

[[!include proof assistants and formalization projects -- list]]

\hypertarget{References}{}\subsection*{{References}}\label{References}

A survey page maintained by [[Steve Awodey]] is \emph{\href{http://www.andrew.cmu.edu/user/awodey/htt.html}{Homotopy Type Theory and the Univalent Foundations of Mathematics}}

\hypertarget{Introductions}{}\subsubsection*{{Introductions}}\label{Introductions}

The standard textbook is

\begin{itemize}%
\item [[Univalent Foundations Project]], \emph{[[Homotopy Type Theory -- Univalent Foundations of Mathematics]]} (2013)

\end{itemize}
An introduction for philosophers is

\begin{itemize}%
\item [[Michael Shulman]], \emph{Homotopy Type Theory: A synthetic approach to higher equalities} (\href{http://arxiv.org/abs/1601.05035}{arXiv:1601.05035})

\end{itemize}
and one with an emphasis on [[synthetic geometry]] is

\begin{itemize}%
\item [[Michael Shulman]], \emph{Homotopy type theory: the logic of space}, in [[Gabriel Catren]], [[Mathieu Anel]] (eds.) \emph{[[New Spaces for Mathematics and Physics]]} (\href{https://arxiv.org/abs/1703.03007}{arXiv:1703.03007})

\end{itemize}
Early sketches and introductions to the idea of homotopy type theory include

\begin{itemize}%
\item [[Steve Awodey]], \emph{Homotopy and Type Theory}, grant proposal project description (\href{https://ncatlab.org/homotopytypetheory/files/proposal2009.pdf}{pdf})


\item [[Steve Awodey]], \emph{Type theory and homotopy}, Epistemology versus Ontology. Springer Netherlands, 2012. 183-201. (2010) \href{http://arxiv.org/abs/1010.1810}{arXiv:1010.1810}


\item [[Michael Shulman]], \emph{Homotopy type theory} \href{http://golem.ph.utexas.edu/category/2011/03/homotopy_type_theory_i.html}{I}, \href{http://golem.ph.utexas.edu/category/2011/03/homotopy_type_theory_ii.html}{II}, \href{http://golem.ph.utexas.edu/category/2011/03/homotopy_type_theory_iii.html}{III}, \href{http://golem.ph.utexas.edu/category/2011/04/homotopy_type_theory_iv.html}{IV}, \href{http://golem.ph.utexas.edu/category/2011/04/homotopy_type_theory_v.html}{V}, \href{http://golem.ph.utexas.edu/category/2011/04/homotopy_type_theory_vi.html}{VI}


\item [[Thorsten Altenkirch]], [[Thierry Coquand]], \emph{Towards higher dimensional type theory}, Nottingham (2011) (\href{http://www.cs.nott.ac.uk/~txa/talks/aimxiii.pdf}{pdf})


\item [[Mike Shulman]], \emph{Minicourse on homotopy type theory}, Swansea, April (2012) (\href{http://home.sandiego.edu/~shulman/hottminicourse2012/}{web})


\item [[Vladimir Voevodsky]], \emph{\href{http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations.html}{Univalent foundations}}



\end{itemize}
Motivation via practical problems in [[homotopy theory]] and [[higher category theory]] is given in

\begin{itemize}%
\item [[Vladimir Voevodsky]], \emph{Univalent foundations}, talk IAS, March 2014 (\href{http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations_files/2014_IAS.pdf}{pdf}, \href{https://video.ias.edu/voevodsky14}{video})

\end{itemize}
(specifically highlighting the technical delicacies involved in the [[Simpson conjecture]]).

A list of video-recorded talks by Voevodsky on this topic is \href{http://video.ias.edu/taxonomy/term/42}{here}.

Writeups on the topic include

\begin{itemize}%
\item [[Nicolai Kraus]], \emph{Homotopy type theory -- An overview} (\href{http://www.cs.nott.ac.uk/~ngk/homotopy_type_theory.pdf}{pdf})


\item [[Egbert Rijke]], \emph{Homotopy type theory} (2012) (\href{http://hottheory.files.wordpress.com/2012/08/hott2.pdf}{pdf})


\item \'A{}lvaro Pelayo, [[Michael Warren]], \emph{Homotopy type theory and Voevodsky's univalent foundations} (\href{http://arxiv.org/abs/1210.5658}{arXiv:1210.5658})


\item Daniel Grayson, \emph{An introduction to univalent foundations for mathematicians}, 2017, \href{https://arxiv.org/abs/1711.01477}{arXiv:1711.01477}.


\item [[Egbert Rijke]], \emph{Introduction to Homotopy Type Theory} (2019) (\href{http://www.andrew.cmu.edu/user/erijke/hott/}{web}, \href{http://www.andrew.cmu.edu/user/erijke/hott/hott_intro.pdf}{pdf}, \href{https://github.com/EgbertRijke/HoTT-Intro}{GitHub})


\item [[Egbert Rijke]], \emph{Classifying Types} (\href{https://arxiv.org/abs/1906.09435}{arXiv:1906.09435})



\end{itemize}
An introduction to the notion of [[equivalence]] in HoTT is in

\begin{itemize}%
\item [[Andrej Bauer]], \emph{A seminar on HoTT equivalences} (\href{http://homotopytypetheory.org/2011/12/07/a-seminar-on-hott-equivalences/}{blog post})

\end{itemize}
A guided walk through the basics of HoTT and then the formal proof in [[Coq]] that the [[univalence axiom]] implies [[functional extensionality]] is at

\begin{itemize}%
\item [[Andrej Bauer]], [[Peter LeFanu Lumsdaine]], \emph{[[Oberwolfach HoTT-Coq tutorial]]}

\end{itemize}
Gentle invitation to some basics:

\begin{itemize}%
\item [[Andrej Bauer]], \emph{What is an explicit bijection?}, talk at \href{http://fpsac2019.fmf.uni-lj.si/}{FPSAC 2019} (\href{http://videolectures.net/site/normal_dl/tag=1244258/FPSAC2019_bauer_explicit_bijection_01.pdf}{slides pdf}, \href{http://videolectures.net/FPSAC2019_bauer_explicit_bijection/}{video recording})

\end{itemize}
\hypertarget{general}{}\subsubsection*{{General}}\label{general}

A blog serving as a base for the HoTT community is at

\begin{itemize}%
\item \emph{Homotopy Type Theory} \href{http://homotopytypetheory.org/}{website}

\end{itemize}
A wiki is here

\begin{itemize}%
\item \emph{\href{https://ncatlab.org/homotopytypetheory/show/HomePage}{HoTT wiki}}

\end{itemize}
Reports from the original Oberwolfach workshop on homotopy type theory are in

\begin{itemize}%
\item \emph{Homotopy type theory} , Oberwolfach Reports 11-2011, (\href{http://hottheory.files.wordpress.com/2011/06/report-11_2011.pdf}{pdf}).

\end{itemize}
Material concerning the

\begin{itemize}%
\item \emph{\href{http://www.math.ias.edu/sp/univalent}{Univalent foundations program 2012/2013}}, Institute of Advanced Study, Princeton

\end{itemize}
is in the wiki

\begin{itemize}%
\item \emph{\href{http://uf-ias-2012.wikispaces.com/}{UF-IAS-2012}} .

\end{itemize}
A FAQ of sorts, with tips for those getting started in the field, is being maintained at

\begin{itemize}%
\item \emph{\href{https://abooij.github.io/wiwikwlhott/}{What I wish I knew when learning HoTT}}.

\end{itemize}
\hypertarget{models_and_categorical_semantics}{}\subsubsection*{{Models and categorical semantics}}\label{models_and_categorical_semantics}

The first [[model]] for [[intensional type theory|intensional]] [[Martin-Löf type theory]] on [[groupoids]] (instead of [[sets]] = [[0-groupoids]]) was

\begin{itemize}%
\item [[Martin Hofmann]], [[Thomas Streicher]] \emph{The groupoid interpretation of type theory}, in: Giovanni Sambin et al. (ed.) , \emph{Twenty-five years of constructive type theory}, Proceedings of a congress, Venice, Italy, October 19---21, 1995. Oxford: Clarendon Press. Oxf. Logic Guides. 36, 83-111 (1998). (\href{http://www.mathematik.tu-darmstadt.de/~streicher/venedig.ps.gz}{ps})

\end{itemize}
Generalization of this to [[strict ∞-groupoids]] were discussed in

\begin{itemize}%
\item [[Michael Warren]], \emph{The strict $\omega$-groupoid interpretation of type theory} (\href{http://www.math.ias.edu/~mwarren/Papers/makkaifest_preprint.pdf}{pdf})

\end{itemize}
The fact that every [[simplicial model category]] in which the cofibrations are [[monomorphisms]] provides a sound [[model]] for [[intensional type theory|intensional]] [[Martin-Löf type theory]] is discussed in

\begin{itemize}%
\item [[Steve Awodey]], [[Michael Warren]], \emph{Homotopy theoretic models of identity type}, Mathematical Proceedings of the Cambridge Philosophical Society vol 146, no. 1 (2009) (\href{http://arxiv.org/abs/0709.0248}{arXiv:0709.0248})

\end{itemize}
and with more details in

\begin{itemize}%
\item [[Michael Warren]], \emph{Homotopy theoretic aspects of constructive type theory}, PhD thesis (2008) (\href{http://www.andrew.cmu.edu/user/awodey/students/warren.pdf}{pdf})


\item [[Richard Garner]], [[Benno van den Berg]], \emph{Topological and simplicial models of identity types}. , ACM Transactions on Computational Logic (\href{http://www.mathematik.tu-darmstadt.de/~berg/papers/main.pdf}{pdf})


\item section 2 of (\hyperlink{Shulman12}{Shulman 12})



\end{itemize}
with lecture notes in

\begin{itemize}%
\item [[Mike Shulman]], \emph{Categorical models of homotopy type theory}, April 13, 2012 (\href{https://home.sandiego.edu/~shulman/hottminicourse2012/03models.pdf}{pdf})


\item [[André Joyal]], \emph{Categorical homotopy type theory}, March 17, 2014 (\href{http://ncatlab.org/homotopytypetheory/files/Joyal.pdf}{pdf})



\end{itemize}
The full model in the [[classical model structure on simplicial sets]] is due to

\begin{itemize}%
\item [[Chris Kapulkin]], [[Peter LeFanu Lumsdaine]], \emph{The Simplicial Model of Univalent Foundations (after Voevodsky)} (\href{https://arxiv.org/abs/1211.2851}{arXiv:1211.2851})

\end{itemize}
The trickiest question in finding models of homotopy type theory is to validate the [[univalence axiom]]. The first model satisfying this axiom was constructed by Voevodsky using the standard [[model structure on simplicial sets]], hence for the archetypical [[(∞,1)-topos]] [[∞Grpd]] of [[discrete ∞-groupoids]]. Some expositions are:

\begin{itemize}%
\item [[Chris Kapulkin]], [[Peter LeFanu Lumsdaine]], [[Vladimir Voevodsky]], \emph{Univalence in simplicial sets}, \href{http://arxiv.org/abs/1203.2553}{arXiv}


\item [[T. Streicher - a model of type theory in simplicial sets - a brief introduction to Voevodsky' s homotopy type theory]]


\item [[Ieke Moerdijk]] (notes by [[Chris Kapulkin]]): \emph{Fiber bundles and univalence}, \href{http://www.pitt.edu/~krk56/fiber_bundles_univalence.pdf}{link}



\end{itemize}
A discussion of univalence for [[categories of presheaves]] over an [[inverse category]], with values in a category for which univalence is already established (such as simplicial sets) is discussed in

\begin{itemize}%
\item [[Michael Shulman]], \emph{The univalence axiom for inverse diagrams} (\href{http://arxiv.org/abs/1203.3253}{arXiv:1203.3253}).

\end{itemize}
Proof that all [[∞-stack]] [[(∞,1)-topos]] have [[presentable (∞,1)-category|presentations]] by [[model categories]] which interpret (provide [[categorical semantics]]) for [[homotopy type theory]] with [[univalence|univalent]] [[type universes]]:

\begin{itemize}%
\item [[Michael Shulman]], \emph{All $(\infty,1)$-toposes have strict univalent universes} (\href{https://arxiv.org/abs/1904.07004}{arXiv:1904.07004}).

\end{itemize}
Discussion of univalence in various other [[model category]] presentations for [[∞Grpd]] ([[cubical sets]], [[cellular sets]]) is in

\begin{itemize}%
\item [[Denis-Charles Cisinski]], \emph{Univalent universes for elegant models of homotopy types} (\href{http://arxiv.org/abs/1406.0058}{arXiv:1406.0058})

\end{itemize}
Models in terms of [[cubical sets]] inside [[constructive set theory]]/[[type theory]] are discussed in

\begin{itemize}%
\item Marc Bezem, [[Thierry Coquand]], Simon Huber, \emph{A model of type theory in cubical sets}, 2013 (\href{http://drops.dagstuhl.de/opus/volltexte/2014/4628/}{web}, \href{http://drops.dagstuhl.de/opus/volltexte/2014/4628/pdf/7.pdf}{pdf})


\item Ambrus Kaposi, [[Thorsten Altenkirch]], \emph{A syntax for cubical type theory} (\href{http://mazzo.li/dump/aim-kaposi-pres.pdf}{pdf})



\end{itemize}
A weaker version of the [[Awodey conjecture]], that the models of HoTT with function extensionality are [[locally cartesian closed (∞,1)-categories]] is explicitly stated in

\begin{itemize}%
\item [[André Joyal]], \emph{Remarks on homotopical logic} Oberwolfach (2011) (\href{http://hottheory.files.wordpress.com/2011/06/report-11_2011.pdf#page=19}{pdf})

\end{itemize}
See also the references at \emph{[[relation between type theory and category theory]]}.

\hypertarget{syntax}{}\subsubsection*{{Syntax}}\label{syntax}

\begin{itemize}%
\item [[Nicola Gambino]], [[Richard Garner]], \emph{The identity type weak factorisation system} , Theoretical Computer Science 409 (2008), no. 3, pages 94--109.


\item [[Richard Garner]], [[Benno van den Berg]], \emph{Types are weak $\omega$-groupoids} ,


\item [[Peter LeFanu Lumsdaine]], \emph{Weak $\omega$-Categories from Intensional Type Theory} , TLCA 2009, Bras\'i{}lia, Logical Methods in Computer Science, Vol. 6, issue 23, paper 24.


\item [[Peter LeFanu Lumsdaine]], \emph{Higher Categories from Type Theories} , PhD Thesis: Carnegie Mellon University, 2010. PDF


\item Michael Hedberg, \emph{A coherence theorem for Martin-L\"o{}f's type theory} , Journal of Functional Programming 8 (4): 413--436, July 1998.



\end{itemize}
\hypertarget{Code}{}\subsubsection*{{Code}}\label{Code}

The basic [[Coq]]-code libraries that set up [[identity types]] and the resulting homotopy type theory are at

\begin{itemize}%
\item [[Vladimir Voevodsky]], \emph{Experimental library of univalent formalization of mathematics} (\href{http://arxiv.org/abs/1401.0053}{arXiv:1401.0053}) \href{https://github.com/UniMath/}{github}


\item \emph{The HoTT Library: A formalization of homotopy type theory in Coq}, Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Mike Shulman, Matthieu Sozeau, Bas Spitters, 2016 \href{https://arxiv.org/abs/1610.04591}{arxiv} and on \href{https://github.com/HoTT/HoTT/wiki}{github}



\end{itemize}
A slightly more human readable version is collected as a single pdf in

\begin{itemize}%
\item \emph{HoTT-Coq code} ([[HoTT-Coq-code.pdf:file]])


\item Voevodsky, Vladimir and Ahrens, Benedikt and Grayson, Daniel and others, [[unimath|UniMath]], \href{https://github.com/UniMath}{GitHub} link.



\end{itemize}
[[!redirects homotopy type theory]] [[!redirects (∞,1)-type theory]] [[!redirects (infinity,1)-type theory]] [[!redirects univalent foundations]] [[!redirects Homotopy type theory]] [[!redirects HoTT]] [[!redirects internal language of an (∞,1)-topos]]



\end{document}