\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*{identity type}

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

\hypertarget{equality_and_equivalence}{}\paragraph*{{Equality and Equivalence}}\label{equality_and_equivalence}

[[!include equality and equivalence - contents]]

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

[[!include type theory - contents]]

\hypertarget{induction}{}\paragraph*{{Induction}}\label{induction}

[[!include induction - contents]]

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

\noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak
\noindent\hyperlink{Definition}{Definition}\dotfill \pageref*{Definition} \linebreak
\noindent\hyperlink{ExplicitDefinition}{With introduction and elimination rules}\dotfill \pageref*{ExplicitDefinition} \linebreak
\noindent\hyperlink{InTermsOfInductiveTypes}{In terms of inductive types}\dotfill \pageref*{InTermsOfInductiveTypes} \linebreak
\noindent\hyperlink{EtaConversion}{Extensionality and $\eta$-conversion}\dotfill \pageref*{EtaConversion} \linebreak
\noindent\hyperlink{categorical_semantics}{Categorical semantics}\dotfill \pageref*{categorical_semantics} \linebreak
\noindent\hyperlink{prerequisites}{Prerequisites}\dotfill \pageref*{prerequisites} \linebreak
\noindent\hyperlink{interpretation_in_a_typetheoretic_model_category}{Interpretation in a type-theoretic model category}\dotfill \pageref*{interpretation_in_a_typetheoretic_model_category} \linebreak
\noindent\hyperlink{weak_groupoids}{Weak $\omega$-groupoids}\dotfill \pageref*{weak_groupoids} \linebreak
\noindent\hyperlink{related_concepts}{Related concepts}\dotfill \pageref*{related_concepts} \linebreak
\noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak
\noindent\hyperlink{ReferencesExplicitDefinition}{Explicit definition}\dotfill \pageref*{ReferencesExplicitDefinition} \linebreak
\noindent\hyperlink{ReferencesByInductiveTypes}{As inductive types}\dotfill \pageref*{ReferencesByInductiveTypes} \linebreak
\noindent\hyperlink{weak_factorization_systems}{Weak factorization systems}\dotfill \pageref*{weak_factorization_systems} \linebreak
\noindent\hyperlink{types_as_groupoids}{Types as $\infty$-groupoids}\dotfill \pageref*{types_as_groupoids} \linebreak


