\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 FAQ}

\begin{quote}%
under construction


\end{quote}
\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]]

This page is to provide non-technical or maybe semi-technical discussion of the nature and role of the [[foundation of mathematics|foundational system]] for [[mathematics]] known as \emph{homotopy type theory}. For more technical details and further pointers see at [[homotopy type theory]].

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

\noindent\hyperlink{faq}{FAQ}\dotfill \pageref*{faq} \linebreak
\noindent\hyperlink{what_is_homotopy_type_theory}{What is homotopy type theory?}\dotfill \pageref*{what_is_homotopy_type_theory} \linebreak
\noindent\hyperlink{for_laymen}{For laymen}\dotfill \pageref*{for_laymen} \linebreak
\noindent\hyperlink{WhatIsHoTTForSetTheorists}{For set theorists}\dotfill \pageref*{WhatIsHoTTForSetTheorists} \linebreak
\noindent\hyperlink{for_type_theorists}{For type theorists}\dotfill \pageref*{for_type_theorists} \linebreak
\noindent\hyperlink{for_homotopy_theorists}{For homotopy theorists}\dotfill \pageref*{for_homotopy_theorists} \linebreak
\noindent\hyperlink{WhyShouldICare}{Why should I care?}\dotfill \pageref*{WhyShouldICare} \linebreak
\noindent\hyperlink{for_laymen_2}{For laymen}\dotfill \pageref*{for_laymen_2} \linebreak
\noindent\hyperlink{WhyShouldICareForSetTheorists}{For set theorists}\dotfill \pageref*{WhyShouldICareForSetTheorists} \linebreak
\noindent\hyperlink{for_type_theorists_2}{For type theorists}\dotfill \pageref*{for_type_theorists_2} \linebreak
\noindent\hyperlink{WhyShouldICareForHomotopyTheorists}{For homotopy theorists}\dotfill \pageref*{WhyShouldICareForHomotopyTheorists} \linebreak
\noindent\hyperlink{WhatRoleDoesTheUnivalenceAxiomPlay}{What role does the univalence axiom play?}\dotfill \pageref*{WhatRoleDoesTheUnivalenceAxiomPlay} \linebreak
\noindent\hyperlink{for_laymen_3}{For laymen}\dotfill \pageref*{for_laymen_3} \linebreak
\noindent\hyperlink{for_set_theorists_3}{For set theorists}\dotfill \pageref*{for_set_theorists_3} \linebreak
\noindent\hyperlink{for_type_theorists_3}{For type theorists}\dotfill \pageref*{for_type_theorists_3} \linebreak
\noindent\hyperlink{for_homotopy_theorists_3}{For homotopy theorists}\dotfill \pageref*{for_homotopy_theorists_3} \linebreak
\noindent\hyperlink{what_advantages_does_homotopy_type_theory_have_over_set_theory}{What advantages does homotopy type theory have over set theory?}\dotfill \pageref*{what_advantages_does_homotopy_type_theory_have_over_set_theory} \linebreak
\noindent\hyperlink{IsHoTTLimitedToConstructiveMathematics}{Is homotopy type theory limited to constructive mathematics?}\dotfill \pageref*{IsHoTTLimitedToConstructiveMathematics} \linebreak
\noindent\hyperlink{InterpretationInInfinityToposes}{Does HoTT have interpretation/semantics/models in $\infty$-toposes?}\dotfill \pageref*{InterpretationInInfinityToposes} \linebreak
\noindent\hyperlink{what_is_meant_by_a_computational_interpretation_of_univalence}{What is meant by a ``computational interpretation of univalence''?}\dotfill \pageref*{what_is_meant_by_a_computational_interpretation_of_univalence} \linebreak
\noindent\hyperlink{what_are_higher_inductive_types}{What are higher inductive types?}\dotfill \pageref*{what_are_higher_inductive_types} \linebreak
\noindent\hyperlink{what_do_we_gain_by_a_proof_in_homotopy_type_theory_of__over_ordinary_proofs}{What do we gain by a proof in homotopy type theory of $\pi_1(S^1) = \mathbb{Z}$ over ordinary proofs?}\dotfill \pageref*{what_do_we_gain_by_a_proof_in_homotopy_type_theory_of__over_ordinary_proofs} \linebreak
\noindent\hyperlink{is_it_possible_to_define_higher_coinductive_types}{Is it possible to define higher coinductive types?}\dotfill \pageref*{is_it_possible_to_define_higher_coinductive_types} \linebreak
\noindent\hyperlink{in_what_sense_does_homotopy_type_theory_already_contain_logic}{In what sense does homotopy type theory already contain logic?}\dotfill \pageref*{in_what_sense_does_homotopy_type_theory_already_contain_logic} \linebreak
\noindent\hyperlink{can_category_theory_be_carried_out_in_homotopy_type_theory}{Can category theory be carried out in homotopy type theory?}\dotfill \pageref*{can_category_theory_be_carried_out_in_homotopy_type_theory} \linebreak
\noindent\hyperlink{can_categories_be_defined_in_homotopy_type_theory}{Can $(\infty,1)$-categories be defined in homotopy type theory?}\dotfill \pageref*{can_categories_be_defined_in_homotopy_type_theory} \linebreak


