\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*{HoTT methods for homotopy theorists}

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

\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{type_theory}{}\paragraph*{{Type theory}}\label{type_theory}

[[!include type theory - contents]]

This page on aspects of [[homotopy type theory]] is meant for readers who are interested in [[homotopy theory]] but not (necessarily) in [[formal logic]] and [[formal proof]]. This page is meant to help answer the question:

\begin{quote}%
I am a homotopy theorist; what can homotopy type theory do for me?


\end{quote}
See also at \emph{[[homotopy type theory FAQ]]} the section \emph{\href{homotopy+type+theory+FAQ#WhyShouldICareForHomotopyTheorists}{Why should I care? -- For homotopy theorists}}.

Since homotopy theory takes place in [[model categories]] and similar categorical structures, the input from homotopy type theory is via its [[categorical semantics]]. In this sense the question which this page is meant to help to answer is

\begin{quote}%
I am a homotopy theorist; which methods can I learn from the [[categorical semantics of homotopy type theory]]?


\end{quote}
For the moment this page will mostly list pointers with brief comments to other entries where details are given. You should maybe read it like an instructional exercise list and follow the pointers for help.

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

\noindent\hyperlink{BasicDictionary}{Basic dictionary for the internal language}\dotfill \pageref*{BasicDictionary} \linebreak
\noindent\hyperlink{homotopy_pullbacks}{Homotopy pullbacks}\dotfill \pageref*{homotopy_pullbacks} \linebreak
\noindent\hyperlink{detecting_truncation}{Detecting $n$-truncation}\dotfill \pageref*{detecting_truncation} \linebreak
\noindent\hyperlink{Induction}{Homotopy algebras over homotopy monads}\dotfill \pageref*{Induction} \linebreak
\noindent\hyperlink{detecting_connectedness}{Detecting $n$-connectedness}\dotfill \pageref*{detecting_connectedness} \linebreak
\noindent\hyperlink{homotopy_pushouts}{Homotopy pushouts}\dotfill \pageref*{homotopy_pushouts} \linebreak
\noindent\hyperlink{constructing_truncation}{Constructing $n$-truncation}\dotfill \pageref*{constructing_truncation} \linebreak
\noindent\hyperlink{specific_hott_proofs_in_homotopy_theory}{Specific HoTT proofs in homotopy theory}\dotfill \pageref*{specific_hott_proofs_in_homotopy_theory} \linebreak
\noindent\hyperlink{blakersmassey_theorem}{Blakers-Massey theorem}\dotfill \pageref*{blakersmassey_theorem} \linebreak
\noindent\hyperlink{essential_uniqueness_of_group_units}{Essential uniqueness of group units}\dotfill \pageref*{essential_uniqueness_of_group_units} \linebreak
\noindent\hyperlink{equivalence_of_notions_of_stabilizer_groups}{Equivalence of notions of stabilizer $\infty$-groups}\dotfill \pageref*{equivalence_of_notions_of_stabilizer_groups} \linebreak


\hypertarget{BasicDictionary}{}\subsection*{{Basic dictionary for the internal language}}\label{BasicDictionary}

Starting from ([[(infinity,1)-category theory|homotopy]]) [[category theory]], the corresponding ([[homotopy type theory|homotopy]]) [[type theory]] is simply a formal language for denoting familiar constructions, as indicated in the following table.

\newline | [[semantics]] | [[syntax]] | | [[object]] $X$ | [[type]] $x : X$ | | [[fibration]]([[display map]]) $\itexarray{A \\ \downarrow^{\mathrlap{p}} \\ X}$ | [[dependent type]] $x : X \vdash A(x) : Type$ | | [[section]] $\itexarray{ X &&\stackrel{t}{\to}&& A \\ & {}_{\mathllap{id}}\searrow && \swarrow_{p} \\ && X}$ | [[term]] $x : X \vdash t(x) : A(x)$ | | [[pullback]] $\itexarray{ f^* A &\to& A \\ \downarrow && \downarrow^{\mathrlap{p}} \\ Y &\stackrel{f}{\to} & X }$ | [[substitution]] $y : Y \vdash A(f(y)) : Type$ | | [[direct image]] $\itexarray{ A && f_* A \\ {}^{\mathllap{p}}\downarrow && \downarrow ^{f_* p}\\ X &\stackrel{f}{\to}& Y}$ | [[dependent product]] $y : Y \vdash \underset{x : X(y)}{\prod } A(x) : Type$ | | \href{locally%20cartesian%20closed%20category#EquivalentCharacterizations}{internal hom in slice} $\itexarray{ X \times f^* A && f_* f^* A & = [X,A]_Y \\ {}^{\mathllap{}}\downarrow && \downarrow \\ X &\stackrel{f}{\to}& Y}$ | [[function type]] $y : Y \vdash X(y) \to A(y) : Type$ | | postcomposition $\itexarray{ A &=& f_! A \\ \downarrow && \downarrow \\ X &\stackrel{f}{\to}& Y}$ | [[dependent sum]] $y : Y \vdash \underset{x : X(y)}{\sum} A(x) : Type$ | | [[fiber product|fiber]][[product]] $\itexarray{ X \times f^* A &=& f_! f^* A & = X \times_Y A\\ \downarrow && \downarrow \\ X &\stackrel{f}{\to}& Y}$ | [[product type]] $y : Y \vdash X(y) \times A(y) : Type$ | | [[Beck-Chevalley condition]] of [[codomain fibration]] | [[substitution]] commutes with [[dependent sum]] | | [[path space object]] $\itexarray{A^I \\ \downarrow^{\mathrlap{(d_1,d_0)}} \\ A \times A}$ | [[identity type]] $a,b : A \vdash (a = b)$ | | [[truncated object in an (infinity,1)-category|(-2)-truncated morphism]]/[[equivalence in an (infinity,1)-category|equivalence]] $\itexarray{Y \\ \downarrow^{\mathrlap{\simeq}} \\ X}$ | [[true]]/[[unit type]] $x : X \vdash 1 : Type$ | | [[truncated object in an (infinity,1)-category|(-1)-truncated morphism]]/[[monomorphism in an (infinity,1)-category|monomorphism]] $\itexarray{\phi \\ \downarrow \\ X}$ | [[proposition]] $x : X \vdash \phi(x) : Type$ | | [[direct image]] of [[truncated object in an (infinity,1)-category|(-1)-truncated morphism]] | [[universal quantifier]] $y : Y \vdash \underset{x \in X(y)}{\forall} \phi(x) : Type$ | | [[truncated object of an (infinity,1)-category|(-1)-truncation]] of postcomposition of [[truncated object in an (infinity,1)-category|(-1)-truncated morphism]] | [[existential quantifier]] $y : Y \vdash \underset{x \in X(y)}{\exists} \phi(x) : Type$ |

The symbols in the right column may be formally manipulated according to the rules of \emph{[[type theory]]}. For the case of ordinary categories, this table defines a [[functor]]

\begin{displaymath}
Lang : LocallyCartesianClosedCategories \to DependentTypeTheories
\end{displaymath}
from \emph{[[locally cartesian closed categories]]} to \emph{[[dependent type theories]]} that sends each category to its \emph{[[internal language]]}.

The important fact is that

\begin{theorem}
\label{}\hypertarget{}{}
The functor $Lang$ is an [[equivalence of categories]].

\end{theorem}
This is discussed at \emph{[[relation between type theory and category theory]]}. So the (dependent) type theory is just an equivalent way of talking about a (locally cartesian closed category).

For the case of [[(∞,1)-categories]]/[[homotopy theories]] that we are interested in here, there remain some things to be fully worked out, but it is clear that we get an analogous construction

\begin{displaymath}
Lang : LocallyCartesianClosed(\infty,1)Categories \to HomotopyTypeTheory
\end{displaymath}
from [[locally cartesian closed (∞,1)-categories]] to [[homotopy type theory]] which is expected to be an [[equivalence of (∞,1)-categories]].

As the above table shows, from the perspective of [[dependent type theory]] [[categories]] $\mathcal{C}$ are regarded systematically via the collection of their [[slice categories]] (their associated ``[[hyperdoctrines]]''). If $\mathcal{C}$ is a [[locally cartesian closed category]] then every [[morphism]] $f : X \to Y$ in $\mathcal{C}$ induces an [[adjoint triple]] of functors between the corresponding slice categories

\begin{uremark}
([[dependent sum]] $\dashv$ [[base change]] $\dashv$ [[dependent product]]) = $(\sum_f \dashv f^* \dashv \prod_f) : \mathcal{C}_{/X} \to \mathcal{C}_{/Y}$.

\end{uremark}
Many familiar constructions are usefully expressed entirely in terms of these [[adjoint triples]]. For instance the [[internal hom]] in a slice category.

While this is in principle clear/well known, the systematic use of the base change adjoint triple enforced by type theory turns out to lead to various elegant constructions that have not found much attention before, and which can be useful in applications.

\hypertarget{homotopy_pullbacks}{}\subsection*{{Homotopy pullbacks}}\label{homotopy_pullbacks}

The yoga of [[homotopy pullbacks]], [[homotopy fibers]], [[loop space objects]], [[fiber sequences]] etc. is basic to [[homotopy theory]], and of course is also fairly elementary. Homotopy type theory can hardly add a previously unknown fact here. Nevertheless, it is noteworthy that many of these constructions, elementary as they are, look \emph{even simpler} when formulated in homotopy type theory.

\begin{tabular}{l|l}
[[category theory]]&[[type theory]]\\
\hline 
[[homotopy pullback]] $\itexarray{A \times_C^h B &\to& B \\ \downarrow &\swArrow_{\simeq}& \downarrow^{\mathrlap{g}} \\ A &\stackrel{f}{\to}& X}$&$\underset{a : A, b : B}{\sum} (f(a) = g(b))$ / $\{ a : A, b : B ; (f(a) = g(b)) \}$\\
[[homotopy fiber]] $\itexarray{hfib(f) &\to& * \\ \downarrow &\swArrow_{\simeq}& \downarrow^{\mathrlap{}} \\ A &\stackrel{f}{\to}& X}$&$\sum_{a : A} (f(a) = *)$ / $\{ a : A ; (f(a) = *) \}$\\
[[mapping cocylinder]] $\itexarray{ CoCyl(f) &\to& X \\ \downarrow && \downarrow^{\mathrlap{f}} \\ Y^I &\stackrel{d_0}{\to} & Y \\ \downarrow^{\mathrlap{d_1}} \\ Y }$&$y : Y \vdash \underset{x : X}{\sum} (f(x) = y)$\\
[[free loop space object]] $\itexarray{\mathcal{L}X &\to& X \\ \downarrow &\swArrow_{\simeq}& \downarrow \\ X &\to& X \times X}$&$\underset{x,y : X}{\sum} (x = y) and (x = y)$\\
\end{tabular}

\begin{itemize}%
\item [[pasting law]] (\ldots{})

\end{itemize}
\hypertarget{detecting_truncation}{}\subsection*{{Detecting $n$-truncation}}\label{detecting_truncation}

The central insight (due to [[Vladimir Voevodsky]]) that boosts dependent type theory with identity types to genuine homotopy type theory is that in terms of [[identity types]] there are simple natural expressions for [[n-truncated|n-truncation]] and detection of $n$-truncation of objects and morphisms. Translated via [[categorical semantics]] to [[homotopy theory]], these formulas turn out to refomulate some basic yoga of model category computation in a new way that hasn't received attention before in homotopy theory, emphasizing the base change adjoint triple.

\begin{tabular}{l|l}
[[category theory]]&[[type theory]]\\
\hline 
object $X$ is [[(-2)-truncated]]/[[contractible]]&[[isContr]]$(X) = \sum_{x : X} \prod_{y : X} (x = y)$\\
morphism $X$ is [[(-2)-truncated]]/[[equivalence in an (infinity,1)-category&equivalence]]\\
\end{tabular}

\begin{remark}
\label{}\hypertarget{}{}
In the [[(∞,1)-category]] [[∞Grpd]] it is true that a morphism $f : X \to Y$ is an equivalence precisely if for all global points $y : * \to Y$ the corresponding homotopy fiber of $f$ is contractible. The same simple statement is not available \emph{in the ``external'' logic} for a general [[(∞,1)-category]], simply because there an object $Y$ may not even have enough global points (it may be non-trivial and have no global point).

The above is useful in that it says that \emph{in the [[internal logic]]} of the $(\infty,1)$-category, the simple statement familiar form [[∞Grpd]] is true generally, after all.

\end{remark}
\hypertarget{Induction}{}\subsection*{{Homotopy algebras over homotopy monads}}\label{Induction}

We have seen that homtopy type theory naturally describes [[homotopy pullbacks]] and some other finite [[(∞,1)-limits]] in terms of [[identity types]] and the [[base change]] [[adjoint triple]]. The [[duality|dual]] notion, \emph{[[homotopy colimits]]}, is conceived of in homotopy type theory as a (vast) generalization of the basic notion of \emph{[[induction]]} and \emph{[[recursion]]}, subsumed type-theoretically in the notion of \emph{[[inductive type]]}, roughly a kind of [[type]] that is given by [[generators and relations]].

Traditionally inductive types are in category theory [[categorical semantics|interpreted]] as \emph{[[algebras over an endofunctor]]}. While useful, this is a concept somewhat alien to usual constructions in category theory or homotopy theory. The natural notion is instead that of an [[algebra over a monad]]. While an [[algebra over an endofunctor]] may be thought of as a monad-algebra over a [[free monad]], from the point of view of homotopy theory it still seems unnatural to restrict attention to free monads.

However, after generalization to \emph{[[homotopy type theory]]} this is rectified: here the homotopy-theoretic notion of [[induction]] turns out to be about [[∞-algebras over an (∞,1)-monad]], as one would hope, and a \emph{[[higher inductive type]]} is an [[initial algebras of a presentable (∞,1)-monad]].

(\ldots{})

\hypertarget{detecting_connectedness}{}\subsection*{{Detecting $n$-connectedness}}\label{detecting_connectedness}

\newline \hypertarget{homotopy_pushouts}{}\subsection*{{Homotopy pushouts}}\label{homotopy_pushouts}

\begin{tabular}{l|l}
[[category theory]]&[[type theory]]\\
\hline 
[[homotopy pushout]] $\itexarray{ C &\stackrel{g}{\to}& B \\ {}^{\mathllap{f}}\downarrow &\swArrow_{\simeq}& \downarrow \\ A &\to&  A \coprod_C^h B}$&$hpushout (A\,B\,C : Type) (f : C \to A) (g : C \to B) : Type \coloneqq \left\{ \itexarray{inl : B \to hpushout(f,g) \\ inr : A \to hpushout(f,g) \\ glue \prod_{c : C} (inl(f(c)) = inr(g(c)))} \right.$\\
\end{tabular}

(\ldots{})

\hypertarget{constructing_truncation}{}\subsection*{{Constructing $n$-truncation}}\label{constructing_truncation}

\begin{tabular}{l|l}
[[category theory]]&[[type theory]]\\
\hline 
[[truncated object in an (infinity,1)-category&(-1)-truncation]] $\tau_{-1}(-)$\\
\end{tabular}

\hypertarget{specific_hott_proofs_in_homotopy_theory}{}\subsection*{{Specific HoTT proofs in homotopy theory}}\label{specific_hott_proofs_in_homotopy_theory}

We list in the following theorems in homotopy theory together with such proofs of them in terms of homotopy type theory language that are either new (to the best of our knowledge), or else that are at least considerably simpler than earlier proofs with traditional homotopy theory tools.

\hypertarget{blakersmassey_theorem}{}\subsubsection*{{Blakers-Massey theorem}}\label{blakersmassey_theorem}

see at \emph{[[Blakers-Massey theorem]]}

\hypertarget{essential_uniqueness_of_group_units}{}\subsubsection*{{Essential uniqueness of group units}}\label{essential_uniqueness_of_group_units}

(\ldots{})

\hypertarget{equivalence_of_notions_of_stabilizer_groups}{}\subsubsection*{{Equivalence of notions of stabilizer $\infty$-groups}}\label{equivalence_of_notions_of_stabilizer_groups}

(\ldots{}) \href{http://nforum.mathforge.org/discussion/3454/stabilizer-subgroup/?Focus=28287#Comment_28287}{\ldots{}}

(\ldots{})



\end{document}