\begin{quote}%
 The [[first original law of thought]] (\href{Science+of+Logic#875}{WdL \S{}875}): everything is identical with itself (\href{Science+of+Logic#863}{WdL \S{}863}), no two things are like each other (\href{Science+of+Logic#903}{WdL \S{}903}).


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

In [[intensional type theory]] under the [[propositions as types]] paradigm, an \textbf{identity type} (or \textbf{equality type}) is the incarnation of [[equality]]. That is, for any [[type]] $A$ and any [[terms]] $x,y:A$, the type $Id_A(x,y)$ is ``the type of [[proofs]] that $x=y$'' or ``the type of reasons why $x=y$''.

To contrast with ``computational'' or [[definitional equality]], sometimes inhabitation of an identity type is sometimes called \textbf{propositional equality}. The identity type $Id_A(x,y)$ is sometimes written $Eq_A(x,y)$ or just $(x=y)$, but in this article we reserve the latter for definitional equality.

In \emph{[[extensional type theory|extensional]]} type theory, such as that modeled in the [[internal logic]] of a 1-category, equality is an [[h-proposition]], and hence each $Id_A(x,y)$ is a [[subsingleton]]. However, in the internal type theory of [[higher category theory|higher categories]], such as the [[internal logic of an (∞,1)-topos]], identity types represent [[path objects]] and are highly nontrivial. One speaks of \emph{[[homotopy type theory]]}. In these cases, one may write for instance $Path_A(x,y)$ instead of $Id_A(x,y)$.

\hypertarget{Definition}{}\subsection*{{Definition}}\label{Definition}

The definition of identity types was originally given in explicit form by [[Per Martin-Löf|Martin-Löf]], in terms of introduction and elimination rules. Later, it was realized that this was a special case of the general notion of [[inductive type]]. We will discuss both formulations.

\begin{itemize}%
\item \hyperlink{ExplicitDefinition}{with introduction and elimination rules}.


\item \hyperlink{InTermsOfInductiveTypes}{in terms of inductive types}



\end{itemize}
\hypertarget{ExplicitDefinition}{}\subsubsection*{{With introduction and elimination rules}}\label{ExplicitDefinition}

The rules for forming identity types and terms are as follows (expressed in [[sequent calculus]]). First the rule that defines the identity type itself, as a [[dependent type]], in some [[context]] $\Gamma$.

\textbf{[[type formation]]}

\begin{displaymath}
\frac{\Gamma \vdash A:Type}
{\Gamma, x:A, y:A \vdash Id_A(x,y):Type}
\end{displaymath}
Now the basic ``introduction'' rule, which says that everything is equal to itself in a canonical way.

\textbf{[[term introduction]]}

\begin{displaymath}
\frac{\Gamma \vdash A:Type}
{\Gamma, x:A \vdash r(x) : Id_A(x,x)}
\end{displaymath}
To a category theorist, it might be more natural to call this $1_X$. The traditional notation $r(x)$ indicates that this is a canonical proof of the \emph{[[reflexive relation|reflexivity]]} of equality.

Then we have the ``elimination'' rule, which is easily the most subtle and powerful.

\textbf{[[term elimination]]}

\begin{displaymath}
\frac{\Gamma, x:A, y:A, p:Id_A(x,y), \Delta(x,y,p) \vdash C(x,y,p):Type \qquad
\Gamma, x:A, \Delta(x,x,r(x)) \vdash t : C(x,x,r(x))}
{\Gamma, x:A, y:A, p:Id_A(x,y), \Delta(x,y,p) \vdash J(t;x,y,p) : C(x,y,p)}
\end{displaymath}
Ignore the presence of the additional context $\Delta$ for now; it is unnecessary if we also have [[dependent product type]]s. The elimination rule then says that if:

\begin{enumerate}%
\item for any $x,y:A$ and any reason $p:Id_A(x,y)$ why they are the same, we have a type $C(x,y,p)$, and
\item if $x$ and $y$ are actually identical and $p:Id_A(x,x)$ is the reflexivity proof $r(x)$, then we have a specified term $t:C(x,x,r(x))$,

\end{enumerate}
then we can construct a canonically defined term $J(t;x,y,p):C(x,y,p)$ for \emph{any} $x$, $y$, and $p:Id_A(x,y)$, by ``transporting'' the term $t$ along the proof of equality $p$. In homotopical or categorical models, this can be viewed as a ``path-lifting'' property, i.e. that the [[display map]]s are some sort of [[fibration]]. This can be made precise with the [[identity type weak factorization system]].

A particular case is when $C$ is a term representing a proposition according to the propositions-as-types philosophy. In this case, the elimination rule says that in order to prove a statement is true about all $x,y,p$, it suffices to prove it in the special case for $x,x,r(x)$.

Finally, we have the ``computation'' or [[β-reduction]] rule. This says that if we substitute along a [[reflexive relation|reflexivity]] proof, nothing happens.

\textbf{[[computation rule]]}

\begin{displaymath}
\frac{\Gamma, x:A, y:A, p:Id_A(x,y), \Delta(x,y,p) \vdash C(x,y,p):Type \qquad
\Gamma, x:A, \Delta(x,x,r(x)) \vdash t : C(x,x,r(x))}
{\Gamma, x:A, \Delta(x,x,r(x)) \vdash J(t;x,x,r(x)) = t}
\end{displaymath}
Note that the equality $=$ in the conclusion of the computation rule is [[definitional equality]], not an instance of the identity/equality type itself.

These rules may seem a little ad-hoc, but they are actually a particular case of the general notion of [[inductive type]].

\hypertarget{InTermsOfInductiveTypes}{}\subsubsection*{{In terms of inductive types}}\label{InTermsOfInductiveTypes}

Using [[inductive types]] the notion of identity types is encoded in a single line (see \hyperlink{Licata11}{Licata 11}, \hyperlink{Shulman12}{Shulman 12}).

In [[Coq]] notation we can say

\begin{verbatim}Inductive id {A} : A -> A -> Type := idpath : forall x, id x x.   \end{verbatim}
In other words, the identity type of $A$ is inductively generated by [[reflexive relation|reflexivity]] $x = x$ (the ``[[first law of thought]]''), in the same way that the [[natural numbers]] are inductively generated by [[zero]] and [[successor]]. From this, the above introduction, elimination, and computation rules are all derived automatically.

This is the approach to identity types taken by practical work in [[homotopy type theory]], which is usually implemented in [[Coq]] or [[Agda]]. See, for instance, \hyperlink{Overturev}{Overture.v}

An essentially equivalent way to give the definition, due to Paulin-Mohring, is

\begin{verbatim}Inductive id {A} (x:A) : A -> Type := idpath : id x x.   \end{verbatim}
The difference here is that now $x$ is a \emph{parameter} of the inductive definition rather than an \emph{index}. In other words, the first definition says ``for each type $A$, we have a type $Id_A$ dependent on $A\times A$, inductively defined by a constructor $idpath$ which takes an element $x\colon A$ as input and yields output in $Id_A(x,x)$'' while the second definition says ``for each type $A$ and each element $x\colon A$, we have a type $Id_A(x)$ dependent on $A$, inductively defined by a constructor $idpath$ which takes \emph{no} input and yields output in $Id_A(x)(x)$.'' The two formulations can be proven equivalent, but sometimes one is more convenient than the other.

\hypertarget{EtaConversion}{}\subsubsection*{{Extensionality and $\eta$-conversion}}\label{EtaConversion}

Almost all types in type theory can be given both [[β-reduction]] and [[η-reduction]] rules. $\beta$-reduction specifies what happens when we apply an eliminator to a term obtained by a constructor; $\eta$-reduction specifies the reverse. Above we have formulated only the $\beta$-reduction rule for identity types; the $\eta$-conversion rule would be the following:

\begin{displaymath}
\frac{\Gamma, x:A, y:A, p:Id_A(x,y), \Delta(x,y,p) \vdash C(x,y,p):Type \qquad
\Gamma, x:A, y:A, p:Id_A(x,y), \Delta(x,x,r(x)) \vdash t : C(x,y,p)}
{\Gamma, x:A, y:A, p:Id_A(x,y), \Delta(x,y,p) \vdash J(t[y/x, r(x)/p];x,y,p) = t}
\end{displaymath}
This says that if $C$ is a type which we can use the eliminator $J$ to construct a term of, but we already \emph{have} a term $t$ of that type, then if we restrict $t$ to [[reflexive relation|reflexivity]] inputs and then apply $J$ to construct a term of type $C$, the result is the same as the term $t$ we started with. As in the $\beta$-reduction rule, the $=$ in the conclusion refers to [[definitional equality]].

This $\eta$-conversion rule has some very strong consequences. For instance, suppose $x\colon A$, $y\colon A$, and $p\colon Id_A(x,y)$, and let $C \coloneqq A$. Then with $t=x$, the $\eta$-conversion rule tells us that $x = J(x[y/x,r(x)/p];x,y,p)$. And with $t=y$, the $\eta$-conversion rule tells us that $y = J(y[y/x,r(x)/p];x,y,p)$. But substituting $y$ for $x$ (and $r(x)$ for $p$) in the term $y$ simply yields the term $y$, which is the same as the result of substituting $y$ for $x$ and $r(x)$ for $p$ in the term $x$. Thus, we have

\begin{displaymath}
x = J(x;x,y,p) = y
\end{displaymath}
In other words, if $Id_A(x,y)$ is inhabited (that is, $x$ and $y$ are propositionally equal) then in fact $x$ and $y$ are definitionally equal. Moreover, by a similar argument we can show that

\begin{displaymath}
p = J(p[y/x, r(x)/p];x,y,p) = J(r(x)[y/x,r(x)/p];x,y,p) = r(x).
\end{displaymath}
(Here we are eliminating into the type $C(x,y,p) \coloneqq Id_A(x,y)$. The term $r(x)$ may be regarded as belonging to this type, because we have already shown that $x$ and $y$ are \emph{definitionally} equal.)

Thus, the definitional $\eta$-conversion rule for identity types implies that the type theory is [[extensional type theory|extensional]] in a very strong sense. (This was observed already in (\hyperlink{Streicher}{Streicher}).) For this reason, in [[homotopy type theory]] we do not assume the $\eta$-conversion rule for identity types.

This sort of extensionality in type theory is also problematic for non-homotopical reasons: since type-checking in dependent type theory depends on definitional equality, but the above rule implies that definitional equality depends on inhabitation of identity types, this makes definitional equality and hence type-checking \emph{undecidable} in the formal computational sense. Thus, $\eta$-conversion for identity types is often omitted (as in [[Coq]]).

On the other hand, it is possible to prove a \emph{propositional} version of $\eta$-conversion using only the identity types as defined above without definitional $\eta$-conversion. In other words, given the hypotheses of the above $\eta$-conversion rule, we can construct a term belonging to the type

\begin{displaymath}
Id_{C(x,y,p)}(J(t[y/x, r(x)/p];x,y,p), t).
\end{displaymath}
This has none of the bad consequences of definitional $\eta$-conversion, and in particular does not imply that the type theory is extensional. The argument that $p\colon Id_A(x,y)$ implies $x=y$ becomes the tautologous statement that if $p\colon Id_A(x,y)$ then $p\colon Id_A(x,y)$, while the subsequent argument that $p= r(x)$ fails because $x$ and $y$ are no longer \emph{definitionally} equal, so $r(x)$ does not have type $Id_A(x,y)$. We can \emph{transport} it along $p$ to obtain a term of this type, but then we obtain only that $p$ is equal to the transport of $r(x)$ along $p$, which is a perfectly intensional/homotopical statement.

\hypertarget{categorical_semantics}{}\subsection*{{Categorical semantics}}\label{categorical_semantics}

We discuss the [[categorical semantics]] for identity types in the extensional case, and identity types in the [[categorical semantics of homotopy type theory]] in the intensional case.

In categorical models of [[extensional type theory]], generally every [[morphism]] of the category is allowed to represent a [[dependent type]], and the extensional identity types are represented by [[diagonal]] maps $A\to A\times A$.

By contrast, in models of [[intensional type theory]], there is only a particular class of [[display maps]] or [[fibrations]] which are allowed to represent dependent types, and intensional identity types are represented by [[path objects]] $P A \to A \times A$.

Both of these cases apply in particular to models in the [[category of contexts]] of the type theory itself, i.e. the [[term model]].

\hypertarget{prerequisites}{}\subsubsection*{{Prerequisites}}\label{prerequisites}

By the standard construction of [[mapping path spaces]] out of [[path space objects]], the existence of identity types allows one to construct a [[weak factorization system]].

Conversely, since any weak factorization system gives rise to [[path objects]] by factorization of [[diagonal maps]], one may hope to construct a [[model]] of type theory with identity types in a category equipped with a WFS $(L,R)$. There are four obstacles in the way of such a construction.

\begin{enumerate}%
\item In order to handle the additional [[context]] $\Delta$ in the explicit definition above, it turns out to be necessary to assume that $L$-maps are preserved by [[pullback]] along $R$-maps between $R$-objects. (Such a condition is also necessary in order to interpret type-theoretic [[dependent products]] in a [[locally cartesian closed category]].)


\item This enables us to define identity types with their elimination and computation rules ``locally'', i.e. for each type individually. However, every construction in type theory is stable under [[substitution]]. This means that if $y\colon Y\vdash A(y)\colon Type$ is a dependent type and $f\colon X\to Y$ is a morphism, then the identity type $x\colon X \vdash Id_{A(f(x))}(-,-)\colon Type$ is the same whether we first construct $Id_{A(y)}$ and then substitute $f(x)$ for $y$, or first substitute $f(x)$ for $y$ to obtain $A(f(x))$ and then construct its identity type. In order for this to hold up to isomorphism, we need to require that the WFS have \emph{stable path objects} --- a choice of path object data in each slice category which is preserved by pullback. In \hyperlink{Warren}{(Warren)} it is shown that any [[simplicial model category]] in which the [[cofibrations]] are the [[monomorphisms]] can be equipped with stable path objects, while \hyperlink{vdBergGarner}{(Garner-van den Berg)} it is shown that the presence of internal path-categories also suffices.


\item The eliminator term $J$ of identity types in type theory is also preserved by substitution. This imposes an additional \emph{[[coherence]]} requirement which is tricky to obtain categorically. See the references by \hyperlink{Warren}{Warren} and \hyperlink{vdBergGarner}{Garner-van den Berg} for methods that ensure this, such as by invoking an [[algebraic weak factorization system]]. It can also be handled \emph{a la} [[Vladimir Voevodsky|Voevodsky]] by using a (possibly [[univalence axiom|univalent]]) [[universe]].


\item Finally, substitution in type theory is strictly functorial/[[associativity|associative]], whereas it is modeled categorically by pullback which is generally not strictly so. This is a general issue with the categorical interpretation of [[dependent type theory]], not something specific to identity types. It can be resolved by passing to a [[split fibration]] which is equivalent to the [[codomain fibration]], or by making use of a [[universe]]. See [[categorical model of dependent types]].



\end{enumerate}
\hypertarget{interpretation_in_a_typetheoretic_model_category}{}\subsubsection*{{Interpretation in a type-theoretic model category}}\label{interpretation_in_a_typetheoretic_model_category}

Assume then that a category $\mathcal{C}$ with suitable WFSs has been chosen, for instance a [[type-theoretic model category]]. Then

\begin{itemize}%
\item The interpretation of a type $\vdash A : Type$ is as a [[fibrant object]] $[\vdash A : Type]$ which we will just write ``$A$'' for short.


\item \textbf{type formation}

The identity type $a, b : A \vdash Id_A(a,b) : Type$ is interpreted as [[generalized the|the]] [[path space object]] [[fibration]]

\begin{displaymath}
\itexarray{
     A^I
     \\
     \downarrow
     \\
     A \times A
  }
\end{displaymath}

\item \textbf{term introduction}

By definition of [[path space object]], there exists a lift $\sigma$ in

\begin{displaymath}
\itexarray{
     && A^I
     \\
     & {}^{\mathllap{\sigma}}\nearrow& \downarrow
     \\
     A &\stackrel{(id,id)}{\to}& A \times A
  }
  \,.
\end{displaymath}
By the [[universal property]] of the [[pullback]] this is equivalently a [[section]] of the [[pullback]] of the path space object along the [[diagonal]] morphism $(id,id) : A \to A \times A$.

\begin{displaymath}
\itexarray{
     && (id,id)^* A^I &\to& A^I
     \\
     &{}^{\mathllap{\sigma}}\nearrow& \downarrow & & \downarrow
     \\
     A &=& A &\stackrel{(id,id)}{\to}& A \times A
  }
  \,.
\end{displaymath}
Since $(id, id)^* A^I$ is the interpretation of the [[substitution]]\newline $a : A \vdash Id_A (a,a) : Type$ in this sense $\sigma$ is now the interpretation of a term $a : A \vdash r_A : Id_A (a,a)$.


\item \textbf{term elimination}

A type depending on an identity type

\begin{displaymath}
a, b : A, p : Id_A(a,b) \vdash C(a,b,p)
\end{displaymath}
is interpreted as a [[fibration]]

\begin{displaymath}
\itexarray{
    C
    \\
    \downarrow
    \\
    A^I
  }
  \,.
\end{displaymath}
The [[substitution]] $C(a,a,r_a)$ is interpreted by the [[pullback]]

\begin{displaymath}
\itexarray{
    (id,id)^* C &\to& C
    \\
    \downarrow && \downarrow
    \\
    A &\stackrel{(id,id)}{\to}& A \times A
  }
  \,.
\end{displaymath}
Therefore a [[term]] $t : C(a,a,r_a)$ is interpreted as a [[section]] of this pullback

\begin{displaymath}
\itexarray{
    && (id,id)^* C &\to& C
    \\
    &{}^{\mathllap{t}}\nearrow& \downarrow && \downarrow
    \\
    A &=& A &\stackrel{(id,id)}{\to}& A \times A
  }
  \,.
\end{displaymath}
By the [[universal property]] of the pullback, this is equivalently a morphism $t$ in

\begin{displaymath}
\itexarray{
    && C
    \\
    & {}^{\mathllap{t}}\nearrow & \downarrow
    \\
    A &\stackrel{(id,id)}{\to}& A \times A
  }
  \,.
\end{displaymath}
The elimination rule says that given such $t$, there exists a compatible section of $C \to Id_A$. If we redraw the previous diagram as a square, then this section is a \emph{[[lifting problem|lift]]} in that diagram

\begin{displaymath}
\itexarray{   
    A &\to& C
    \\
    {}^{\mathllap{r}}\downarrow &\nearrow& \downarrow
    \\
    A^I &=& A^I
  }
  \,.
\end{displaymath}
In particular, if $C$ itself is the pullback of a fibration $D \to B$ along a morphism $A^I \to B$, then $r$ has the left lifting property also against that fibration

\begin{displaymath}
\itexarray{   
    A &\to& C &\to& D
    \\
    {}^{\mathllap{r}}\downarrow &\nearrow& \downarrow && \downarrow
    \\
    A^I &=& A^I &\to& B
  }
  \,.
\end{displaymath}
So the term elimination rule says that the interpretaton $A \to A^I$ of $a : A \vdash r(a) : Id_A (a,a)$ has the [[left lifting property]] against all fibrations, hence that $A \to A^I$ is to be interpreted as an acyclic cofibration.



\end{itemize}
\hypertarget{weak_groupoids}{}\subsubsection*{{Weak $\omega$-groupoids}}\label{weak_groupoids}

Some of the first work noticing the homotopical / higher-categorical interpretation of identity types (see below) focused on the fact that the tower of iterated identity types of a type has the structure of an internal \emph{[[algebraic definition of higher categories|algebraic]]} [[∞-groupoid]].

In retrospect, this is roughly an algebraic version of the standard fact that every object of a model category (or more generally a [[category of fibrant objects]] or a category with a weak factorization system) admits a [[simplicial resolution]] which is an [[internalization|internal]] [[Kan complex]], i.e. a nonalgebraic $\infty$-groupoid. Note, however, that the first technical condition above (stability of $L$-maps under pullback along $R$-maps) seems to be necessary for the algebraic version of the result to go through.

\hypertarget{related_concepts}{}\subsection*{{Related concepts}}\label{related_concepts}

\begin{itemize}%
\item [[identity of indiscernibles]]


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


\item [[axiom K]]


\item [[axiom UIP]]



\end{itemize}
\hypertarget{references}{}\subsection*{{References}}\label{references}

\hypertarget{ReferencesExplicitDefinition}{}\subsubsection*{{Explicit definition}}\label{ReferencesExplicitDefinition}

A survey is in chapter 1 of

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

\end{itemize}
Extensionality and intensionality isses are studied in

\begin{itemize}%
\item [[Thomas Streicher]], \emph{Investigations Into Intensional Type Theory}, Habilitationsschrift (\href{http://www.mathematik.tu-darmstadt.de/~streicher/HabilStreicher.pdf}{pdf})

\end{itemize}
\hypertarget{ReferencesByInductiveTypes}{}\subsubsection*{{As inductive types}}\label{ReferencesByInductiveTypes}

\begin{itemize}%
\item [[Dan Licata]], \emph{\href{https://homotopytypetheory.org/2011/04/10/just-kidding-understanding-identity-elimination-in-homotopy-type-theory/}{Understanding Identity Elimination in Homotopy Type Theory}}, 2011


\item [[Mike Shulman]], \emph{Inductive types and identity types}, 2012 (\href{https://home.sandiego.edu/~shulman/hottseminar2012/03induction-handout1up.pdf}{pdf})


\item \href{https://github.com/HoTT/HoTT/blob/master/theories/Basics/Overture.v#L169-L170}{https://github.com/HoTT/HoTT/blob/master/theories/Basics/Overture.v}



\end{itemize}
\hypertarget{weak_factorization_systems}{}\subsubsection*{{Weak factorization systems}}\label{weak_factorization_systems}

\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 [[Steve Awodey]] and [[Michael Warren]], \emph{Homotopy theoretic models of identity types}, \href{http://arxiv.org/abs/0709.0248}{arXiv}.


\item [[Nicola Gambino]], [[Richard Garner]], \emph{The identity type weak factorisation system}, \href{http://arxiv.org/abs/0803.4349}{arXiv}


\item [[Richard Garner]], [[Benno van den Berg]], \emph{Topological and simplicial models of identity types}, \href{http://arxiv.org/abs/1007.4638}{arXiv}.



\end{itemize}
\hypertarget{types_as_groupoids}{}\subsubsection*{{Types as $\infty$-groupoids}}\label{types_as_groupoids}

The observation that identity types witness [[groupoid]] and [[infinity-groupoid]]-structure:

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


\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}
For more see the references at \emph{[[homotopy type theory]]}.

See also

\begin{itemize}%
\item [[Benno van den Berg]], [[Richard Garner]], \emph{Types are weak $\omega$-groupoids} , (\href{http://arxiv.org/abs/0812.0298}{arXiv:0812.0298})


\item [[Peter LeFanu Lumsdaine]], \emph{Weak $\omega$-categories from intensional type theory} , (\href{http://arxiv.org/abs/0812.0409}{arXiv:0812.0409})



\end{itemize}
[[!redirects identity types]] [[!redirects equality type]] [[!redirects equality types]] [[!redirects path type]] [[!redirects path types]] [[!redirects stable path object]] [[!redirects stable path objects]] [[!redirects propositional equality]] [[!redirects propositionally equal]]

[[!redirects principle of substitution]] [[!redirects principle of substitution of equals for equals]] [[!redirects principle of substituting equals for equals]]

[[!redirects intensional identity type]] [[!redirects intensional identity types]] [[!redirects extensional identity type]] [[!redirects extensional identity types]] [[!redirects identical]]



\end{document}