\hypertarget{faq}{}\subsection*{{FAQ}}\label{faq}

\hypertarget{what_is_homotopy_type_theory}{}\subsubsection*{{What is homotopy type theory?}}\label{what_is_homotopy_type_theory}

\hypertarget{for_laymen}{}\paragraph*{{For laymen}}\label{for_laymen}

(\ldots{})

\hypertarget{WhatIsHoTTForSetTheorists}{}\paragraph*{{For set theorists}}\label{WhatIsHoTTForSetTheorists}

Homotopy type theory is a refinement of [[constructive set theory]] that takes fully seriously the constructive nature also of [[identity types|identity]]. (As with all [[constructive mathematics]], with the relevant [[axioms]] added, this subsumes, rather than excludes, classical mathematics, see below at \emph{\hyperlink{IsHoTTLimitedToConstructiveMathematics}{Is HoTT limited to constructive mathematics?}}.)

It is this insistence on constructive witnesses for identity and on witnesses for identity of such witnesses, and so ever on, that makes what in traditional [[set theory]] are just [[sets]] (whose elements are either equal or not) in homotopy type theory instead be [[groupoids]] (whose elements may have non-trivial [[isomorphism]] between them) and indeed [[2-groupoids]] (with isomorphisms between these isomorphisms) and so ever on; hence what makes what used to be just [[sets]] be what is kown as \emph{[[∞-groupoids]]} or \emph{[[homotopy types]]}.

