\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*{univalence axiom} \hypertarget{context}{}\subsubsection*{{Context}}\label{context} \hypertarget{type_theory}{}\paragraph*{{Type theory}}\label{type_theory} [[!include type theory - contents]] \hypertarget{equality_and_equivalence}{}\paragraph*{{Equality and Equivalence}}\label{equality_and_equivalence} [[!include equality and equivalence - contents]] \hypertarget{universes}{}\paragraph*{{Universes}}\label{universes} [[!include universe - contents]] \hypertarget{homotopy_theory}{}\paragraph*{{Homotopy theory}}\label{homotopy_theory} [[!include homotopy - 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{in_the_type_theory}{In the type theory}\dotfill \pageref*{in_the_type_theory} \linebreak \noindent\hyperlink{InCategoricalSemantics}{In categorical semantics}\dotfill \pageref*{InCategoricalSemantics} \linebreak \noindent\hyperlink{InSimplicialSets}{In simplicial sets}\dotfill \pageref*{InSimplicialSets} \linebreak \noindent\hyperlink{InSimplicialPresheaves}{In simplicial presheaves}\dotfill \pageref*{InSimplicialPresheaves} \linebreak \noindent\hyperlink{properties}{Properties}\dotfill \pageref*{properties} \linebreak \noindent\hyperlink{relation_to_function_extensionality}{Relation to function extensionality}\dotfill \pageref*{relation_to_function_extensionality} \linebreak \noindent\hyperlink{WeakerEquivalentForms}{Weaker equivalent forms}\dotfill \pageref*{WeakerEquivalentForms} \linebreak \noindent\hyperlink{Canonicity}{Canonicity}\dotfill \pageref*{Canonicity} \linebreak \noindent\hyperlink{related_concepts}{Related concepts}\dotfill \pageref*{related_concepts} \linebreak \noindent\hyperlink{References}{References}\dotfill \pageref*{References} \linebreak \hypertarget{idea}{}\subsection*{{Idea}}\label{idea} In [[intensional type theory]], [[identity types]] behave like [[path space objects]]; this viewpoint is called [[homotopy type theory]]. This induces furthermore a notion of [[homotopy fibers]], hence of [[homotopy equivalence]]s between [[types]]. On the other hand, if type theory contains a [[universe]] [[Type]], so that types can be considered as \emph{points} of $Type$, then between two types we also have an [[identity type]] $Paths_{Type}(X,Y)$. The \emph{univalence axiom} says that these two notions of ``sameness'' for types are the same. Extensionality principles like [[function extensionality]], [[propositional extensionality]], and univalence (``typal extensionality'') are naturally regarded as a stronger form of \emph{[[identity of indiscernibles]]}. In particular, the [[consistency]] of univalence means that in [[Martin-Löf type theory]] without univalence, one cannot define any [[predicate]] that provably distinguishes isomorphic [[types]]; thus isomorphic types are ``externally indiscernible'', and univalence incarnates that principle internally by making them identical. The name \emph{univalence} (due to Voevodsky) comes from the following reasoning. A fibration or bundle $p\colon E\to B$ of some sort is commonly said to be \emph{universal} if every other bundle of the same sort is a pullback of $p$ in a unique way (up to homotopy). Less commonly, a bundle is said to be \emph{versal} if every other bundle is a pullback of it in \emph{some} way, not necessarily unique. By contrast, a bundle is said to be \emph{univalent} if every other bundle is a pullback of it in \emph{at most one} way (up to homotopy). In the language of [[(∞,1)-category]] theory, a univalent bundle is an [[object classifier]]. The univalence axiom does not \emph{literally} say that anything is univalent in this sense. However, it is \emph{equivalent} to saying that the canonical fibration over $Type$ is univalent: every fibration with \emph{small} fibers is an essentially unique pullback of this one (while those with large fibers are not, they are pullbacks of the next higher $Type_1$). For a description of this equivalence, see section 4.8 of the [[HoTT Book]] (syntactically) and \hyperlink{GepnerKock12}{Gepner-Kock} (semantically). \hypertarget{definition}{}\subsection*{{Definition}}\label{definition} We state univalence first in ([[intensional type theory|intensional]]) [[type theory]] and then in its [[categorical semantics]]. \hypertarget{in_the_type_theory}{}\subsubsection*{{In the type theory}}\label{in_the_type_theory} Let $X$ and $Y$ be [[types]]. There is a canonically defined map from the [[identity type]] $(X = Y)$ of paths (in [[Type]]) between them to the [[function type]] $(X \stackrel{\simeq}{\to} Y)$ of [[equivalences in homotopy type theory]] between them. It can be defined by \emph{\href{inductive%20type#PathInduction}{path induction}}, i.e. the [[term elimination rule|eliminator]] for the identity types, by specifying that it takes the identity path $1_X \colon (X=X)$ to the identity equivalence of $X$. \textbf{Univalence:} \emph{For any two [[types]] $X,Y$, this map $(X=Y)\to (X\simeq Y)$ is an [[equivalence in homotopy type theory|equivalence]].} When $X$ and $Y$ are \href{propositions+as+types#PropositionsAsSomeTypes}{propositions}, univalence corresponds to [[propositional extensionality]]. Univalence is a commonly assumed [[axiom]] in [[homotopy type theory]], and is central to the proposal (\hyperlink{Voevodsky}{Voevodsky}) that this provides a natively [[homotopy theory|homotopy theoretic]] [[foundation]] of [[mathematics]] (the \emph{Univalent Foundations Project}.) \hypertarget{InCategoricalSemantics}{}\subsubsection*{{In categorical semantics}}\label{InCategoricalSemantics} Let $\mathcal{C}$ be a [[locally cartesian closed model category]] in which all objects are cofibrant. By the [[categorical semantics]] of [[homotopy type theory]], a [[dependent type]] \begin{displaymath} b : B \vdash E(b) : Type \end{displaymath} corresponds to a [[morphism]] $E \to B$ in $\mathcal{C}$ that is a [[fibration]] between fibrant objects. Then the [[dependent type|dependent]] [[function type]] \begin{displaymath} b_1, b_2 : B \vdash ( E(b_1) \to E(b_2)) : Type \end{displaymath} is interpreted as the [[internal hom]] $[-,-]_{\mathcal{C}/_{B \times B}}$ in the [[slice category]] $\mathcal{C}/_{B \times B}$ after extending $E$ to the [[context]] $B \times B$ by pulling back along the two projections $p_1, p_2 : B \times B \to B$, respectively. Hence this is interpreted as \begin{displaymath} [p_1^* E \, , \, p_2^* E]_{\mathcal{C}/_{B \times B}} \simeq [E \times B \, , \, B \times E]_{\mathcal{C}/_{B \times B}} \in \mathcal{C}/_{B \times B} \,. \end{displaymath} Consider then the [[diagonal]] morphism $\Delta_B : B \to B \times B$ in $\mathcal{C}$ as an object of $\mathcal{C}/_{B \times B}$. We would like to define a morphism \begin{displaymath} q \colon \Delta_B \to [E \times B , B \times E]_{\mathcal{C}/_{B \times B}} \,. \end{displaymath} in $\mathcal{C}/_{B \times B}$. By the defining ([[product]] $\dashv$ [[internal hom]])-[[adjunction]], it suffices to define a morphism \begin{displaymath} \Delta_B \times_{\mathcal{C}/_{B \times B}} E \times B \to B \times E \end{displaymath} in $\mathcal{C}/_{B \times B}$. But now by the [[universal property]] of [[pullback]], it suffices to define just in $\mathcal{C}_{/B}$ a morphism \begin{displaymath} \Delta_B \times_{\mathcal{C}/_{B \times B}} E \times B \to \Delta_B \times_{\mathcal{C}/_{B \times B}} B \times E\,. \end{displaymath} And since the composite pullback along either composite \begin{displaymath} B \xrightarrow{\Delta_B} B\times B \xrightarrow{\pi_1} B \end{displaymath} \begin{displaymath} B \xrightarrow{\Delta_B} B\times B \xrightarrow{\pi_2} B \end{displaymath} is the identity, both $\Delta_B \times_{\mathcal{C}/_{B \times B}} E \times B$ and $\Delta_B \times_{\mathcal{C}/_{B \times B}} B \times E$ are isomorphic to $E$; thus here we can take the [[identity]] morphism. Now, using the [[path object]] factorization in $\mathcal{C}$ \begin{displaymath} \itexarray{ B &&\stackrel{\simeq}{\hookrightarrow}&& B^I \\ & {}_{\mathllap{\Delta_B}}\searrow && \swarrow_{\mathrlap{}} \\ && B \times B } \end{displaymath} by an acyclic cofibration followed by a fibration, we obtain a fibrant replacement of $\Delta_B$ in the [[slice model category]] $\mathcal{C}_{B \times B}$. Since also $[E \times B, B \times E]_{\mathcal{C}/_{B \times B}}$ is fibrant by the axioms on the [[locally cartesian closed model category]] $\mathcal{C}$, we have a lift $\hat q$ in the [[diagram]] in $\mathcal{C}/_{B \times B}$ \begin{displaymath} \itexarray{ B &\stackrel{q}{\to}& [E \times B, B \times E]_{\mathcal{C}/_{B \times B}} \\ \downarrow &{}^{\mathllap{\hat q}}\nearrow& \downarrow \\ B^I &\to& B \times B = *_{\mathcal{C}/_{B \times B}} } \,. \end{displaymath} This lift is the interpretation of the [[identity type|path induction]] that deduces a map on all paths $\gamma \in B^I$ from one on just the identity paths $id_b \in B \hookrightarrow B^I$. Finally, let $Eq(E) \hookrightarrow [E \times B , B \times E]_{\mathcal{C}/_{B \times B}}$ be the [[subobject]] on the weak equivalences (\ldots{}), and observe that $q$ and $\hat q$ factor through this to give a morphism \begin{displaymath} \hat q : B^I \to Eq(E) \,. \end{displaymath} The fibration $E \to B$ is \textbf{univalent} in $\mathcal{C}$ if this morphism is a weak equivalence. By the [[2-out-of-3 property]], of course, it is equivalent to ask that $q\colon B\to Eq(E)$ be a weak equivalence. (\ldots{}) \hypertarget{InSimplicialSets}{}\paragraph*{{In simplicial sets}}\label{InSimplicialSets} We specialize the \hyperlink{InCategoricalSemantics}{general discussion} above to the realization in $\mathcal{C} =$ [[sSet]], equipped with the standard [[model structure on simplicial sets]]. For $E \to B$ any fibration ([[Kan fibration]]) between fibrant objects ([[Kan complexes]]), consider first the simplicial set \begin{displaymath} [E \times B , B \times E]_{B \times B} \in sSet/_{B \times B} \end{displaymath} defined as the [[internal hom]] in the [[slice category]] $sSet/_{B \times B}$. Notice that the vertices of this simplicial set over a fixed pair $(b_1, b_2) : * \to B \times B$ of vertices in $B$ form the set of morphisms $E_{b_1} \to E_{b_2}$ between the [[fibers]] in $sSet$. This is because -- by the defining property of the [[internal hom]] in the [[slice category|slice]] and using that [[products]] in $sSet/_{B \times B}$ are [[pullbacks]] in $sSet$ -- the horizontal morphisms of simplcial sets in \begin{displaymath} \itexarray{ * &&\to&& [E \times B, B \times E]_{B \times B} \\ & {}_{\mathllap{(b_1,b_2)}}\searrow && \swarrow \\ && B \times B } \end{displaymath} correspond bijectively to the horizontal morphisms in \begin{displaymath} \itexarray{ E_{b_1} \times \{b_2\} &&\to&& \{b_1\} \times E_{b_2} \\ & \searrow && \swarrow \\ && B \times B } \end{displaymath} in $sSet$, which are precisely morphisms $E_{b_1} \to E_{b_2}$. Let then \begin{displaymath} Eq(E) \hookrightarrow [E \times B, B \times E]_{B \times B} \in sSet/_{B \times B} \end{displaymath} be the full sub-simplicial set on those vertices that correspond to [[weak equivalences]] (([[weak homotopy equivalence|weak]]) [[homotopy equivalences]]). By a similar consideration, one sees that the [[diagonal]] morphism $\Delta_B : B \to B \times B$ in $sSet$, regarded as an object $B \in sSet/_{B \times B}$, comes with a canonical morphism \begin{displaymath} B \to Eq(E) \,. \end{displaymath} The fibration $E \to B$ is univalent, precisely when this morphism is a weak equivalence. This appears originally as \hyperlink{UnivalentFoundationsProject}{Voevodsky, def. 3.4} \hypertarget{InSimplicialPresheaves}{}\paragraph*{{In simplicial presheaves}}\label{InSimplicialPresheaves} (\ldots{}) See (\hyperlink{Shulman12}{Shulman 12}, \href{UF13}{UF 13}) (\ldots{}) \hypertarget{properties}{}\subsection*{{Properties}}\label{properties} \hypertarget{relation_to_function_extensionality}{}\subsubsection*{{Relation to function extensionality}}\label{relation_to_function_extensionality} The univalence axiom implies [[function extensionality]]. A commented version of a formal proof of this fact can be found in (\hyperlink{BauerLumsdaine}{Bauer-Lumsdaine}). \hypertarget{WeakerEquivalentForms}{}\subsubsection*{{Weaker equivalent forms}}\label{WeakerEquivalentForms} The univalence axiom proper says that the canonical map $coe:(X=Y)\to (X\simeq Y)$ is an equivalence. However, there are several seemingly-weaker (and therefore often easier to verify) statements that are equivalent to this, such as: \begin{enumerate}% \item For any type $X$, the type $\sum_{Y:U} (X\simeq Y)$ is [[contractible type|contractible]]. This follows since then the map on total spaces from $\sum_{Y:U} (X=Y)$ to $\sum_{Y:U} (X\simeq Y)$ induced by $coe$ is an equivalence, hence a fiberwise equivalence $(X=Y) \simeq (X\simeq Y)$. \item For any $X,Y:U$ we have a map $ua:(X\simeq Y) \to (X=Y)$ such that $coe(ua(f)) = f$. This exhibits $X\simeq Y$ as a retract of $X=Y$, hence $\sum_{Y:U} (X\simeq Y)$ as a retract of the contractible type $\sum_{Y:U} (X=Y)$, so it is contractible. This was observed by \href{https://groups.google.com/forum/#!msg/homotopytypetheory/j2KBIvDw53s/YTDK4D0NFQAJ}{Dan Licata}. \item Ian Orton and Andrew Pitts showed \href{http://types2017.elte.hu/proc.pdf#page=93}{here} that assuming function extensionality, this can be further simplified to the following special cases: \begin{itemize}% \item $unit : A = \sum_{a:A} 1$ \item $flip : (\sum_{a:A} \sum_{b:B} C(a,b)) = (\sum_{b:B} \sum_{a:A} C(a,b))$ \item $contract: IsContr(A) \to (A=1)$ \item $unit_\beta : coe(unit(a)) = (a,\star)$ \item $flip_\beta : coe(flip(a,b,c)) = (b,a,c)$. \end{itemize} The proof constructs $ua(f): A=B$ (for $f:A\simeq B$) as the composite \begin{displaymath} A \overset{unit}{=} \sum_{a:A} 1 \overset{contract}{=} \sum_{a:A} \sum_{b:B} f a=b \overset{flip}{=} \sum_{b:B} \sum_{a:A} f a = b \overset{contract}{=} \sum_{b:B} 1 \overset{unit}{=} B \end{displaymath} and uses $unit_\beta$ and $flip_\beta$ to compute that $coe(ua(f))(a) = f(a)$, hence by function extensionality $coe(ua(f)) = f$. \end{enumerate} \hypertarget{Canonicity}{}\subsubsection*{{Canonicity}}\label{Canonicity} It is currently open whether the univalence axiom enjoys [[canonicity]] in general, but for the special case of [[1-truncated]] homotopy types ([[groupoids]]) (and two nested univalent [[universes]] and [[function extensionality]]), a ``homotopical'' sort of [[canonicity]] has been shown in (\hyperlink{Shulman12}{Shulman 12, section 13}. Thus, in univalent homotopy 1-type theory with two universes, every [[term]] of [[type]] of the [[natural numbers]] is [[propositional equality|propositionally equal]] to a [[numeral]]. The construction in (\hyperlink{Shulman12}{Shulman 12, section 13}) uses [[Artin gluing]] of a suitable [[type-theoretic model category|type-theoretic fibration category]] with the [[category]] [[Set]] and [[Grpd]], respectively, effectively inducing canonicity from these categories. By (\hyperlink{Shulman12}{Shulman 12, remark 13.13}) for this construction to generalize to untruncated univalent type theory, one seems to need a sufficiently strict [[global sections]] functor with values in some model for [[infinity-groupoids]]. A proof of the full result has been announced by [[Christian Sattler]] and [[Krzysztof Kapulkin]] (\hyperlink{Sattler19}{Sattler 19}). Notice that this sort of [[canonicity]] does not yet imply [[computational effectiveness]], which would require also an [[algorithm]] to extract that [[numeral]] from the given [[term]]. There may be such an algorithm, but so far attempts to extract one from the proof (or to give a [[constructive mathematics|constructive]] version of the [[proof]], which would imply the existence of an algorithm) have not succeeded. It is also a \emph{[[propositional equality|propositional]]} canonicity, as opposed to the [[judgmental equality|judgmental]] canonicity which many traditional [[type theories]] enjoy. Another approach to canonicity for 1-truncated univalence can be found in (\hyperlink{HarperLicata}{Harper-Licata}), which involves modifying the type theory by adding more [[judgmental equalities]], resulting in a judgmental canonicity. However, no [[algorithm]] for computing canonical forms has yet been given for this approach either. Canonicity has been proved for [[cubical type theory]]. One might also try to construct the Hoffman-Streicher groupoid model in a constructive framework; Awodey and Bauer have done some work in this direction with an [[predicative mathematics|impredicative]] [[universe]] of [[h-sets]]. \hypertarget{related_concepts}{}\subsection*{{Related concepts}}\label{related_concepts} \begin{itemize}% \item Univalence is closely related to the ``completeness'' condition in the theory of [[Segal spaces]]/[[semi-Segal spaces]]. See \emph{[[complete Segal space]]}/\_[[complete semi-Segal space]]\_. \item [[propositional extensionality]] \item contrary to univalence is the [[axiom UIP]] \end{itemize} \hypertarget{References}{}\subsection*{{References}}\label{References} Perhaps the earliest occurrence of the univalence axiom is in section 5.4 of \begin{itemize}% \item [[Martin Hofmann]] and [[Thomas Streicher]], \emph{The groupoid interpretation of type theory} (1996) \end{itemize} under the name ``universe extensionality''. They formulate almost the modern univalence axiom; the only difference is the lack of a coherent definition of equivalence. The univalence axiom in its modern form was introduced and promoted by Vladimir Voevodsky around 2005. (?) \begin{itemize}% \item [[Vladimir Voevodsky]], \emph{Univalent Foundations Project} (\href{http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations_files/univalent_foundations_project.pdf}{pdf}) \end{itemize} A quick survey is for instance in \begin{itemize}% \item [[Peter Aczel]], \emph{On Voevodsky's univalence axiom} (\href{http://www.cs.man.ac.uk/~petera/Recent-Slides/Edinburgh-2011-slides_pap.pdf}{pdf}) \end{itemize} An exposition is at \begin{itemize}% \item [[Mike Shulman]], \emph{Homotopy type theory, IV} (\href{http://golem.ph.utexas.edu/category/2011/04/homotopy_type_theory_iv.html}{blog post}) \end{itemize} An accessible account of Voevodsky's proof that the universal [[Kan fibration]] in [[simplicial sets]] is univalent is at \begin{itemize}% \item [[Chris Kapulkin]], [[Peter LeFanu Lumsdaine]], [[Vladimir Voevodsky]], \emph{Univalence in simplicial sets}, \href{http://arxiv.org/abs/1203.2553}{arXiv} \end{itemize} A quick elegant proof of the [[object classifier]]/universal [[associated infinity-bundle]] in simplicial sets/$\infty$-groupoids is in \begin{itemize}% \item [[Ieke Moerdijk]] (notes by Chris Kapulkin), \emph{Fiber bundles and univalence} (\href{http://www-home.math.uwo.ca/~kkapulki/notes/fiber_bundles_univalence.pdf}{pdf}) \end{itemize} See also \begin{itemize}% \item [[Colin McLarty]], \emph{A univalent universe in finite order arithmetic} (\href{http://arxiv.org/abs/1412.6714}{arXiv:1412.6714}) \end{itemize} The [[HoTT]]-[[Coq]] code is at \begin{itemize}% \item \emph{\href{https://github.com/HoTT/HoTT/blob/master/theories/Types/Universe.v}{HoTT/HoTT theories/Types/Universe.v}} \item \emph{\href{https://github.com/HoTT/HoTT/blob/master/theories/UnivalenceAxiom.v}{HoTT/HoTT theories/UnivalenceAxiom.v}} \end{itemize} A guided walk through the formal proof that univalence implies [[functional extensionality]] is at \begin{itemize}% \item [[Andrej Bauer]], [[Peter LeFanu Lumsdaine]], \emph{[[Oberwolfach HoTT-Coq tutorial]]} \end{itemize} A discussion of univalence in categories of [[diagrams]] over an [[inverse category]] with values in a category for which univalence is already established is discussed in \begin{itemize}% \item [[Michael Shulman]], \emph{Univalence for inverse diagrams, oplax limits, and gluing, and homotopy canonicity} (\href{http://arxiv.org/abs/1203.3253}{arXiv:1203.3253}) \end{itemize} This discusses [[canonicity]] of univalence in its section 13. Another approach to showing canonicity is (via [[cubical sets]]) in \begin{itemize}% \item [[Thierry Coquand]], Simon Huber, \emph{A model of type theory in cubical sets}, 2013 (\href{http://www.cse.chalmers.se/~coquand/mod1.pdf}{pdf}, \href{https://github.com/simhu/cubical}{Haskell code}, \href{https://groups.google.com/forum/#!topic/homotopytypetheory/GmXKEArD3HY}{discussion}) \end{itemize} A proof of canonicity is presented in the talk \begin{itemize}% \item [[Christian Sattler]], \emph{Homotopy Canonicity}, (\href{http://www.ii.uib.no/~bezem/abstracts/TYPES_2019_paper_110}{abstract}) \end{itemize} On the issue of strict pullback of the univalent universe see \begin{itemize}% \item Univalent Foundations Mailing List, \emph{\href{https://groups.google.com/d/msg/univalent-foundations/Glo7NgNvhJA/4j9SewiFvQ0J}{Quotients}}, March 2013 \end{itemize} The computational interpretation of univalence / [[canonicity]] is discussed in \begin{itemize}% \item [[Dan Licata]], [[Robert Harper]], \emph{Computing with Univalence} (2012) (\href{http://4wft.fmf.uni-lj.si/wp-content/uploads/2012/04/Licata.pdf}{pdf}) \item [[Robert Harper]], [[Daniel Licata]], \emph{Canonicity for 2-dimensional type theory} (2011) (\href{http://www.cs.cmu.edu/~rwh/papers/2dtt-can/paper.pdf}{pdf}) \end{itemize} \begin{itemize}% \item [[Daniel Licata]] \emph{The computational interpretation of HoTT (in 2D)}, talk at [[UF-IAS-2012]] (\href{http://video.ias.edu/stream&ref=1674}{video}) \item Simon Huber (with [[Thierry Coquand]]), \emph{Towards a computational justification of the Axiom of Univalence} , talk at \emph{TYPES 2011} (\href{http://www.cse.chalmers.se/~simonhu/slides/types11.pdf}{pdf}) \item Bruno Barras, [[Thierry Coquand]], Simon Huber, \emph{A Generalization of Takeuti-Gandy Interpretation} (\href{http://uf-ias-2012.wikispaces.com/file/view/semi.pdf}{pdf}) \end{itemize} and realized in [[cubical type theory]] in \begin{itemize}% \item [[Thierry Coquand]] (with [[Marc Bezem]] and [[Simon Huber]]), \emph{Computational content of the Axiom of Univalence}, September 2013 (\href{http://www.humboldt-kolleg.iam.unibe.ch/talks/Coquand.pdf}{pdf}) \item [[Cyril Cohen]], [[Thierry Coquand]], [[Simon Huber]], [[Anders Mörtberg]], \emph{Cubical Type Theory: a constructive interpretation of the univalence axiom} (\href{https://hal.inria.fr/hal-01378906/document}{pdf}) \item [[Marc Bezem]], [[Thierry Coquand]], [[Simon Huber]], \emph{The univalence axiom in cubical sets} (\href{https://arxiv.org/abs/1710.10941}{arXiv:1710.10941}) \end{itemize} A study of the [[semantics|semantic]] side of univalence in [[(infinity,1)-toposes]], as well as further cases of [[locally cartesian closed (infinity,1)-categories]] is in \begin{itemize}% \item [[David Gepner]], [[Joachim Kock]], \emph{Univalence in locally cartesian closed infinity-categories} (\href{http://arxiv.org/abs/1208.1749}{arXiv:1208.1749}) \end{itemize} This does not yet show that the univalence axiom in its usual form holds in the internal type theory of [[(infinity,1)-toposes]], however, due to the lack of a (known) sufficiently strict model for the object classifier. (But it works with Tarskian [[type universes]], see there). Constructions of such a model in some very special cases are in \hyperlink{Shulman12}{Shulman12} above, and also in \begin{itemize}% \item [[Michael Shulman]], \emph{The univalence axiom for elegant Reedy presheaves}, \href{http://arxiv.org/abs/1203.3253}{arXiv:1307.6248}. \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} Finally, full 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} For more references see \emph{[[homotopy type theory]]}. [[!redirects univalence]] [[!redirects univalent foundations]] \end{document}