\documentclass[11pt]{article}
\usepackage{graphicx}
\usepackage{amscd, amssymb}

\textwidth = 6.5 in
\textheight = 9 in
\oddsidemargin = 0.0 in
\evensidemargin = 0.0 in
\topmargin = 0.0 in
\headheight = 0.0 in
\headsep = 0.0 in
\parskip = 0.2in
\parindent = 0.0in

\renewcommand{\thesubsection}{\arabic{subsection}}
%
%
\newenvironment{eq}{\begin{equation}}{\end{equation}}
%
\newenvironment{proof}{{\bf Proof}:}{\vskip 5mm }
\newenvironment{rem}{{\bf Remark}:}{\vskip 5mm }
\newenvironment{remarks}{{\bf Remarks}:\begin{enumerate}}{\end{enumerate}}
\newenvironment{examples}{{\bf Examples}:\begin{enumerate}}{\end{enumerate}}  
%
\newtheorem{proposition}{Proposition}
\newtheorem{lemma}[proposition]{Lemma}
\newtheorem{definition}[proposition]{Definition}
\newtheorem{theorem}[proposition]{Theorem}
\newtheorem{cor}[proposition]{Corollary}
\newtheorem{conjecture}{Conjecture}
\newtheorem{pretheorem}[proposition]{Pretheorem}
\newtheorem{hypothesis}[proposition]{Hypothesis}
\newtheorem{example}[proposition]{Example}
\newtheorem{remark}[proposition]{Remark}
\newtheorem{ex}[proposition]{Exercise}
\newtheorem{cond}[proposition]{Conditions}
\newtheorem{cons}[proposition]{Construction}
%
%
%\newcommand{\C}[4]{\left[\begin{array}{rcl}&#1\\#3&\dw\dw&#4\\&#2\end{array}\right]}
%\newcommand{\llabel}[1]{\label{#1}[{\bf #1}]}
\newcommand{\llabel}[1]{\label{#1}}
\newcommand{\comment}[1]{}
\newcommand{\sr}{\rightarrow}
\newcommand{\lr}{\longrightarrow}
\newcommand{\xr}{\xrightarrow}
\newcommand{\dw}{\downarrow}
\newcommand{\bdl}{\bar{\Delta}}
\newcommand{\zz}{{\bf Z\rm}}
\newcommand{\zq}{{\bf Z}_{qfh}}
\newcommand{\nn}{{\bf N\rm}}
\newcommand{\qq}{{\bf Q\rm}}
\newcommand{\nq}{{\bf N}_{qfh}}
\newcommand{\oo}{\otimes}
\newcommand{\uu}{\underline}
\newcommand{\ih}{\uu{Hom}}
\newcommand{\af}{{\bf A}^1}
\newcommand{\wt}{\widetilde}
\newcommand{\gm}{{\bf G}_m}
\newcommand{\dsr}{\stackrel{\sr}{\scriptstyle\sr}}
\newcommand{\PP}{$P_{\infty}$}
\newcommand{\tp}{\tilde{D}}
\newcommand{\HH}{$H_{\infty}$}
\newcommand{\ii}{\stackrel{\scriptstyle\sim}{\sr}}
\newcommand{\BB}{_{\bullet}}
\newcommand{\D}{\Delta}
\newcommand{\colim}{{\rm co}\hspace{-1mm}\lim}
\newcommand{\cf}{{\it cf} }
\newcommand{\msf}{\mathsf }
\newcommand{\mcal}{\mathcal }
\newcommand{\ep}{\epsilon}
\newcommand{\tl}{\widetilde}
\newcommand{\ub}{\mbox{\rotatebox{90}{$\in$}}}
%
\newcommand{\piece}{\vskip 3mm\noindent\refstepcounter{proposition}{\bf
\theproposition}\hspace{2mm}}
\newcommand{\subpiece}{\vskip 3mm\noindent\refstepcounter{equation}{\bf\theequation}\hspace{2mm}}{\vskip
3mm}

\begin{document}
%
\begin{center}
{\bf\Large A very short note on homotopy $\lambda$-calculus}

{\bf Vladimir Voevodsky}

{October 2, 2006}  
\end{center}
%
%
%\tableofcontents
%
The homotopy $\lambda$-calculus is a hypothetical (at the moment) type system. To some extent one may say that $H\lambda$ is an attempt to bridge the gap between the "classical" type systems such as the ones of PVS or HOL Light and polymorphic type systems such as the one of $Coq$. The main problem with the polymorphic type systems lies in the properties of the equality types. As soon as we have a universe $U$ of which $Prop$ is a member we are in trouble. In the Boolean case, $Prop$ has an automorphism of order 2 (the negation) and it is clear that this automorphism should correspond to a member of $Eq(U;Prop,Prop)$. However, as far as I understand there is no way to produce such a member in, say, $Coq$. A related problem looks as follows. Suppose $T,T':U$ are two type expressions and there exists an isomorphism $T\sr T'$ (the later notion of course requires the notion of equality for members of $T$ and $T'$). Clearly, any proposition which is true for $T$ should be true for $T'$ i.e. for all functions $P:U\sr Prop$ one should have $P(T)=P(T')$. Again as far as I understand this can not be proved in $Coq$ no matter what notion of equality for members of $T$ and $T'$ we use. 

Here is the general picture as I understand it at the moment. Let us consider the type system $TS$ which is generated by the sequents
%
$$\vdash U_i:U_{i+1}$$
%
(for $i=-1,0,1,\dots$) and the rules:
%
\begin{enumerate}
\item $$\frac{\Gamma\vdash T:U_i}{\Gamma\vdash T:U_{i+1}}\,\,\,\,\,\,\,\,\,\,\frac{\Gamma\vdash T:U_i}{\Gamma\vdash T:Type}$$
\item The usual dependent $\prod$-rules (inside each $U_n$)
\item The usual dependent $\sum$-rules with strong elimination (inside each $U_n$)\footnote{We may also consider systems $TS_X$ where $X$ is any "recursive" partially ordered set such that $U_x$ is defined for any $x\in X$ and the rules are modified accordingly. Already the system $TS_{pt}$ where $pt$ is the one point set seems to be non-trivial.}
\end{enumerate}
%
The system $H\lambda$ is supposed to be an extension of $TS$. In $H\lambda$, $U_{-1}$ becomes the empty type $\emptyset$ and $U_0$ becomes $Prop$. The natural numbers are defined (see (\ref{natnum}) below) in terms of $U_1$. 

Let $CC$  be the contexts category of $TS$. By a model of $TS$ with values in a category $D$, I mean a functor $CC\sr D$ which "preserves the relevant structures".  The main observation is that there is a canonical model $M$ of $TS$ with values in the usual homotopy category $H$ provided that we consider homotopy types based on a sufficiently large universe of sets. To define this model one starts with a not-so-canonical model $N$ of $TS$ with values in the category of spaces (actually simplicial sets, but I will speak of spaces since they provide a more familiar  model for homotopy types) and then sets $M$ to be the composition of $N$ with the projection $Spc\sr H$.  The main properties of $N$ are are follows.
%
\begin{enumerate}
\item By definition $N$ takes a context $\Gamma$ to a space $N(\Gamma)$.
\item A sequent of the form $\Gamma\vdash T:Type$ (where $T$ is an expression) defines a morphism 
%
$$(\Gamma,x:T)\sr \Gamma$$
%
in $CC$. Morphisms of this type go to {\em fibrations} 
%
$$N(\Gamma;T):N(\Gamma,x:T)\sr N(\Gamma),$$
%
\item A sequent of the form $\Gamma\vdash t:T$ (where $T$ and $t$ are expressions) defines a morphism 
%
$$\Gamma\sr (\Gamma,x:T)$$
%
in $CC$. Morphisms of this type go to {\em sections} 
%
$$N(\Gamma;T,t):N(\Gamma)\sr N(\Gamma,x:T)$$
%
of $N(\Gamma;T)$.
\end{enumerate}
%
Given $\Gamma\vdash P:Type$ and $\Gamma, x:P\vdash Q:Type$ we can form $\Gamma\vdash\prod x:P.Q$ and $\Gamma\vdash\sum x:P.Q$. On the model level our data defines two fibrations 
%
$$N(\Gamma,x:P,y:Q)\stackrel{q}{\sr} N(\Gamma,x:P)\stackrel{p}{\sr} N(\Gamma)$$
%
The fibration 
%
$$N(\Gamma,z:\prod x:P.Q)\sr N(\Gamma)$$
%
is the "$p_*(q)$". Its fiber over $x\in N(\Gamma)$ is the space of sections (continuous ones!) of the fiber of $q$ over $x$.

The fibration 
%
$$N(\Gamma,z:\sum x:P.Q)\sr N(\Gamma)$$
%
is the "$p_!(q)$". It is simply the composition of $p$ and $q$. The meaning of term constructors associated with $\sum$ and $\prod$ is the obvious one. If we took a model with values in $Sets$ where all maps are fibrations we would get the usual rules for interpretation of $\sum$ and $\prod$ but formulated in a slightly unusual way.

The rigorous description of the value of $N$ on $U_n$'s is complicated. Up to homotopy equivalence, the space $N(U_n)$ is the nerve of the $n$-groupoid of $(n-1)$-groupoids in the ZF with $n-2$ universes (see below for the explicit form in the case $n\le 1$). Alternatively, one may say that $U_n$ is the base of the universal fibration whose fibers are $(n-1)$-types which lie in ZF with $n-2$ universes (so that itself it lies in the ZF with $n-1$ universe. The equivalence of these two points of view follows from the fact that n-groupoids are the same as n-homotopy types. 

In particular, 
%
$$M(U_{-1})=\emptyset$$
%
and  
%
$$M(U_0)=\{0,1\}.$$
%
We further have
%
$$M(U_1)=\coprod_{n\ge 0} BS_n$$
%
where $BS_n$ is the classifying space of the permutation group on $n$ elements ($BS_0$ is empty, $BS_1$ is one point and $BS_2$ is homotopy equivalent to ${\bf R}P^{\infty}=B\zz/2$). In particular, $\pi_0(M(U_1))=\nn$ and one uses $U_1$ to define the type of natural numbers in $H\lambda$. As far as I understand at the moment $M(U_2)$ is $\coprod_{X\in u_2} BAut(X)$ where $u_2$ is the set of equivalence classes of all groupoids with sets of morphisms and objects being $ZF$-sets. Starting with $U_2$ one needs $ZF$ with universes in order for the model to be defined.  The model of $U_3$ is the nerve of the 3-groupoid of 2-groupoids in ZF with one universe. 

Of course there are many other models of $TS$ in $H$. To define a model 

This model is very "incomplete" in the sense that there are many type expressions $T$  such that $M(T)$ is non-empty while $T$ has no terms in $TS$. This is of course unavoidable because of the Goedel's theorem. However, some of these incompletenesses are of a special kind. For example $M(U_{-1})=\emptyset$ hence we may add the empty type rule
%
$$\frac{\Gamma\vdash c:U_{-1}\,\,\,\,\Gamma\vdash T:Type}{\Gamma\vdash \iota(c,T):T}$$
%
which expresses the fact that if the empty type is inhabited in a context then any other type is. It does not look provable in $TS$.

Other examples of such rules involve the equality types. Given a valid type expression $T:U_n$ and two term expressions $t1,t2:T$ we get on the level of models a space $X=M(T)$ (up to homotopy) and two points $x1,x2\in X$. One of the most important observations concerning the picture outlined so far is that it is possible to define equality (equivalence) types $Eq(T;t1,t2)$ in $TS$  such that the model of $Eq(T;t1,t2)$ is (homotopy equivalent to) the space $P(X;x1,x2)$ of paths from $x1$ to $x2$ in $X$. 

The definition proceeds in the following steps:
%
%
\begin{description}
\item[Define the contractibility on the level of $TS$.] 
Set 
%
$$true=(U_{-1}\sr U_{-1}):U_0$$
$$false=U_{-1}:U_0.$$
%
For $T,T':U_0$ set 
%
$$Equiv(T,T')=(T\sr T')\times (T'\sr T).$$
%
For $T:U_n$ set 
%
$$Contr(T)=\prod F:U_n\sr U_0.Equiv(F(T),F(true))$$
%
then $M(Contr(T))\ne \emptyset$ iff $M(T)$ belongs to the same connected component of $M(U_n)$ as $M(true)$ i.e. if $M(T)$ is a contractible space.  In that case $M(Contr(T))$ is itself contractible. 
%
\item[Define representable functors on the level of $TS$.] Suppose $T:U_n$ is a type (expression). I want to think of its model $X=M(T)$ as of the nerve of some $n$-groupoid in $U_n$. The members of $T$ correspond to objects. For $T=U_n$ we get the groupoid of all groupoids. Functions $T\sr U_n$ correspond to functors from $T$ to the groupoid of all groupoids. Among these functors there are representable ones i.e. we have the homotopy type $Rep(T)$ which maps to $T\sr U_n$. For $F:T\sr U_n$ set
%
$$rep(F)=Contr(\sum t:T.F(T)).$$
%
One verifies that on the level of models $rep(F)\ne \emptyset$ iff $F$ is representable. Set
%
$$Rep(T)=\sum F:T\sr U_n.rep(F).$$
%
then the model of $Rep(T)$ is the space of representable functors on $T$. By abuse of notation I will write $F(t):U_n$ instead of the formal $(\pi F)(t)$ for $F:Rep(T)$ and $t:T$. 
%
\item[Define the equality types.] For $T:U_n$ and $T1,t2:T$ one sets:
%
$$Eq(T;t1,t2)=\prod F:Rep(T).F(t1)\sr F(t2)$$
%
where I write $F(t)$ for $F:Rep(T)$ instead of the correct but long $(\pi F)(t)$.
\end{description}
%
\begin{theorem}
\llabel{main1}
There is a homotopy equivalence
%
$$M(Eq(T;t1,t2))=P(M(T);M(t1),M(t2)).$$
\end{theorem}
%
Once the equality types (path spaces) are defined many other constructions familiar on the model level can be formulated on the level of the type system. The first thing to define is the {\em level} "filtration" on type expressions or, equivalently on the types $U_n$. The model of $U_n$ has a natural filtration by subspaces $U_{n,k}$, $k=0,\dots,n$ where $U_{n,k}$ is (the nerve of) the $k$-groupoid of $(k-1)$-groupoids in the universe $U_n$. In particular $U_{n,1}$ is the (nerve of) the usual groupoid of sets in $U_n$ and their isomorphisms. We define a $(-1)$-groupoid as a set where any two elements are equal i.e. one of the two sets $\emptyset$ and $pt$. Hence for any $n\ge 0$ the model of $U_{n,0}$ is the two point set $\{0,1\}=\{true,false\}$.  
%
$$
\begin{CD}
U_{0,0} @= U_{1,0} @=U_{2,0} @= U_{3,0} @= \dots\\
@. @VVV @VVV @VVV\\
@. U_{1,1} @>>> U_{2,1} @>>> U_{3,1} @>>> \dots\\
@. @. @VVV @VVV\\
@. @. U_{2,2} @>>> U_{3,2} @>>> \dots\\
@. @. @. @VVV\\
@. @. @.  U_{3,3} @>>> \dots\\
\end{CD}
$$
%
All the arrows are inclusions with the image being a disjoint union of some of the connected components of the target and the usual arguments a-la Russell's paradox imply that except for the ones marked as equalities the arrows are proper inclusions e.g. $U_{2,1}$ (which is responsible for sets in $U_2$) is strictly larger than $U_{1,1}$ (which is responsible for sets in $U_1$) etc. 

To get $U_{n,k}$'s as type expressions we first define type expressions $Lv_k(T):U_0$ for $T:U_n$ which are "indicator functions" for $U_{n,k}$ setting:
%
$$Lv_{-1}(T)=Contr(T)$$
%
and for $k\ge 0$
%
$$Lv_{k}(T)=\prod t1:T.\prod t2:T.Lv_{k-1}(Eq(T;t1,t2)).$$
%
Then
%
$$U_{n,k}=\sum T:U_n.Lv_k(T).$$
%
One verifies easily that this definition is consistent with the model level definition given above.  We will also use the following notations. For $F:T'\sr T$ and $t:T$ set
%
$$Hfiber(F,t)=\sum t':T'.Eq(T;t,F(t'))$$
%
one verifies easily that the model of $Hfiber$ is the homotopy fiber of $F$ over $t$. Set further
%
$$isheq(F)=\prod t:T.Contr(hfiber(F,t)).$$
%
This is a truth value and the model of $isheq(f)$ is $true$ iff the model of $f$ is a homotopy equivalence. Set further
%
$$Heq(T',T)=\sum F:T'\sr T.isheq(F)$$
%
then $M(Heq(T',T))$ is the space of homotopy equivalences from $T'$ to $T$. 
%
For a type expression $T$ set:
%
$$\Pi_{-1}(T)=(T\sr U_{-1})\sr U_{-1}$$
%
it is a truth value and on the model level $\Pi_{-1}(T)=true$ iff $T$ is not empty. For $F:T'\sr T$ set
%
$$Im(F)=\sum t:T.\Pi_{-1}(Hfiber(F,t)).$$
%
The model of $Im(F)$ is the union of connected components of $T$ whose pre-image under $F$ is non-empty. Set
%
$$ev(T',T)=\lambda t:T.\lambda F:T'\sr T.F(t):T'\sr ((T'\sr T)\sr T)$$
%
$$\Pi_0(T)=Im(ev(T,U_0)).$$
%
The model of $\Pi_0(T)$ is the set of connected components of $T$. 

We can now give more examples of things which hold on the model level but (probably) can not be proved on  the level of $TS$ or even $TS$ with the empty type rule. 
%
\begin{enumerate}
\item The natural maps $U_{n,0}\sr U_{n+1,0}$ are equivalences on the model level for $n\ge 0$. It seems to be unprovable in $TS$. To fix it  one may add the rule
%
$$\frac{\Gamma\vdash T:Type\,\,\,\,\,\Gamma\vdash a:Lv_0(T)}{\Gamma\vdash T:U_0}.$$
%
Alternatively one can impose stabilization together with the Boolean rule by adding a term constructor 
%
$$\frac{\Gamma\vdash T:Type\,\,\,\,\,\Gamma\vdash a:Lv_0(T)}{\Gamma\vdash boo(T,a):((T\sr \emptyset)\sr\emptyset)\sr T}$$
%
\item Set
%
\begin{eq}
\llabel{natnum}\nn=\Pi_0(U_1).
\end{eq}
%
The model of $\nn$ is of course $\nn$ -- the set of natural numbers. It is not clear however to what extend $\nn$ is a natural numbers object in the sense of type theory.
\item For $T:U_n$ we may consider $T$ also as a member of $U_{n+1}$. Thus we have two definitions of $Rep(T)$ one using $U_n$ and another one using $U_{n+1}$. They should agree i.e. any $F:T\sr U_{n+1}$ such that $rep(F)=true$ should factor through $U_n$. More precisely there are two expressions $Rep_n(T)$ and $Rep_{n+1}(T)$ and it should be possible to construct a function $Rep_{n+1}(F)\sr Rep_n(F)$ which is "inverse" to the obvious one going in the opposite direction.
\item Given $T,T':U_n$ there are two different expressions which both model to the space of equivalences from $T'$ to $T$. One is $Eq(U_n;T',T)$ and another one is  $Heq(T',T)$. 
So we should have an equivalence
%
$$Heq(T',T)\sr Eq(U_n;T',T).$$
%
Again it is unclear how to construct it on the level of the type system.
\end{enumerate}
%
A subtle thing about imposing all these properties on $TS$ is that while they all hold for $M$ it is not clear which ones one may get on the level of $N$. In particular the stabilization of $U_{0,k}$'s does not hold for the version of $N$ which I have been considering. For example $N(U_{0,2})$ is much smaller as a space then $N(U_{0,3})$ since there are many more one point sets in ZF with a universe then there are in "pure" ZF. 

The context category $CH\lambda$ of $H\lambda$ has a structure reminiscent of a Quillen model structure or rather of the structure of a category with fibrations and weak equivalences considered by Baues in "Algebraic Homotopy". The associated homotopy category $HH$ is some sort of a free homotopy category.

Originally, I was considering a different approach to $H\lambda$ where the equality types where introduced as "primitives" along with $\sum$ and $\prod$ and the universes where "defined" but it seems to me now that it is nicer to start with $\sum$, $\prod$ and universes and define the equality types later. What is left from this earlier stage is certain understanding of which properties of/structures on the equality types might be sufficient to ensure that they behave nicely (e.g. that for any $t:T$, $\pi_1(T;t)=\Pi_0(Eq(T;t,t))$ is a group or that there is a long exact sequence of "homotopy groups" associated to a fibration).  

The advantage of $H\lambda$ and its homotopy-theoretic model over the less sophisticated type systems is that it better reflects the way mathematicians envision "types" corresponding to mathematical structures of higher level. For example if we fix the size of the universe $n$ and write in the usual way the type expression for, say, the type $Gr(U_n)$ of groups in $U_n$ then the model of $Gr(U_n)$ will be (the nerve of) the groupoid of groups in the universe $U_n$ and their isomorphisms. Similarly, if we write down the definition of a category in a proper way then the model of $Cat(U_n)$ will be (the nerve of) the 2-groupoid of categories in $U_n$, their equivalences and natural isomorphisms between equivalences. Moreover, any construction on categories described in the language of $H\lambda$ is automatically "invariant" under equivalences of categories. E.g. any function we can describe in $H\lambda$ from $Cat(U_n)$ to $Gr(U_n)$ will on the model level correspond to a construction which produces a group from a category which maps equivalences between categories to isomorphisms between the corresponding groups. In the usual type systems we can do something like that for types of "level 1"  i.e. sets with structures but not for higher levels (e.g. categories). 

At the moment much of what I said above is at the level of conjectures. Even the definition of the model of $TS$ in the homotopy category is non-trivial. Similarly, the definition of equality types in terms of universes is rather involved and I am not sure which of the properties of these types have to be imposed so that the rest will follow.
\end{document}   