More technically, restriction to the [[0-truncated types]] in HoTT (the ``[[h-set]]s'') gives a [[predicative topos]] ``of sets'', and a [[topos]] if one allows the [[resizing axiom]] (details are \href{http://ncatlab.org/nlab/show/set%20theory#ReferencesInHomotopyTypeTheory}{here}). When adding the [[axiom of choice]] to HoTT, one obtains a model of [[ETCS]]. The iterative notion of set can also be captured. Aczel's sets-as-trees interpretation gives a model of constructive set theory [[CZF]]. Again by adding choice to HoTT, one obtains a model of [[ZFC]]; see Ch10 of the HoTT book.

Conversely HoTT has [[models]] in [[ZFC]] (+a number of [[Grothendieck universes]] to model the type theoretic universes), namely in structures called \emph{[[(∞,1)-toposes]]} which are presented by [[presheaves]] of [[simplicial sets]]. (See also at \emph{\hyperlink{InterpretationInInfinityToposes}{Does HoTT have models in infinity-toposes?}})

The nature and role of these higher toposes in HoTT may be understood by analogy with the familar [[forcing]] [[models]]: When one proves something in [[ZF]], it is automatically also true in all [[forcing]] extensions. The same is true for [[constructive set theory]], except that there are more forcing extensions since we don't have to force the [[law of excluded middle]]; those constructive notions of forcing (which also subsume [[permutation models]]) are called ``[[sites]]'' and their [[models]] are called ``[[topos|1-toposes]]''. Now in HoTT we have an even more general sort of forcing appropriate for [[homotopy theory]], called [[(∞,1)-sites]], whose models are called [[(∞,1)-toposes]].

\hypertarget{for_type_theorists}{}\paragraph*{{For type theorists}}\label{for_type_theorists}

(\ldots{})

\hypertarget{for_homotopy_theorists}{}\paragraph*{{For homotopy theorists}}\label{for_homotopy_theorists}

(\ldots{})

\hypertarget{WhyShouldICare}{}\subsubsection*{{Why should I care?}}\label{WhyShouldICare}

\hypertarget{for_laymen_2}{}\paragraph*{{For laymen}}\label{for_laymen_2}

\hypertarget{WhyShouldICareForSetTheorists}{}\paragraph*{{For set theorists}}\label{WhyShouldICareForSetTheorists}

Traditional [[set theory]] is formulated in [[first-order logic]]. Under the [[propositions as types]] interpretation, first order logic maps soundly and completely into [[type theory]] (\href{type+theory#MartinLoef74}{Martin-L\"o{}f 74, section 3.1}, \href{pure+type+system#Barendregt91}{Barendregt 91, section 4}). But now the [[homotopy 0-types]] in [[homotopy type theory]] already give a [[constructive set theory]], natively, without further axiomatization. See at \emph{[[h-set]]} for more.

\hypertarget{for_type_theorists_2}{}\paragraph*{{For type theorists}}\label{for_type_theorists_2}

\hypertarget{WhyShouldICareForHomotopyTheorists}{}\paragraph*{{For homotopy theorists}}\label{WhyShouldICareForHomotopyTheorists}

Most homotopy-theoretic theorems that are proven in the [[Homotopy Type Theory -- Univalent Foundations of Mathematics|HoTT textbook]] are, in their traditional informal version, material of a first-year course on homotopy theory. Experts who do not care about [[formal proof]] might not be impressed yet.

But the point is that there is significant prospect. By the discussion at \emph{\hyperlink{InterpretationInInfinityToposes}{Does HoTT have models in infinity-toposes}}, it is a fact that homotopy type theory is the [[internal language]] of [[(∞,1)-toposes]], hence of the most powerful modern incarnation of [[homotopy theory]]. Whether or not anyone has already made impressive use of this fact (but see below), this is of genuine interest in homotopy theory irrespective of the issue of formal proof.

Historically, making use of the [[internal logic]]-perspective of [[elementary toposes]] led to substantial insight into all theory that uses [[Grothendieck toposes]], such as notably [[algebraic geometry]]. While [[Jacob Lurie|Lurie]]`s book \emph{[[Higher Topos Theory]]} based on [[Charles Rezk]]'s note \emph{\href{infinity,1-topos#Rezk10}{Homotopy Topos Theory}} is an astounding piece of work, it falls short of saying anything about this crucial internal aspect of (higher) topos theory. Homotopy type theory is precisely what fills this gap. For more on how this works see at \emph{[[HoTT methods for homotopy theorists]]}.

An illustration of the use of this is the proof of the \emph{[[Blakers-Massey theorem]]}. This basic fact of homotopy theory has a classical proof in the classical homotopy category [[∞Grpd]] $\simeq$ $L_{whe}$ [[Top]], a proof that is however rather roundabout. From this follows a proof in all [[(∞,1)-toposes]] with an [[(∞,1)-site]] of definition by, essentially, reducing [[stalk|stalkwise]] to the classical theorem (details are \href{Blakers-Massey%20theorem#Rezk10}{here}). But now the theorem was also proven in homotopy type theory (details are \href{Blakers-Massey%20theorem#LumsdaineFinsterLicata13}{here}). Translating this formal proof back to ordinary language produces first of all a \emph{new} and more elegant proof of Blakers-Massey in [[∞Grpd]] $\simeq$ $L_{whe}$ [[Top]], second a new and elegant proof of the statement for [[(∞,1)-toposes]] with [[(∞,1)-site]] of definition. This is something that some homotopy theorists tried to find by classical means and failed (details are \href{Blakers-Massey%20theorem#Rezk14}{here}). And moreover, the HoTT proof of Blakers-Massey is actually a new result when applied to [[elementary (∞,1)-toposes]], where the classical methods of proving it completely break down.

It seems rather plausible that this is just a simple first example of a future where HoTT methods allow to enter new territory in classical homotopy theory. Of course it will require some expert homotopy theorists to seriously look into the internal-language-of-$\infty$-toposes way of doing homotopy theory. This is now an open problem for homotopy theorists just as it is for type theorists.

\hypertarget{WhatRoleDoesTheUnivalenceAxiomPlay}{}\subsubsection*{{What role does the univalence axiom play?}}\label{WhatRoleDoesTheUnivalenceAxiomPlay}

\hypertarget{for_laymen_3}{}\paragraph*{{For laymen}}\label{for_laymen_3}

The [[axiom]] of [[univalence]] may be thought of as a [[formal logic|formalization]] of what might be called the \emph{[[principle of equivalence]]} of [[mathematics]], which is the basic but important idea that [[mathematical structures]] which are [[equivalence|equivalent]] should behave the same, satisfy the same theorems and so forth.

Obvious as this may seem, this principle may be violated in other [[foundations of mathematics]] such as [[ZFC]]. On the other hand, while these models allow such violation, in practice one essentially never wants to use such violation. The univalence axiom hence serves to make formal mathematical foundation be closer to the actual ``nature of mathematics'', at least to the practice of mathematics.

\hypertarget{for_set_theorists_3}{}\paragraph*{{For set theorists}}\label{for_set_theorists_3}

\hypertarget{for_type_theorists_3}{}\paragraph*{{For type theorists}}\label{for_type_theorists_3}

The axiom of [[univalence]] added to [[Martin-Löf type theory]] implies all of the following:

\begin{enumerate}%
\item [[functional extensionality]]


\item [[quotient types]]


\item [[higher inductive types]] with nontrivial homotopies,

Which in turn imply a wealth of further structure such as (but not limited to)

\begin{enumerate}%
\item [[bracket types]]


\item etc.



\end{enumerate}


\end{enumerate}
\hypertarget{for_homotopy_theorists_3}{}\paragraph*{{For homotopy theorists}}\label{for_homotopy_theorists_3}

In view of the answer at \emph{\hyperlink{InterpretationInInfinityToposes}{Does HoTT have interpretation in infinity-toposes?}} the [[axiom]] of [[univalence]] axiomatizes the presence of an [[object classifier]] in an [[(∞,1)-topos]] $\mathbf{H}$ (details are \href{univalence+axiom#GepnerKock12}{here}).

In the default choice $\mathbf{H} =$[[∞Grpd]] $\simeq$ $L_{whe}$[[Top]] of traditonal [[homotopy theory]] this is the [[universal principal ∞-bundle|universal fibration]] over the disjoint union of [[classifying spaces]] $\coprod_{[F]} B Aut(F)$ of the [[automorphism ∞-groups]] of all (small) [[homotopy types]] $[F]$.

Therefore from the axiom of [[univalence]] follows for instance the theory of [[∞-actions]], [[associated ∞-bundles]] and of [[twisted cohomology]] (details are [[schreiber:Principal ∞-bundles -- theory, presentations and applications|here]]).

\hypertarget{what_advantages_does_homotopy_type_theory_have_over_set_theory}{}\subsubsection*{{What advantages does homotopy type theory have over set theory?}}\label{what_advantages_does_homotopy_type_theory_have_over_set_theory}

As explained at \emph{\hyperlink{WhatIsHoTTForSetTheorists}{What is HoTT for set theorists?}}, HoTT subsumes [[set theory]]. It has all the advantages that [[structural set theory]] ([[Algebraic set theory]], [[ETCS]]) has over [[material set theory]] ([[ZFC]]), but moreover it allows us to natively capture [[higher category theory|higher categorical]] (more precisely, [[infinity-groupoid|higher groupoidal]]) and [[homotopy theory|homotopical]] reasoning. Moreover, as a practical foundation, set theory may be compared to the Turing machine model, or perhaps more generously, say, \href{http://en.wikipedia.org/wiki/ALGOL}{ALGOL}. Whereas, homotopy type theory is closely related to modern programming languages like Haskell and ML, or more accurately [[Coq]] and [[Agda]].

\hypertarget{IsHoTTLimitedToConstructiveMathematics}{}\subsubsection*{{Is homotopy type theory limited to constructive mathematics?}}\label{IsHoTTLimitedToConstructiveMathematics}

No. On the [[0-types]] (the [[h-sets]]) the axioms of [[classical logic]] may be imposed, such as the [[law of excluded middle]] (details are \href{excluded+middle#ReferencesInHomotopyTypeTheory}{here}) and the [[axiom of choice]] (details are \href{axiom+of+choice#ReferencesInHomotopy}{here}).

One [[model]] that interprets the resulting axioms is the standard model in [[simplicial sets]] (\href{model%20structure%20on%20simplicial%20sets#KapulkinLumnsdaineVoevodsky12}{here}) inside [[ZFC]]+[[inaccessible cardinals]]. The [[0-types]] in this model are precisely the ordinary sets in ZFC. See also the discussion at \emph{\hyperlink{WhatIsHoTTForSetTheorists}{What is HoTT? For set theorists}}.

For more exposition see also

\begin{itemize}%
\item [[Andrej Bauer]], \emph{\href{http://math.andrej.com/2014/01/13/univalent-foundations-subsume-classical-mathematics/}{Univalent foundations subsume classical mathematics}} (2013)

\end{itemize}
\hypertarget{InterpretationInInfinityToposes}{}\subsubsection*{{Does HoTT have interpretation/semantics/models in $\infty$-toposes?}}\label{InterpretationInInfinityToposes}

The short answer is: Yes. Homotopy type theory has [[higher category theory|higher]] [[categorical semantics]] in every [[(∞,1)-topos]], in refinement of how plain [[dependent type theory]] has [[categorical semantics]] in [[toposes]].

The more detailed answer depends on which axiomatics precisely one subsumes under ``homotopy type theory''. A hierarchy of three main variants (``fragments'') of homotopy type theory should be distinguished here:

\begin{enumerate}%
\item HoTT without [[univalence|univalent]] [[type universes]];


\item HoTT with [[univalence|univalent]] weak [[type universes]] \href{type%20of%20types#TarskiStyle}{\`a{} la Tarski};


\item HoTT with [[univalence|univalent]] strict [[type universes]] \href{type%20of%20types#RussellStyle}{\`a{} la Russell} or \href{type%20of%20types#TarskiStyle}{\`a{} la Tarski};



\end{enumerate}
In all three cases the $\infty$-categorical semantics is induced by ordinary [[categorical semantics]] in a [[type-theoretic model category]] which in turn [[locally presentable (infinity,1)-category|presents]] an [[(∞,1)-category]]. The way this works is reviewed also at \emph{[[HoTT methods for homotopy theorists]]}. This relies on standard techniques for interpreting any [[dependent type theory]] in a [[locally cartesian closed category]] (see \href{relation+between+type+theory+and+category+theory#DependentTypeTheory}{here} for details).

With that understood, the higher categorical semantics for the above three cases is as follows:

\begin{enumerate}%
\item HoTT without univalent universes has semantics in every [[locally presentable (∞,1)-category|locally presentable]] [[locally cartesian closed (∞,1)-category]] (details are \href{locally+cartesian+closed+%28infinity,1%29-category#InternalLogic}{here}).


\item HoTT with strict univalent universes has semantics at least in [[(∞,1)-category of (∞,1)-presheaves|(∞,1)-presheaf]] [[(∞,1)-toposes]] over [[elegant Reedy categories]]. This includes in particular the standard [[base (∞,1)-topos]] [[∞Grpd]] as well as for instance the [[Sierpinski (∞,1)-topos]] (details are \href{relation+between+type+theory+and+category+theory#Shulman13}{here}).


\item HoTT with weak univalent universes has semantics in every [[(∞,1)-sheaf (∞,1)-topos]] (details are [[homotopytypetheory:model of type theory in an (infinity,1)-topos|here]]).



\end{enumerate}
Since we are assuming [[locally presentable (∞,1)-category|local presentability]] here, all these models have enough [[(∞,1)-colimits]] to interpret [[higher inductive types]]. (One might also ask for models of HoTT without univalence and without higher inductive types and would expect that this then also includes [[locally cartesian closed (∞,1)-categories]] which are not necessarily locally presentable.)

One may also ask about models in [[elementary (∞,1)-toposes]]. Their theory or even definition is however much in the making. On the other hand, existing proposals essentially turn the question around and define [[elementary (∞,1)-toposes]] as [[(∞,1)-categories]] with the minimum of properties such that HoTT may be modeled in them. This reflects the idea that what is ``elementary'' about elementary $(\infty,1)$-toposes is precisely the fact that there is an internal type theory language for them.

In conclusion, every [[proposition]] [[proof|proven]] in homtopy type theory yields (subject to the above qualification) a statement that holds true in every [[(∞,1)-topos]] (in every presentable [[locally cartesian closed (∞,1)-category]]), i.e. homotopy type theory is the [[internal language]] of $\infty$-toposes.

If one wishes to prove statements that hold only in some class of $\infty$-toposes, then one needs to add further [[axioms]] to HoTT that characterize these classes. For instance adding [[higher modalities]] that define [[cohesive homotopy type theory]] make it a language that proves theorems which hold in all [[cohesive (∞,1)-toposes]].

\hypertarget{what_is_meant_by_a_computational_interpretation_of_univalence}{}\subsubsection*{{What is meant by a ``computational interpretation of univalence''?}}\label{what_is_meant_by_a_computational_interpretation_of_univalence}

\hypertarget{what_are_higher_inductive_types}{}\subsubsection*{{What are higher inductive types?}}\label{what_are_higher_inductive_types}

\hypertarget{what_do_we_gain_by_a_proof_in_homotopy_type_theory_of__over_ordinary_proofs}{}\subsubsection*{{What do we gain by a proof in homotopy type theory of $\pi_1(S^1) = \mathbb{Z}$ over ordinary proofs?}}\label{what_do_we_gain_by_a_proof_in_homotopy_type_theory_of__over_ordinary_proofs}

\hypertarget{is_it_possible_to_define_higher_coinductive_types}{}\subsubsection*{{Is it possible to define higher coinductive types?}}\label{is_it_possible_to_define_higher_coinductive_types}

\hypertarget{in_what_sense_does_homotopy_type_theory_already_contain_logic}{}\subsubsection*{{In what sense does homotopy type theory already contain logic?}}\label{in_what_sense_does_homotopy_type_theory_already_contain_logic}

\hypertarget{can_category_theory_be_carried_out_in_homotopy_type_theory}{}\subsubsection*{{Can category theory be carried out in homotopy type theory?}}\label{can_category_theory_be_carried_out_in_homotopy_type_theory}

\hypertarget{can_categories_be_defined_in_homotopy_type_theory}{}\subsubsection*{{Can $(\infty,1)$-categories be defined in homotopy type theory?}}\label{can_categories_be_defined_in_homotopy_type_theory}

[[!redirects HoTT FAQ]]



\end{document}