michael/type-theory
2
0
Fork 0
Code Issues 21 Pull requests Projects 1 Releases 1 Packages Wiki Activity Actions

add CCHM

Browse source
This commit is contained in:
Michael Zhang 2024-06-03 00:10:40 -04:00
parent d9b9f37ee2
commit ea0da820e3
15 changed files with 4564 additions and 83 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
.gitignore vendored
View file

@ -1,2 +1,3 @@
*.agdai
.DS_Store
.DS_Store
node_modules

13
aux/preprocessGraph.ts Normal file
View file

@ -0,0 +1,13 @@
if (Bun.argv.length > 1) {
if (Bun.argv[2] === "supports") {
process.exit(0);
}
}
const doc = await Bun.stdin.json();
// Bun.write("book.json", JSON.stringify(doc));
// TODO: Generate some kind of graph of pages?
console.log(JSON.stringify(doc));

BIN
bun.lockb Executable file
View file

Binary file not shown.

3
html/book.toml
View file

@ -8,7 +8,8 @@ title = "Research"
[preprocessor.katex]
macros = "./macros.txt"
# [preprocessor.pagetoc]
[preprocessor.graph]
command = "bun aux/preprocessGraph.ts"
[preprocessor.chapter-zero]
levels = [0]

10
package.json Normal file
View file

@ -0,0 +1,10 @@
{
"name": "type-theory",
"type": "module",
"devDependencies": {
"@types/bun": "latest"
},
"peerDependencies": {
"typescript": "^5.0.0"
}
}

552
resources/CCHM/appendix.tex vendored Normal file
View file

@ -0,0 +1,552 @@
\section{Details of composition for
glueing}\label{appendix:composition-glueing}
We build the element~$\Gamma \der b_1 = \comp^i~B~[\psi\mapsto
b]~b_0:(\Glue~[\varphi\mapsto(T,\myeq{})]~A)(i1)$ as the element
$\glue~[\varphi(i1) \mapsto t_1]~a_1$ where
%
\begin{align*}
\Gamma,\varphi(i1) \der & \; t_1 : T(i1)[\psi \mapsto b(i1)]\\
\Gamma \der & \; a_1 : A(i1)[\varphi(i1) \mapsto \myeq{}(i1) \; t_1,\psi \mapsto (\ugl~b)(i1)]
\end{align*}
As intermediate steps, we gradually build elements that satisfy more
and more of the equations that the final elements $t_1$ and $a_1$
should satisfy. The construction of these is given in five steps.
Before explaining how we can define them and why they are well
defined, we illustrate the construction in \fig{fig:compglue},
with $\psi = (j=1)$ and $\varphi = (i=0) \vee (j=1)\vee (i=1)$.
We pose $\delta = \forall i.\varphi$ (cf.\ \sect{sec:pathtypes}), so
that we have that~$\delta$ is independent from~$i$, and in our example
$\delta = (j = 1)$ and it represents the right-hand side of the
picture.
\begin{enumerate}
\item The element $a'_1:A(i1)$ is a first approximation of~$a_1$, but
$a'_1$ is not necessarily in the image of~$\myeq{}(i1)$
in~$\Gamma,\varphi(i1)$;
\item the partial element $\inctxt{\delta}{t'_1:T(i1)}$, which is a
partial final result for~$\inctxt{\varphi(i1)}{t_1}$;
\item the partial path $\inctxt{\delta}{\omega}$, between~$a'_1$ and
the image of~$t'_1$;
\item both the final element $\inctxt{\varphi(i1)}{t_1}$ and a path
$\inctxt{\varphi(i1)}{\alpha}$ between~$a'_1$ and
$\myeq{}(i1) \; t_1$;
\item finally, we build $a_1$ from~$a'_1$ and~$\alpha$.
\end{enumerate}
%
\begin{figure}[!h]
\centering
$$
\begin{tikzpicture}
\coordinate (A00) at (0,0);
\coordinate (A10) at ++ (3,0) ;
\coordinate (A'11) at ++ (3,2) ;
\coordinate (A'01) at ++ (0,2) ;
\coordinate (A01) at ($(A'01) + (0,1.5)$);
\coordinate (A11) at ($(A'11) + (0,1.5)$);
\coordinate (O) at ($(A00) + (-4,1)$);
\draw[fun line] (O) -- node[left] () {$i$} ++(0,1);
\draw[fun line] (O) -- node[below] () {$j$} ++(1,0);
% inner
\begin{pgfonlayer}{background}
\draw [path line] (A00) -- node [above] (a_0) {$\ugl~b_0$}
(A10) -- coordinate (aj1)
(A'11) -- coordinate (midA') (A'01);
\draw [path line] (A01) -- coordinate (midA)
node[above] () {Step 5: $a_1$} (A11);
\draw (midA') node[below] {Step 1: $a'_1$} (A'01);
\end{pgfonlayer}
\draw (aj1) node[right, fill=white] () {$(\ugl~b)(j1)$};
% links
\begin{pgfonlayer}{background}
\draw [fun line, <-] (A00) --
node[left, xshift=-5] (f00) {$f$} ++ (-1,-1) coordinate (T00);
\draw [fun line, <-] (A01) --
node[left, xshift=-5] (f00) {$f$} ++ (-1,1) coordinate (T01);
\draw [fun line, <-] (A10) --
node[left, xshift=-5] (f00) {$f$} ++ (1,-1) coordinate (T10);
\draw [fun line, <-] (A11) --
node[left, xshift=-5] (f00) {$f$} ++ (1,1) coordinate (T11);
\end{pgfonlayer}
\fill (T11) circle [radius=2pt] node [right,xshift=10] () {Step 2:
$\inctxt{\delta}{t'_1}$};
\fill (A11) circle [radius=2pt] node [right,xshift=10,fill=white] ()
{$\inctxt{\delta}{\myeq{}(i1) \; t'_1}$};
% outer
\begin{pgfonlayer}{background}
\draw [path line] (T00) -- node[below] (b_0)
{$\inctxt{\varphi(i0)}{b_0}$}
(T10) -- coordinate (bj1)
(T11) -- node[above] (t_1) {Step 4: $\inctxt{\varphi(i1)}{t_1}$} (T01);
\draw [fun line] (b_0) -- node[left] {$\myeq{}$} (a_0);
\end{pgfonlayer}
\draw (bj1) node[right, fill=white] () {$b(j1)$};
\draw [comp line] (A'11) -- node[right, xshift=10,fill=white] ()
{Step 3: $\inctxt{\delta}{\omega}$ constant on $\psi$} (A11);
% inner top diag edge
% \coordinate (A''01) at ($(A'01) !0.25! (A01)$);
% \draw [path line] (A''01) -- coordinate (midA'')
% node[below,yshift=-5] () {Step 4: $a''_1$} (A11);
\draw [comp line] (midA') --
node[left] () {Step 4': $\inctxt{\varphi(i1)}{\alpha}$} (midA);
\end{tikzpicture}
$$
\caption{Composition for glueing}
\label{fig:compglue}
\end{figure}
We define:
\begin{align*}
% \Gamma,i:\II,\psi,\varphi\der t : T\label{eq:glue-t}\\
% \Gamma,i:\II,\psi\der a = & \; \ugl~ b: A[\varphi\mapsto \myeq{} \; b]%\label{eq:glue-a}
\Gamma,\psi,i:\II \der a = & \; \ugl~ b: A[\varphi\mapsto \myeq{} \; b]%\label{eq:glue-a}
\\
% \Gamma,\varphi(i0)\der t_0 : T(i0)[\psi\mapsto t(i0)]\label{eq:glue-t0}\\
\Gamma\der a_0 = & \; \ugl~ b_0: A(i0)[\varphi(i0)\mapsto \myeq{}(i0) \; b_0,\psi\mapsto a(i0)]%\label{eq:glue-a0}
\end{align*}
\subparagraph*{Step 1} We define~$a'_1$ as the composition of~$a$
and~$\ugl~b_0$, in the direction~$i$, which is well defined since
$\ugl~b_0 = (\ugl~b)(i0)$ over the extent $\psi$
%
\begin{equation}
\label{eq:glue-a'1}
\Gamma \der a_1' = \comp^i~A~[\psi\mapsto~a]~a_0:A(i1)[\psi\mapsto~a(i1)]
\end{equation}
%\[\textrm{which is well defined because}\quad
%\begin{cases}
% \Gamma,i:\II,\psi\der a : A \hfill \textrm{by~(\ref{eq:glue-a})}\\
% \Gamma\der a_0 : A(i0)[\psi\mapsto a(i0)] \hspace{1cm} \textrm{by~(\ref{eq:glue-a0})}
%\end{cases}\]
\subparagraph*{Step 2} We also define~$t'_1$ as the composition of~$b$
and~$b_0$, in the direction~$i$:
%
\begin{equation}
\label{eq:glue-t'1}
\Gamma,\delta\der t_1' = \comp^i~T~[\psi\mapsto~b]~b_0:T(i1)[\psi\mapsto~b(i1)]
\end{equation}
\[\textrm{which is well defined because}\quad
\begin{cases}
\Gamma,\delta,i:\II,\psi\der b : T \hfill
\textrm{by Lemma \ref{admissible}} \\
\Gamma,\delta\der b_0 : T(i0)[\psi\mapsto b(i0)] \hspace{1cm} \textrm{as~%(\ref{eq:glue-t0}) and
$\delta \leqslant \varphi(i0)$}
\end{cases}\]
%
Moreover, since
\[
\begin{cases}
\Gamma,\delta,\psi,i:\II \der a = \myeq{} \; b \hspace{1cm} \textrm{by~%(\ref{eq:glue-a}) and
$\delta \leqslant \varphi$ ~~~~} \\
\Gamma,\delta\der~a_0=\myeq{}(i0)~b_0 \hfill \textrm{by~%(\ref{eq:glue-a0}) and
$\delta \leqslant \varphi(i0)$}
\end{cases}\]
we can re-express~$a'_1$ on the extent $\delta$
%
\[
\Gamma, \delta \der a_1' = \comp^i~A~[\psi\mapsto\myeq{}~b]~\left(\myeq{}(i0)~b_0\right)
\]
%
%Hence, the element~$a'_1$ restricted to the extent $\delta$ is the composition of images by~$\myeq{}$.
\subparagraph*{Step 3} We can hence find a path~$\omega$
connecting~$a'_1$ and~$\myeq{}(i1) \; t'_1$ in~$\Gamma,\delta$
using Lemma~\ref{pres}:
%
\[
\Gamma,\delta \der \omega = \pres{i}~\myeq{}~[\psi\mapsto b]~b_0 :
\left(\Path~A(i1)~a_1'~\left(\myeq{}(i1) \;
t'_1\right)\right)[\psi\mapsto\pabs{j} a(i1)]
\]
%
Picking a fresh name~$j$, we have
%
\begin{equation}
\Gamma,\delta,j:\II\der \omega~j : A(i1)[(j=0)\mapsto
a'_1,(j=1)\mapsto \myeq{}(i1) \; t'_1,\psi\mapsto a(i1)]\label{eq:glue-omega}
\end{equation}
% \subparagraph*{Step 4} We then define~$a''_1$ as the composition
% of~$[\delta \mapsto \omega \; j, \psi \mapsto a(i1)]$ and~$a'_1$, in
% the direction~$j$:
% %
% \[\Gamma\der a''_1 = \comp^j~A(i1)~[\delta\mapsto \omega \; j,~\psi\mapsto
% a(i1)]~a_1' : A(i1)[\delta\mapsto\omega \; 1, \psi\mapsto a(i1)]
% \]
% \[\textrm{which is well defined because}\quad
% \begin{cases}
% \Gamma,j:\II,\delta,\psi\der \omega~j = a(i1)
% \hfill \textrm{by~(\ref{eq:glue-omega})} \\
% \Gamma,j:\II,\delta\der \omega~0 = a'_1
% \hfill \textrm{by~(\ref{eq:glue-omega})} \\
% \Gamma,j:\II,\psi\der a(i1) = a'_1
% \hspace{1cm} \textrm{by~(\ref{eq:glue-a'1})}
% \end{cases}
% \]
% and since $\Gamma,\delta\der\omega~1 = \myeq{}(i1) \; t'_1$,
% because~$\omega$ is a partial path between $a'_1$ and
% $\myeq{}(i1) \; t'_1$, we can re-express the type of~$a''_1$ in the
% following way:
% %
% \begin{equation}
% \Gamma\der a''_1 : A(i1)[\delta\mapsto\myeq{}(i1) \; t'_1,~\psi\mapsto a(i1)]\label{eq:glue-a''1}
% \end{equation}
\subparagraph*{Step 4} Now we define the final element~$t_1$ as the
inverse image of~$a'_1$ by~$\myeq{}(i1)$, together with the
path~$\alpha$ between~$a'_1$ and~$\myeq{}(i1) \; t_1$, in
$\Gamma,\varphi(i1)\der$, using Lemma~\ref{equiv}:
%
\[\Gamma,\varphi(i1)\der(t_1,\alpha) =
\eq~\myeq{}(i1)~[\delta\mapsto~(t'_1,\omega),\psi\mapsto~\left(b(i1),\pabs{j}a'_1\right)]~a_1'\]
\[{\textrm{with}\quad}\begin{cases}
\Gamma,\varphi(i1)\der t_1 :
T(i1)[\delta\mapsto~t'_1,\psi\mapsto~b(i1)] % \label{eq:glue-t1}
\\
\Gamma,\varphi(i1)\der\alpha :
\left(\Path~A(i1)~a'_1~\left(\myeq{}(i1) \; t_1\right)\right)
[\delta\mapsto\omega,\psi\mapsto~\pabs{j} a'_1)]
\end{cases}
\]
These are well defined because the two systems in~$\delta$ and~$\psi$
are compatible:
\[\begin{cases}
\Gamma, \delta, \psi \der t'_1 = b(i1) & \textrm{by~(\ref{eq:glue-t'1})} \\
\Gamma, \delta, \psi \der \omega = \pabs{j}a'_1 &
\textrm{by~(\ref{eq:glue-omega}) and~(\ref{eq:glue-a'1})}
\end{cases}
\]
% %
% \[\begin{cases}
% \Gamma,\varphi(i1),\delta\der a'_1 = \myeq{}(i1) \; t'_1
% \hfill \textrm{by~(\ref{eq:delta-a'1})} \\
% \Gamma,\varphi(i1),\psi\der a'_1 = a(i1) = \myeq{}(i1) \; b(i1)
% \hspace{1cm} \textrm{by~(\ref{eq:glue-a'1}) in~$\Gamma,\psi\der$} %and~(\ref{eq:glue-a}) in~$\Gamma,\varphi\der$}
% \end{cases}\]
%
Picking a fresh name~$j$, we have
%
\begin{equation}
\Gamma,\varphi(i1),j:\II\der \alpha~j : A(i1)[(j=0)\mapsto
a'_1,~(j=1)\mapsto \myeq{}(i1) \; t_1,~\delta\mapsto~a'_1,~\psi\mapsto a(i1)]\label{eq:glue-alpha}
\end{equation}
\subparagraph*{Step 5} Finally, we define~$a_1$ by composition
of~$\alpha$ and~$a'_1$:
%
\[\Gamma\der~a_1:=\comp^j~A(i1)~[\varphi(i1)\mapsto\alpha~j,\psi\mapsto~a(i1)]~a'_1:
A(i1)[\varphi(i1)\mapsto\alpha~1,\psi\mapsto~a(i1)]\]
\[\textrm{which is well defined because}\quad
\begin{cases}
\Gamma,j:\II,\varphi(i1),\psi \der \alpha~j = a(i1)
&\textrm{by~(\ref{eq:glue-alpha})} \\
\Gamma,\varphi(i1)\der \alpha~0 = a'_1
&\textrm{by~(\ref{eq:glue-alpha})} \\
\Gamma,\psi\der a(i1) = a'_1
&\textrm{by~(\ref{eq:glue-a'1})}
\end{cases}
\]
and since $\Gamma,\varphi(i1)\der\alpha~1 = \myeq{}(i1) \; t_1$, we can
re-express the type of~$a_1$ in the following way:
\[
\Gamma\der a_1 : A(i1)[\varphi(i1)\mapsto\myeq{}(i1) \;
t_1,~\psi\mapsto a(i1)]
\]
Which is exactly what we needed to build
$\Gamma\der b_1 := \glue ~[\varphi(i1)\mapsto t_1]~a_1:
B(i1)[\psi\mapsto b(i1)]$.
\medskip
\noindent Finally we check that $b_1 = \comp^i~T~ [\psi\mapsto~b]~b_0$
on $\delta$:
%
\begin{align*}
b_1 &= \glue ~[\varphi(i1)\mapsto t_1]~a_1 &&\textrm{by def.} \\
&=t_1 : T(i1)[\delta\mapsto~t'_1,\psi\mapsto~b(i1)]
&& \textrm{as $\varphi(i1) = 1_\FF$} \\
&=t'_1 && \textrm{as $\delta = 1_\FF$} \\
&= \comp^i~T~[\psi\mapsto~b]~b_0 && \textrm{by def.}
\end{align*}
% \[\begin{array}{llll}
% b_1 & = & \glue ~[\varphi(i1)\mapsto t_1]~a_1 & \hspace{2cm} \textrm{by def.} \\
% & = & t_1 : T(i1)[\delta\mapsto~t'_1,\psi\mapsto~t(i1)] &
% \hspace{2cm} \textrm{as $\varphi(i1) = 1_\FF$} \\
% & = & t'_1 & \hspace{2cm} \textrm{as $\delta = 1_\FF$} \\
% & = & \comp^i~T~[\psi\mapsto~b]~b_0 & \hspace{2cm} \textrm{by def.}
% \end{array}\]
\section{Univalence from glueing}
\label{sec:univ-from-glue}
We also give two alternative proofs of the univalence axiom for
$\Path$ only involving the glue construction.%
\footnote{The proofs of the univalence axiom have all been formally
verified inside the system using the \Haskell{} implementation. We
note that the proof of Theorem~\ref{thm:unglueequiv} can be given
such that it extends $\myeq{}.2$ and hence in
Corollary~\ref{cor:equiv-contr} we do not need the fact that
$\isEquiv~X~A~\myeq{}.1$ is a proposition. For details see:\\
\url{https://github.com/mortberg/cubicaltt/blob/v1.0/examples/univalence.ctt}}
The first is a direct proof of the standard formulation of the
univalence axiom while the second goes through an alternative
formulation as in Corollary~\ref{cor:equiv-contr}.%
\footnote{The second of these proofs is inspired by a proof by Dan Licata from:\\
\url{https://groups.google.com/d/msg/homotopytypetheory/j2KBIvDw53s/YTDK4D0NFQAJ}}
\begin{lemma}
\label{lem:ua-prel}
For $\Gamma \vdash A : \U$, $\Gamma \vdash B : \U$, and an
equivalence $\Gamma \vdash \myeq : \Equiv~A~B$ we have the following
constructions:
\begin{enumerate}
\item\label{item:uap1} $\Gamma \vdash \eqToPath \myeq :
\Path\, \U\, A\, B$;
\item\label{item:uap2} $\Gamma \vdash \Path \, (A \to B) \,
(\transport^i (\eqToPath \myeq \, i))) \, \myeq.1$ is
inhabited; and
\item\label{item:uap3} if $\myeq = \eq^i (P \, i)$ for $\Gamma
\vdash P : \Path \, \U\, A \, B$, then the following type is
inhabited:
\[
\Gamma \vdash %
\Path \, (\Path \, \U \, A \, B) \, (\eqToPath {(\eq^i (P \, i))})
\, P
\]
\end{enumerate}
\end{lemma}
\begin{proof}
For \eqref{item:uap1} we define
\begin{align}
\label{eq:def-eqToPath}
\eqToPath \myeq = \pabs i {\Glue \, [ (i=0) \mapsto
(A,\myeq), (i=1) \mapsto (B, \eq^k B)] \, B }.
\end{align}
Note that here $\eq^k B$ is an equivalence between $B$ and $B$ (see
\sect{subsec:compU}). For \eqref{item:uap2} we have to closely look
at how the composition was defined for $\Glue$. By unfolding the
definition, we see that the left-hand side of the equality is equal
$\myeq.1$ composed with multiple transports in a constant type;
using filling and functional extensionality, these transports can be
shown to be equal to the identity; for details see the formal proof.
The term for \eqref{item:uap3} is given by:
\begin{align*}
\pabs {j} \pabs {i} \Glue \,[ %
&(i=0) \mapsto (A, \eq^k (P\, k)),\\
&(i=1) \mapsto (B, \eq^k B),\\
&(j=1) \mapsto (P \, i, \eq^k (P (i \lor k)))]\\
&B \qedhere
\end{align*}
\end{proof}
\begin{corollary}[Univalence axiom]
\label{cor:ua}
For the canonical map
\[
\can : (A \, B : \U) \to \Path \,\U\,A\,B \to \Equiv~A~B
\]
we have that $\can \, A \, B$ is an equivalence for
all $A : \U$ and $B : \U$.
\end{corollary}
\begin{proof}[Proof 1]
Let us first show that the canonical map $\can$ is path equal to:
\[
\eq = \lambda A \, B : \U. \, \lambda P : \Path\,\U\,A\,B. \, \eq^i (P\, i)
\]
By function extensionality, it suffices to check this pointwise.
Using path-induction, we may assume that $P$ is reflexivity. In
this case $\can\,A\,A\,\refl{A}$ is the identity equivalence by
definition. Because being an equivalence is a proposition, it thus
suffices that the first component of $\eq^i A$ is propositionally
equal to the identity. By definition, this first component is given
by transport (now in the constant type $A$) which is easily seen to
be the identity using filling (see \sect{sec:kan-filling}).
Thus it suffices to prove that $\eq\,A\,B$ is an equivalence. To do
so it is enough to give an inverse (see Theorems 4.2.3 and 4.2.6 of
\cite{hott-book}). But $\eqToPath$ is a left inverse by
Lemma~\ref{lem:ua-prel}~\eqref{item:uap3}, and a right inverse by
Lemma~\ref{lem:ua-prel}~\eqref{item:uap2} using that being an
equivalence is a proposition.
\end{proof}
%
\begin{proof}[Proof 2]
Points~\eqref{item:uap1} and~\eqref{item:uap2} of
Lemma~\ref{lem:ua-prel} imply that~$\Equiv~A~B$ is a retract
of~$\Path \,\U\,A\,B$. Hence $(X : \U) \times \Equiv~A~X$ is a
retract of $(X : \U) \times \Path\,\U\,A\,X$. But $(X : \U) \times
\Path\,\U\,A\,X$ is contractible, so $(X : \U) \times \Equiv~A~X$ is
also contractible as a retract of a contractible type. As
discussed in~\sect{sec:univalence-axiom} this is an alternative
formulation of the univalence axiom and the rest of this proof
follows as there.
\end{proof}
Note that the first proof uses all three of the points of
Lemma~\ref{lem:ua-prel} while the second proof only uses the first
two. As the second proof only uses the first two points it is possible
to prove it if point~\eqref{item:uap1} is defined as in
Example~\ref{exa:equivtopath} leading to a slightly simpler proof of
point~\eqref{item:uap2}.
\section{Singular cubical sets}\label{sec-singular}
Recall the functor $\CC \to \Top, I \mapsto [0,1]^I$ given
at~\eqref{eq:georeal} in \sect{sec:cubecat}. In particular, the face
maps $(ib) \colon I-i \to I$ (for $b=0_\II$ or $1_\II$) induce the
maps $(ib)\colon [0,1]^{I-i} \to [0, 1]^{I}$ by $i(ib)u = b$ and
$j(ib)u = ju$ if $j\neq i$ is in $I$. If $\psi$ is in $\FF(I)$ and
$u$ in $[0,1]^I$, then $\psi u$ is a truth value.
We assume given a family of idempotent functions
$r_I:[0,1]^I\times [0,1]\rightarrow [0,1]^I\times [0,1]$ such that
\begin{enumerate}
\item $r_I(u,z) = (u,z)$ if{f} $\partial_I u = 1$ or $z = 0$, and
\item for any {\em strict} $f$ in ${\sf Hom}(I,J)$ we have
$r_J(f\times\id)r_I = r_J(f\times\id)$.
\end{enumerate}
\medskip
Such a family can for instance be defined as in the following picture
(``retraction from above center''). If the center has coordinate
$(1/2,2)$, then $r_I(u,z) = r_I(u',z')$ is equivalent to $(2-z')
(-1+2u) = (2-z) (-1+2u')$.
$$
\begin{tikzpicture}[scale=2]
% bottom
\draw [thick,solid] (0,0) --
node [near start,below=-1pt] (DL) {}
node [near end,below=-1pt] (DR) {}
(1,0);
% left and right
\draw [thick,solid] (0,0) --
node [near end,](L) {} (0,1);
\draw [thick,solid] (1,0) -- node (R) {} (1,1);
% top
\draw [dashed] (0,1) -- (1,1);
% rays
\def\raypt{(0.5,1.5)}
\draw[->,>=stealth]\raypt -- (DL);
\draw[->,>=stealth]\raypt -- (DR);
\draw[->,>=stealth]\raypt -- (L);
\draw[->,>=stealth]\raypt -- (R);
\end{tikzpicture}
$$
Property (1) holds for the retraction defined by this picture.
The property (2) can be reformulated as $r_I(u,z) =
r_I(u',z')\rightarrow r_J(f u,z) = r_J(f u',z')$. It also holds
in this case,
since $r_I(u,z) = r_I(u',z')$ is then equivalent to $(2-z') (-1+2u) = (2-z) (-1+2u')$,
which implies $(2-z') (-1+2f u) = (2-z)(-1+2 f u')$ if $f$ is strict.
Using this family, we can define for each $\psi$ in $\FF(I)$ an
idempotent function
\[
r_{\psi}:[0,1]^I\times [0,1]\rightarrow [0,1]^I\times [0,1]
\]
having for fixed-points the element $(u,z)$ such that $\psi u = 1$ or $z = 0$.
This function $r_{\psi}$ is completely characterized by the following properties:
\begin{enumerate}
\item $r_{\psi} = \id$ if $\psi = 1$
\item $r_{\psi} = r_{\psi}r_I$ if $\psi \neq 1$
\item $r_{\psi}(u,z) = (u,z)$ if $z = 0$
\item $r_{\psi}((ib)\times\id) = ((ib)\times\id)r_{\psi(ib)}$
\end{enumerate}
%% \medskip
%% For instance, these functions witness the fact that the following polyhedrons, corresponding
%% respectively to the formula $\psi = ((i=1)\wedge (j=0))\vee (i=0)\vee (j=1)$
%% and $\psi = ((i=0)\vee (i=1))\wedge ((j=0)\vee (j=1))$, are retract of the
%% filled cube on directions $i,j,k$.
%% \[
%% \begin{tikzpicture}[scale=1.5, z=.5cm, rotate around y=5]
%% % bottom
%% \filldraw [thick,draw=black,fill=gray!30] (0,0,0) -- (1,0,0) -- (1,0,1) --
%% (0,0,1) -- cycle;
%% % back
%% \filldraw [thick,draw=black,fill=gray!60] (0,0,1) -- (1,0,1) -- (1,1,1) --
%% (0,1,1) -- cycle;
%% % right
%% \filldraw [thick,draw=black,fill=gray!60] (1,0,0) -- (1,1,0) -- (1,1,1) --
%% (1,0,1) -- cycle;
%% % pins
%% \draw [thick, black] (0,0,0) -- (0,1,0);
%% \draw [thick, black] (1,0,0) -- (1,1,0);
%% % points
%% \draw [thick, fill = black, circle] (0,0,0) circle (0.05);
%% \draw [thick, fill = black, circle] (0,1,0) circle (0.05);
%% % \node[align = center, below]{$\psi$ = (i=0)\vee (j=0)\vee ((i=1)\wedge (j=1))};
%% \end{tikzpicture}
%% \qquad\qquad
%% \begin{tikzpicture}[scale=1.5, z=.5cm, rotate around y=5]
%% % bottom
%% \filldraw [thick,draw=black,fill=gray!30] (0,0,0) -- (1,0,0) -- (1,0,1) --
%% (0,0,1) -- cycle;
%% % back
%% \filldraw [thick,draw=black,fill=gray!60] (0,0,1) -- (1,0,1) -- (1,1,1) --
%% (0,1,1) -- cycle;
%% % left
%% \filldraw [thick,draw=black,fill=gray!50] (0,0,1) --
%% (0,1,1) -- (0,1,0) -- (0,0,0) -- cycle;
%% % right
%% \filldraw [thick,draw=black,fill=gray!80] (1,0,0) -- (1,0,1) --
%% (1,1,1) -- (1,1,0) -- cycle;
%% % back
%% \filldraw [thick,draw=black,fill=gray!90] (0,0,0) -- (1,0,0) -- (1,1,0) --
%% (0,1,0) -- cycle;
%% % points
%% \end{tikzpicture}
%% \]
These properties imply for instance $r_{\partial_I}(u,z) = (u,z)$ if
$\partial_I u = 1$ or $z=0$ and so they imply $r_{\partial_I} = r_I$.
They also imply that $r_{\psi}(u,z) = (u,z)$ if $\psi u = 1$.
\medskip
From these properties, we can prove the uniformity of the family of
functions $r_{\psi}$.
\begin{theorem}
If $f$ is in ${\sf Hom}(I,J)$ and $\psi$ is in $\FF(J)$, then
$r_{\psi}(f\times\id) = (f\times\id)r_{\psi f}$.
\end{theorem}
This is proved by induction on the number of element of $I$ (the
result being clear if $I$ is empty).
A particular case is $r_J(f\times\id) = (f\times\id)r_{\partial_J
f}$. Note that, in general, $\partial_Jf$ is not $\partial_I$.
\medskip
A direct consequence of the previous theorem is the following.
\begin{corollary} The singular cubical set associated to a topological space
has a composition structure.
\end{corollary}
%% Local Variables:
%% mode: latex
%% TeX-master: "main"
%% End:

2940
resources/CCHM/cubicaltt.tex vendored Normal file
View file

File diff suppressed because it is too large Load diff

166
resources/CCHM/macro.tex vendored Normal file
View file

@ -0,0 +1,166 @@
\newcommand{\Haskell}{{\sc Haskell}}
\newcommand{\eg}{{e.g.}}
\newcommand{\ie}{{i.e.}}
\newcommand{\cf}{{cf.}}
\newcommand{\sect}[1]{Section~\ref{#1}}
\newcommand{\fig}[1]{Figure~\ref{#1}}
\renewcommand{\|}{{~\mid~}}
\renewcommand{\:}{{\; : \;}}
\renewcommand{\=}{{~~ = ~~}}
\newcommand{\der}{\vdash}
\newcommand{\emptyctxt}{()}
\newcommand{\inctxt}[2]{#1\der#2}
\newcommand{\inctxtT}[3]{#1\der#2~:#3}
\newcommand{\set}[1]{\{ #1 \}}
% the subst and mod macros
\newcommand{\subst}[2]{(#1/#2)}
%\newcommand{\subst}[2]{(#1=#2)}
\renewcommand{\mod}[1]{\; ({\sf mod.} \; #1)}
\newcommand{\hmapsto}{~}
% generic name for an equivalence (used to be \sigma, now f)
\newcommand\myeq{f}
% path abstraction: <i>
\newcommand{\pabs}[1]{{\langle}#1{\rangle} \; }
% refl
\newcommand{\refl}[1]{{1_{#1}}} % {{\sf refl_{#1}}}
\DeclareMathOperator{\transport}{\mathsf{transp}} % transport as special case of comp
%\DeclareMathOperator{\J}{\mathsf{J}}
\newcommand{\J}{\mathsf{J}}
\DeclareMathOperator{\idrefl}{\mathsf{r}}
\newcommand{\dM}{{\sf dM}}
\newcommand{\II}{\mathbb{I}}
\newcommand{\FF}{\mathbb{F}}
% nat
\newcommand{\NN}{{\sf N}}
\newcommand{\natrec}{{\sf natrec}}
\newcommand{\s}{{\sf s}}
\newcommand{\suc}[1]{\s \; #1}
\newcommand{\0}{{\sf 0}}
\newcommand{\Id}{{\sf Id}}
\newcommand{\ident}{{\sf id}}
\newcommand{\Path}{{\sf Path}}
\newcommand{\Equiv}{{\sf Equiv}}
\newcommand{\isEquiv}{{\sf isEquiv}}
\newcommand{\ext}{{\sf contr}}
\newcommand{\isContr}{{\sf isContr}}
\DeclareMathOperator{\dom}{dom}
\DeclareMathOperator{\cod}{cod}
\def\NN{\hbox{\sf N}}
\def\Type{\hbox{\sf Type}}
\def\Box{\hbox{\sf B}}
\def\PER{\hbox{\sf PER}}
\def\FUN{\Pi}
\def\ELEM{\hbox{\sf El}}
\def\GG{\hbox{\sf G}}
\def\TP{\hbox{\sf TP}}
\def\N0{\hbox{\sf N}_0}
\def\ZERO{\hbox{\sf zero}}
\def\SUCC{\hbox{s}}
%% \newcommand{\app}{\mathsf{app}}
\newcommand{\lam}[2]{{\langle}#1{\rangle}#2}
%\newcommand{\id}{{1}}
\newcommand{\id}{\mathrm{id}}
\newcommand{\pp}{{\sf p}}
\newcommand{\qq}{{\sf q}}
\newcommand{\comp}{{\sf comp}}
\newcommand{\hcomp}{{\sf hcomp}}
\newcommand{\pres}[1]{{\sf pres}^{#1}}
\newcommand{\extend}{{\sf extend}}
\newcommand{\eq}{{\sf equiv}}
\newcommand{\Comp}{{\sf fill}}
% HIT
\newcommand{\base}{{\sf base}}
\newcommand{\inc}{{\sf inc}}
\newcommand{\inh}{\mathsf{inh}}
\newcommand{\squash}{{\sf squash}}
\newcommand{\transp}{{\sf transp}} % defined operation on HITs
\newcommand{\squeeze}{{\sf squeeze}}
\newcommand{\LOOP}{{\sf loop}}
\newcommand{\Sp}{{\sf S}}
% Universe
\newcommand{\Glue}{{\sf Glue}}
\newcommand{\glue}{{\sf glue}}
\newcommand{\ugl}{{\sf unglue}}
\newcommand{\U}{\mathsf{U}}
\DeclareMathOperator{\eqToPath}{\mathsf{eqToPath}}
\newcommand{\can}{\mathsf{pathToEq}} % "the" canonical map for ua
% Semantics
\newcommand{\Set}{\mathbf{Set}}
\newcommand{\Top}{\mathbf{Top}}
\DeclareMathOperator{\sing}{\mathrm{S}}
\newcommand{\CC}{\mathcal{C}}
\renewcommand{\deg}{\mathrm{s}}
\newcommand{\op}{\mathrm{op}}
% \newcommand{\CdM}{\CC_\dM}
\DeclareMathOperator{\Hom}{Hom}
\newcommand{\cwf}{CwF}
\DeclareMathOperator{\Ty}{Ty}
\DeclareMathOperator{\FTy}{FTy} % for "fibrant" types
\DeclareMathOperator{\Ter}{Ter}
\newcommand{\den}[1]{[\![#1]\!]} % denotation
\DeclareMathOperator{\yoneda}{\mathbf{y}}
%\DeclareMathOperator{\scomp}{\mathbf{c}} % semantic composition
\DeclareMathOperator{\scomp}{\mathtt{comp}} % semantic composition
\DeclareMathOperator{\sGlue}{\mathtt{Glue}} % semantic Glue
\DeclareMathOperator{\sglue}{\mathtt{glue}} % semantic glue
\DeclareMathOperator{\sugl}{\mathtt{unglue}} % semantic unglue
\newcommand{\sNN}{\mathtt{N}}
%\DeclareMathOperator{\sequiv}{\mathbf{e}} % equivalence structure
\DeclareMathOperator{\sequiv}{\mathtt{e}} % equivalence structure
%\newcommand{\sPath}{\Path}
\newcommand{\sPath}{\mathtt{Path}}
\newcommand{\spabs}{\langle \, \rangle}
\newcommand{\NAT}{\mathbb{N}} % {0,1,2,..}
\newcommand{\UU}{\mathtt{U}} % semantic universe
\DeclareMathOperator{\app}{\mathtt{app}}
\DeclareMathOperator{\El}{\mathsf{El}}
\newcommand{\code}[1]{\ulcorner #1 \urcorner}
\tikzset{
comp line/.style={thick,draw=black,decorate, decoration={snake},
->, >=stealth'},
path line/.style={thick,draw=black},
fun line/.style={thick,draw=black, ->, >=stealth'}
}
\tikzset{
comp line/.style={thick,draw=black,decorate, decoration={snake},
->, >=stealth'},
path line/.style={thick,draw=black},
fun line/.style={thick,draw=black, ->, >=stealth'}
}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "main"
%%% End:

174
resources/CCHM/main.bbl vendored Normal file
View file

@ -0,0 +1,174 @@
\begin{thebibliography}{10}
\bibitem{Aczel99}
P.~Aczel.
\newblock {On Relating Type Theories and Set Theories}.
\newblock In T.~Altenkirch, B.~Reus, and W.~Naraschewski, editors, {\em Types
for Proofs and Programs}, volume 1657 of {\em Lecture Notes in Computer
Science}, pages 1--18. Springer Verlag, Berlin, Heidelberg, New York, 1999.
\bibitem{Altenkirch99}
T.~Altenkirch.
\newblock {Extensional Equality in Intensional Type Theory}.
\newblock In {\em 14th Annual {IEEE} Symposium on Logic in Computer Science},
pages 412--420, 1999.
\bibitem{Balbes}
R.~Balbes and P.~Dwinger.
\newblock {\em {Distributive Lattices}}.
\newblock Abstract Space Publishing, 2011.
\bibitem{paramtt}
J.-P. Bernardy, T.~Coquand, and G.~Moulin.
\newblock {A Presheaf Model of Parametric Type Theory}.
\newblock {\em Electronic Notes in Theoretical Computer Science}, 319:67--82,
2015.
\bibitem{ttincolor}
J.-P. Bernardy and G.~Moulin.
\newblock {Type-theory in Color}.
\newblock {\em SIGPLAN Not.}, 48(9):61--72, September 2013.
\bibitem{BCH}
M.~Bezem, T.~Coquand, and S.~Huber.
\newblock {A Model of Type Theory in Cubical Sets}.
\newblock In R.~Matthes and A.~Schubert, editors, {\em 19th International
Conference on Types for Proofs and Programs (TYPES 2013)}, volume~26 of {\em
Leibniz International Proceedings in Informatics (LIPIcs)}, pages 107--128.
Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2014.
\bibitem{Brown}
R.~Brown, P.J. Higgins, and R.~Sivera.
\newblock {\em {Nonabelian Algebraic Topology: Filtered Spaces, Crossed
Complexes, Cubical Homotopy Groupoids}}, volume~15 of {\em EMS tracts in
mathematics}.
\newblock European Mathematical Society, 2011.
\bibitem{Cisinski}
D.-C. {Cisinski}.
\newblock {Univalent universes for elegant models of homotopy types}.
\newblock {\em arXiv:1406.0058}, May 2014.
\newblock Preprint.
\bibitem{Dybjer96}
P.~Dybjer.
\newblock {Internal Type Theory}.
\newblock In {\em Lecture Notes in Computer Science}, pages 120--134. Springer
Verlag, Berlin, Heidelberg, New York, 1996.
\bibitem{Fourman-Scott}
M.~Fourman and D.~Scott.
\newblock Sheaves and logic.
\newblock In M.~Fourman, C.~Mulvey, and D.~Scott, editors, {\em {Applications
of Sheaves}}, volume 753 of {\em Lecture Notes in Mathematics}, pages
302--401. Springer Berlin Heidelberg, 1979.
\bibitem{GambinoSattler}
N.~{Gambino} and C.~{Sattler}.
\newblock {Uniform Fibrations and the Frobenius Condition}.
\newblock {\em arXiv:1510.00669}, October 2015.
\newblock Preprint.
\bibitem{Hofmann97}
M.~Hofmann.
\newblock Syntax and semantics of dependent types.
\newblock In A.M. Pitts and P.~Dybjer, editors, {\em Semantics and logics of
computation}, volume~14 of {\em Publ. Newton Inst.}, pages 79--130. Cambridge
University Press, Cambridge, 1997.
\bibitem{simonlic}
S.~Huber.
\newblock {\em {A Model of Type Theory in Cubical Sets}}.
\newblock Licentiate thesis, University of Gothenburg, May 2015.
\bibitem{Huber16}
S.~Huber.
\newblock Canonicity for cubical type theory.
\newblock {\em arXiv:1607.04156v1}, July 2016.
\newblock Preprint.
\bibitem{Kalman58}
J.~A. Kalman.
\newblock Lattices with involution.
\newblock {\em Transactions of the American Mathematical Society}, 87:485--491,
1958.
\bibitem{Kan55}
D.~M. Kan.
\newblock Abstract homotopy. {I}.
\newblock {\em Proceedings of the National Academy of Sciences of the United
States of America}, 41(12):1092--1096, 1955.
\bibitem{KL}
C.~{Kapulkin} and P.~{LeFanu Lumsdaine}.
\newblock {The Simplicial Model of Univalent Foundations (after {V}oevodsky)}.
\newblock {\em arXiv:1211.2851v4}, November 2012.
\newblock Preprint.
\bibitem{LicataBrunerie}
D.~R. Licata and G.~Brunerie.
\newblock {A Cubical Approach to Synthetic Homotopy Theory}.
\newblock In {\em 30th Annual {ACM/IEEE} Symposium on Logic in Computer
Science}, pages 92--103, 2015.
\bibitem{ML75}
P.~Martin-Löf.
\newblock An intuitionistic theory of types: predicative part.
\newblock In {\em Logic {C}olloquium '73 ({B}ristol, 1973)}, pages 73--118.
Studies in Logic and the Foundations of Mathematics, Vol. 80. North-Holland,
Amsterdam, 1975.
\bibitem{MLTT72}
P.~Martin-Löf.
\newblock An intuitionistic theory of types.
\newblock In G.~Sambin and J.~M. Smith, editors, {\em Twenty-five years of
constructive type theory ({V}enice, 1995)}, volume~36 of {\em Oxford Logic
Guides}, pages 127--172. Oxford University Press, 1998.
\bibitem{PittsBook}
A.~M. Pitts.
\newblock {\em {Nominal Sets: Names and Symmetry in Computer Science}}.
\newblock Cambridge University Press, New York, NY, USA, 2013.
\bibitem{Pitts}
A.~M. Pitts.
\newblock {Nominal Presentation of Cubical Sets Models of Type Theory}.
\newblock In H.~Herbelin, P.~Letouzey, and M.~Sozeau, editors, {\em 20th
International Conference on Types for Proofs and Programs (TYPES 2014)},
volume~39 of {\em Leibniz International Proceedings in Informatics (LIPIcs)},
pages 202--220. Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik, 2015.
\bibitem{Polonsky14}
Andrew Polonsky.
\newblock {Extensionality of lambda-*}.
\newblock In H.~Herbelin, P.~Letouzey, and M.~Sozeau, editors, {\em 20th
International Conference on Types for Proofs and Programs (TYPES 2014)},
volume~39 of {\em Leibniz International Proceedings in Informatics (LIPIcs)},
pages 221--250. Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2015.
\bibitem{Streicher91}
T.~Streicher.
\newblock {\em {Semantics of Type Theory}}.
\newblock Progress in Theoretical Computer Science. Birkh{\"a}user Basel, 1991.
\bibitem{Swan}
A.~{Swan}.
\newblock {An Algebraic Weak Factorisation System on 01-Substitution Sets: A
Constructive Proof}.
\newblock {\em arXiv:1409.1829}, September 2014.
\newblock Preprint.
\bibitem{hott-book}
The {Univalent Foundations Program}.
\newblock {\em {Homotopy Type Theory: Univalent Foundations of Mathematics}}.
\newblock \url{http://homotopytypetheory.org/book}, Institute for Advanced
Study, 2013.
\bibitem{Voevodsky}
V.~{Voevodsky}.
\newblock {The equivalence axiom and univalent models of type theory. (Talk at
CMU on February 4, 2010)}.
\newblock {\em arXiv:1402.5556}, February 2014.
\newblock Preprint.
\end{thebibliography}

128
resources/CCHM/main.tex vendored Normal file
View file

@ -0,0 +1,128 @@
\documentclass[10pt,a4paper,utf8]{article}
\usepackage[a4paper,inner=100pt,outer=100pt,textheight=630pt,centering]{geometry}
\usepackage{enumerate}
\usepackage[usenames,dvipsnames]{xcolor}
\usepackage[pagebackref,citecolor=blue,linkcolor=OliveGreen,urlcolor=Mahogany,colorlinks]{hyperref}
\usepackage[utf8]{inputenc}
\usepackage{color}
\usepackage{url}
\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{amsthm}
\usepackage{cases}
\usepackage[innertopmargin=-5,skipbelow=-5]{mdframed}
\usepackage{stmaryrd}
\usepackage{mathpartir}
\usepackage{tikz}
\usepackage{tikz-cd}
\usetikzlibrary{arrows,matrix,decorations.pathmorphing,
decorations.markings, calc, backgrounds}
\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem*{theorem*}{Theorem}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem*{lemma*}{Lemma}
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem*{corollary*}{Corollary}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem*{proposition*}{Proposition}
\theoremstyle{definition}
\newtheorem{definition}[theorem]{Definition}
\newtheorem*{definition*}{Definition}
\newtheorem{example}[theorem]{Example}
\newtheorem*{example*}{Example}
\theoremstyle{remark}
\newtheorem{remark}[theorem]{Remark}
\newtheorem*{remark*}{Remark}
\input{macro}
\begin{document}
\title{Cubical Type Theory: a constructive interpretation of the
univalence axiom\footnote{This material is based upon work supported
by the National Science Foundation under agreement
No. DMS-1128155. Any opinions, findings and conclusions or
recommendations expressed in this material are those of the
author(s) and do not necessarily reflect the views of the National
Science Foundation.}}
\author{Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg}
\date{}
\maketitle
\begin{abstract}
This paper presents a type theory in which it is possible to
directly manipulate $n$-dimensional cubes (points, lines, squares,
cubes, etc.) based on an interpretation of dependent type theory in
a cubical set model. This enables new ways to reason about identity
types, for instance, function extensionality is directly provable in
the system. Further, Voevodsky's univalence axiom is provable in
this system. We also explain an extension with some higher inductive
types like the circle and propositional truncation. Finally we
provide semantics for this cubical type theory in a constructive
meta-theory.
\end{abstract}
\tableofcontents
\input{cubicaltt}
\subparagraph*{Acknowledgements}
This work originates from discussions between the four authors around an implementation
of a type system corresponding to the model described in~\cite{BCH}. This implementation
indicated a problem with the representation of higher inductive types, e.g., the elimination rule
for the circle, and suggested the need of extending this cubical model with a diagonal
operation. The general framework (uniformity condition, connections, semantics of spheres and propositional
truncation) is due to the second author. In particular, the glueing operation with its composition was
introduced as a generalization of the operation described in~\cite{BCH} transforming an equivalence
into a path, and with the condition $A = \Glue~[]~A$. In a first attempt, we tried to force ``regularity'',
i.e., the equation $\transport~i~A~a_0 = a_0$ if $A$ is independent of $i$ (which seemed to be necessary
in order to get filling from compositions, and which implies $\Path = \Id$).
There was a problem however for getting regularity for the universe, that was discovered by Dan Licata (from
discussions with Carlo Angiuli and Bob Harper). Thanks to this discovery, it was realized that
regularity is actually not needed for the model to work. In particular, the second author
adapted the definition of filling from composition as in Section \ref{sec:kan-filling},
the third author noticed that we can remove the condition $A = \Glue~[]~A$, and together with the last author,
they derived the univalence axiom from the glueing operation as presented in the appendix.
This was surprising since glueing was introduced
a priori only as a way to transform equivalences into paths, but was later explained by a remark of Dan Licata
(also presented in the appendix: we get univalence as soon as the transport map associated to this
path is path equal to the given equivalence).
The second author introduced then the restriction operation $\Gamma,\varphi$
on contexts, which, as noticed by Christian Sattler, can be seen as an explicit syntax for the notion of
cofibration, and designed the other proof of univalence in \sect{sec:univalence-axiom} from
discussions between Nicola Gambino, Peter LeFanu Lumsdaine and the third author. Not having regularity, the type of
paths is not the same as the $\Id$ type but, as explained in \sect{sec:identitytypes}, we can recover
the usual identity type from the path type, following an idea of Andrew Swan.
\medskip
The authors would like to thank the referees and Mart\'in Escard\'o, Georges Gonthier,
Dan Grayson, Peter Hancock, Dan Licata, Peter LeFanu Lumsdaine,
Christian Sattler, Andrew Swan, Vladimir Voevodsky for many
interesting discussions and remarks.
\bibliographystyle{plainurl}% the recommended bibstyle
\bibliography{references}
\newpage
\appendix
\input{appendix}
\end{document}
%% Local Variables:
%% ispell-local-dictionary: "english"
%% mode: latex flyspell
%% TeX-master: "main"
%% End:

492
resources/CCHM/mathpartir.sty vendored Normal file
View file

@ -0,0 +1,492 @@
% Mathpartir --- Math Paragraph for Typesetting Inference Rules
%
% Copyright (C) 2001, 2002, 2003, 2004, 2005, 2015 Didier Rémy
%
% Author : Didier Remy
% Version : 1.3.1
% Bug Reports : to author
% Web Site : http://pauillac.inria.fr/~remy/latex/
%
% Mathpartir is free software; you can redistribute it and/or modify
% it under the terms of the GNU General Public License as published by
% the Free Software Foundation; either version 2, or (at your option)
% any later version.
%
% Mathpartir is distributed in the hope that it will be useful,
% but WITHOUT ANY WARRANTY; without even the implied warranty of
% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
% GNU General Public License for more details
% (http://pauillac.inria.fr/~remy/license/GPL).
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% File mathpartir.sty (LaTeX macros)
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\NeedsTeXFormat{LaTeX2e}
\ProvidesPackage{mathpartir}
[2015/11/06 version 1.3.1 Math Paragraph for Typesetting Inference Rules]
%%
%% Identification
%% Preliminary declarations
\RequirePackage {keyval}
%% Options
%% More declarations
%% PART I: Typesetting maths in paragraphe mode
%% \newdimen \mpr@tmpdim
%% Dimens are a precious ressource. Uses seems to be local.
\let \mpr@tmpdim \@tempdima
% To ensure hevea \hva compatibility, \hva should expands to nothing
% in mathpar or in inferrule
\let \mpr@hva \empty
%% normal paragraph parametters, should rather be taken dynamically
\def \mpr@savepar {%
\edef \MathparNormalpar
{\noexpand \lineskiplimit \the\lineskiplimit
\noexpand \lineskip \the\lineskip}%
}
\def \mpr@rulelineskip {\lineskiplimit=0.3em\lineskip=0.2em plus 0.1em}
\def \mpr@lesslineskip {\lineskiplimit=0.6em\lineskip=0.5em plus 0.2em}
\def \mpr@lineskip {\lineskiplimit=1.2em\lineskip=1.2em plus 0.2em}
\let \MathparLineskip \mpr@lineskip
\def \mpr@paroptions {\MathparLineskip}
\let \mpr@prebindings \relax
\newskip \mpr@andskip \mpr@andskip 2em plus 0.5fil minus 0.5em
\def \mpr@goodbreakand
{\hskip -\mpr@andskip \penalty -1000\hskip \mpr@andskip}
\def \mpr@and {\hskip \mpr@andskip}
\def \mpr@andcr {\penalty 50\mpr@and}
\def \mpr@cr {\penalty -10000\mpr@and}
%\def \mpr@cr {\penalty -10000\vadjust{\vbox{}}\mpr@and}
\def \mpr@eqno #1{\mpr@andcr #1\hskip 0em plus -1fil \penalty 10}
\def \mpr@bindings {%
\let \and \mpr@andcr
\let \par \mpr@andcr
\let \\\mpr@cr
\let \eqno \mpr@eqno
\let \hva \mpr@hva
}
\let \MathparBindings \mpr@bindings
% \@ifundefined {ignorespacesafterend}
% {\def \ignorespacesafterend {\aftergroup \ignorespaces}
\newenvironment{mathpar}[1][]
{$$\mpr@savepar \parskip 0em \hsize \linewidth \centering
\vbox \bgroup \mpr@prebindings \mpr@paroptions #1\ifmmode $\else
\noindent $\displaystyle\fi
\MathparBindings}
{\unskip \ifmmode $\fi\egroup $$\ignorespacesafterend}
\newenvironment{mathparpagebreakable}[1][]
{\begingroup
\par
\mpr@savepar \parskip 0em \hsize \linewidth \centering
\mpr@prebindings \mpr@paroptions #1%
\vskip \abovedisplayskip \vskip -\lineskip%
\ifmmode \else $\displaystyle\fi
\MathparBindings
}
{\unskip
\ifmmode $\fi \par\endgroup
\vskip \belowdisplayskip
\noindent
\ignorespacesafterend}
% \def \math@mathpar #1{\setbox0 \hbox {$\displaystyle #1$}\ifnum
% \wd0 < \hsize $$\box0$$\else \bmathpar #1\emathpar \fi}
%%% HOV BOXES
\def \mathvbox@ #1{\hbox \bgroup \mpr@normallineskip
\vbox \bgroup \tabskip 0em \let \\ \cr
\halign \bgroup \hfil $##$\hfil\cr #1\crcr \egroup \egroup
\egroup}
\def \mathhvbox@ #1{\setbox0 \hbox {\let \\\qquad $#1$}\ifnum \wd0 < \hsize
\box0\else \mathvbox {#1}\fi}
%% Part II -- operations on lists
\newtoks \mpr@lista
\newtoks \mpr@listb
\long \def\mpr@cons #1\mpr@to#2{\mpr@lista {\\{#1}}\mpr@listb \expandafter
{#2}\edef #2{\the \mpr@lista \the \mpr@listb}}
\long \def\mpr@snoc #1\mpr@to#2{\mpr@lista {\\{#1}}\mpr@listb \expandafter
{#2}\edef #2{\the \mpr@listb\the\mpr@lista}}
\long \def \mpr@concat#1=#2\mpr@to#3{\mpr@lista \expandafter {#2}\mpr@listb
\expandafter {#3}\edef #1{\the \mpr@listb\the\mpr@lista}}
\def \mpr@head #1\mpr@to #2{\expandafter \mpr@head@ #1\mpr@head@ #1#2}
\long \def \mpr@head@ #1#2\mpr@head@ #3#4{\def #4{#1}\def#3{#2}}
\def \mpr@flatten #1\mpr@to #2{\expandafter \mpr@flatten@ #1\mpr@flatten@ #1#2}
\long \def \mpr@flatten@ \\#1\\#2\mpr@flatten@ #3#4{\def #4{#1}\def #3{\\#2}}
\def \mpr@makelist #1\mpr@to #2{\def \mpr@all {#1}%
\mpr@lista {\\}\mpr@listb \expandafter {\mpr@all}\edef \mpr@all {\the
\mpr@lista \the \mpr@listb \the \mpr@lista}\let #2\empty
\def \mpr@stripof ##1##2\mpr@stripend{\def \mpr@stripped{##2}}\loop
\mpr@flatten \mpr@all \mpr@to \mpr@one
\expandafter \mpr@snoc \mpr@one \mpr@to #2\expandafter \mpr@stripof
\mpr@all \mpr@stripend
\ifx \mpr@stripped \empty \let \mpr@isempty 0\else \let \mpr@isempty 1\fi
\ifx 1\mpr@isempty
\repeat
}
\def \mpr@rev #1\mpr@to #2{\let \mpr@tmp \empty
\def \\##1{\mpr@cons ##1\mpr@to \mpr@tmp}#1\let #2\mpr@tmp}
%% Part III -- Type inference rules
\newif \if@premisse
\newbox \mpr@hlist
\newbox \mpr@vlist
\newif \ifmpr@center \mpr@centertrue
\def \mpr@vskip {}
\def \mpr@htovlist {%
\setbox \mpr@hlist
\hbox {\strut
\ifmpr@center \hskip -0.5\wd\mpr@hlist\fi
\unhbox \mpr@hlist}%
\setbox \mpr@vlist
\vbox {\if@premisse
\box \mpr@hlist
\ifx \mpr@vskip \empty \else
\hrule height 0em depth \mpr@vskip width 0em
\fi
\unvbox \mpr@vlist
\else
\unvbox \mpr@vlist
\ifx \mpr@vskip \empty \else
\hrule height 0em depth \mpr@vskip width 0em
\fi
\box \mpr@hlist
\fi}%
}
% OLD version
% \def \mpr@htovlist {%
% \setbox \mpr@hlist
% \hbox {\strut \hskip -0.5\wd\mpr@hlist \unhbox \mpr@hlist}%
% \setbox \mpr@vlist
% \vbox {\if@premisse \box \mpr@hlist \unvbox \mpr@vlist
% \else \unvbox \mpr@vlist \box \mpr@hlist
% \fi}%
% }
\def \mpr@item #1{$\displaystyle #1$}
\def \mpr@sep{2em}
\def \mpr@blank { }
\def \mpr@hovbox #1#2{\hbox
\bgroup
\ifx #1T\@premissetrue
\else \ifx #1B\@premissefalse
\else
\PackageError{mathpartir}
{Premisse orientation should either be T or B}
{Fatal error in Package}%
\fi \fi
\def \@test {#2}\ifx \@test \mpr@blank\else
\setbox \mpr@hlist \hbox {}%
\setbox \mpr@vlist \vbox {}%
\if@premisse \let \snoc \mpr@cons \else \let \snoc \mpr@snoc \fi
\let \@hvlist \empty \let \@rev \empty
\mpr@tmpdim 0em
\expandafter \mpr@makelist #2\mpr@to \mpr@flat
\if@premisse \mpr@rev \mpr@flat \mpr@to \@rev \else \let \@rev \mpr@flat \fi
\def \\##1{%
\def \@test {##1}\ifx \@test \empty
\mpr@htovlist
\mpr@tmpdim 0em %%% last bug fix not extensively checked
\else
\setbox0 \hbox{\mpr@item {##1}}\relax
\advance \mpr@tmpdim by \wd0
%\mpr@tmpdim 1.02\mpr@tmpdim
\ifnum \mpr@tmpdim < \hsize
\ifnum \wd\mpr@hlist > 0
\if@premisse
\setbox \mpr@hlist
\hbox {\unhbox0 \hskip \mpr@sep \unhbox \mpr@hlist}%
\else
\setbox \mpr@hlist
\hbox {\unhbox \mpr@hlist \hskip \mpr@sep \unhbox0}%
\fi
\else
\setbox \mpr@hlist \hbox {\unhbox0}%
\fi
\else
\ifnum \wd \mpr@hlist > 0
\mpr@htovlist
\mpr@tmpdim \wd0
\fi
\setbox \mpr@hlist \hbox {\unhbox0}%
\fi
\advance \mpr@tmpdim by \mpr@sep
\fi
}%
\@rev
\mpr@htovlist
\ifmpr@center \hskip \wd\mpr@vlist\fi \box \mpr@vlist
\fi
\egroup
}
%%% INFERENCE RULES
\@ifundefined{@@over}{%
\let\@@over\over % fallback if amsmath is not loaded
\let\@@overwithdelims\overwithdelims
\let\@@atop\atop \let\@@atopwithdelims\atopwithdelims
\let\@@above\above \let\@@abovewithdelims\abovewithdelims
}{}
%% The default
\def \mpr@@fraction #1#2{\hbox {\advance \hsize by -0.5em
$\displaystyle {#1\mpr@over #2}$}}
\def \mpr@@nofraction #1#2{\hbox {\advance \hsize by -0.5em
$\displaystyle {#1\@@atop #2}$}}
\let \mpr@fraction \mpr@@fraction
%% A generic solution to arrow
\def \mpr@@fractionaboveskip {0ex}
\def \mpr@@fractionbelowskip {0.22ex}
\def \mpr@make@fraction #1#2#3#4#5{\hbox {%
\def \mpr@tail{#1}%
\def \mpr@body{#2}%
\def \mpr@head{#3}%
\setbox1=\hbox{$#4$}\setbox2=\hbox{$#5$}%
\setbox3=\hbox{$\mkern -3mu\mpr@body\mkern -3mu$}%
\dimen0\ht3\advance\dimen0 by \dp3\relax
\dimen0 0.5\dimen0\relax
\advance \dimen0 by \mpr@@fractionaboveskip
\setbox1=\hbox {\raise \dimen0 \box1}\relax
\dimen0 -\dimen0\advance \dimen0 \mpr@@fractionaboveskip\dimen0 -\dimen0
\advance \dimen0 by \mpr@@fractionbelowskip
\setbox2=\hbox {\lower \dimen0 \box2}\relax
\setbox0=\hbox {$\displaystyle {\box1 \atop \box2}$}%
\dimen0=\wd0\box0
\box0 \hskip -\dimen0\relax
\hbox to \dimen0 {$%\color{blue}
\mathrel{\mpr@tail}\joinrel
\xleaders\hbox{\copy3}\hfil\joinrel\mathrel{\mpr@head}%
$}}}
%% Old stuff should be removed in next version
\def \mpr@@nothing #1#2
{$\lower 0.01pt \mpr@@nofraction {#1}{#2}$}
\def \mpr@@reduce #1#2{\hbox
{$\lower 0.01pt \mpr@@fraction {#1}{#2}\mkern -15mu\rightarrow$}}
\def \mpr@@rewrite #1#2#3{\hbox
{$\lower 0.01pt \mpr@@fraction {#2}{#3}\mkern -8mu#1$}}
\def \mpr@infercenter #1{\vcenter {\mpr@hovbox{T}{#1}}}
\def \mpr@empty {}
\def \mpr@inferrule
{\bgroup
\ifnum \linewidth<\hsize \hsize \linewidth\fi
\mpr@rulelineskip
\let \and \qquad
\let \hva \mpr@hva
\let \@rulename \mpr@empty
\let \@rule@options \mpr@empty
\let \mpr@over \@@over
\mpr@inferrule@}
\newcommand {\mpr@inferrule@}[3][]
{\everymath={\displaystyle}%
\def \@test {#2}\ifx \empty \@test
\setbox0 \hbox {$\vcenter {\mpr@hovbox{B}{#3}}$}%
\else
\def \@test {#3}\ifx \empty \@test
\setbox0 \hbox {$\vcenter {\mpr@hovbox{T}{#2}}$}%
\else
\setbox0 \mpr@fraction {\mpr@hovbox{T}{#2}}{\mpr@hovbox{B}{#3}}%
\fi \fi
\def \@test {#1}\ifx \@test\empty \box0
\else \vbox
%%% Suggestion de Francois pour les etiquettes longues
%%% {\hbox to \wd0 {\RefTirName {#1}\hfil}\box0}\fi
{\hbox {\DefTirName {#1}}\box0}\fi
\egroup}
\def \mpr@vdotfil #1{\vbox to #1{\leaders \hbox{$\cdot$} \vfil}}
% They are two forms
% \inferrule [label]{[premisses}{conclusions}
% or
% \inferrule* [options]{[premisses}{conclusions}
%
% Premisses and conclusions are lists of elements separated by \\
% Each \\ produces a break, attempting horizontal breaks if possible,
% and vertical breaks if needed.
%
% An empty element obtained by \\\\ produces a vertical break in all cases.
%
% The former rule is aligned on the fraction bar.
% The optional label appears on top of the rule
% The second form to be used in a derivation tree is aligned on the last
% line of its conclusion
%
% The second form can be parameterized, using the key=val interface. The
% folloiwng keys are recognized:
%
% width set the width of the rule to val
% narrower set the width of the rule to val\hsize
% before execute val at the beginning/left
% lab put a label [Val] on top of the rule
% lskip add negative skip on the right
% left put a left label [Val]
% Left put a left label [Val], ignoring its width
% right put a right label [Val]
% Right put a right label [Val], ignoring its width
% leftskip skip negative space on the left-hand side
% rightskip skip negative space on the right-hand side
% vdots lift the rule by val and fill vertical space with dots
% after execute val at the end/right
%
% Note that most options must come in this order to avoid strange
% typesetting (in particular leftskip must preceed left and Left and
% rightskip must follow Right or right; vdots must come last
% or be only followed by rightskip.
%
%% Keys that make sence in all kinds of rules
\def \mprset #1{\setkeys{mprset}{#1}}
\define@key {mprset}{andskip}[]{\mpr@andskip=#1}
\define@key {mprset}{lineskip}[]{\lineskip=#1}
\define@key {mprset}{lessskip}[]{\lineskip=0.5\lineskip}
\define@key {mprset}{flushleft}[]{\mpr@centerfalse}
\define@key {mprset}{center}[]{\mpr@centertrue}
\define@key {mprset}{rewrite}[]{\let \mpr@fraction \mpr@@rewrite}
\define@key {mprset}{atop}[]{\let \mpr@fraction \mpr@@nofraction}
\define@key {mprset}{myfraction}[]{\let \mpr@fraction #1}
\define@key {mprset}{fraction}[]{\def \mpr@fraction {\mpr@make@fraction #1}}
% To be documented.
\define@key {mprset}{defaultfraction}[]{\let \mpr@fraction \mpr@@fraction}
\define@key {mprset}{sep}{\def\mpr@sep{#1}}
\define@key {mprset}{fractionaboveskip}{\def\mpr@@fractionaboveskip{#1}}
\define@key {mprset}{fractionbelowskip}{\def\mpr@@fractionbelowskip{#1}}
\define@key {mprset}{style}[1]{\def\TirNameStyle{#1}def}
\define@key {mprset}{rightstyle}[1]{\def\RightTirNameStyle{#1}}
\define@key {mprset}{leftstyle}[1]{\def\LeftTirNameStyle{#1}}
\define@key {mprset}{vskip}[1]{\def \mpr@vskip{#1}}
\newbox \mpr@right
\define@key {mpr}{flushleft}[]{\mpr@centerfalse}
\define@key {mpr}{center}[]{\mpr@centertrue}
\define@key {mpr}{rewrite}[]{\let \mpr@fraction \mpr@@rewrite}
\define@key {mpr}{myfraction}[]{\let \mpr@fraction #1}
\define@key {mpr}{fraction}[]{\def \mpr@fraction {\mpr@make@fraction #1}}
\define@key {mpr}{width}{\hsize #1}
\define@key {mpr}{sep}{\def\mpr@sep{#1}}
\define@key {mpr}{before}{#1}
\define@key {mpr}{lab}{\let \DefTirName \LabTirName \def \mpr@rulename {#1}}
\define@key {mpr}{Lab}{\let \DefTirName \LabTirName \def \mpr@rulename {#1}}
\define@key {mpr}{style}[1]{\def\TirNameStyle{#1}def}
\define@key {mpr}{rightstyle}[1]{\def\RightTirNameStyle{#1}}
\define@key {mpr}{leftstyle}[1]{\def\LeftTirNameStyle{#1}}
\define@key {mpr}{vskip}[1]{\def \mpr@vskip{#1}}
\define@key {mpr}{narrower}{\hsize #1\hsize}
\define@key {mpr}{leftskip}{\hskip -#1}
\define@key {mpr}{reduce}[]{\let \mpr@fraction \mpr@@reduce}
\define@key {mpr}{rightskip}
{\setbox \mpr@right \hbox {\unhbox \mpr@right \hskip -#1}}
\define@key {mpr}{LEFT}{\setbox0 \hbox {$#1$}\relax
\advance \hsize by -\wd0\box0}
\define@key {mpr}{left}{\setbox0 \hbox {$\LeftTirName {#1}\;$}\relax
\advance \hsize by -\wd0\box0}
\define@key {mpr}{Left}{\llap{$\LeftTirName {#1}\;$}}
\define@key {mpr}{right}
{\setbox0 \hbox {$\;\RightTirName {#1}$}\relax \advance \hsize by -\wd0
\setbox \mpr@right \hbox {\unhbox \mpr@right \unhbox0}}
\define@key {mpr}{RIGHT}
{\setbox0 \hbox {$#1$}\relax \advance \hsize by -\wd0
\setbox \mpr@right \hbox {\unhbox \mpr@right \unhbox0}}
\define@key {mpr}{Right}
{\setbox \mpr@right \hbox {\unhbox \mpr@right \rlap {$\;\RightTirName {#1}$}}}
\define@key {mpr}{vdots}{\def \mpr@vdots {\@@atop \mpr@vdotfil{#1}}}
\define@key {mpr}{after}{\edef \mpr@after {\mpr@after #1}}
\define@key {mpr}{vcenter}[]{\mpr@vcentertrue}
\newif \ifmpr@vcenter \mpr@vcenterfalse
\newcommand \mpr@inferstar@ [3][]{\begingroup
\setbox0 \hbox
{\let \mpr@rulename \mpr@empty \let \mpr@vdots \relax
\setbox \mpr@right \hbox{}%
\setkeys{mpr}{#1}%
$\ifx \mpr@rulename \mpr@empty \mpr@inferrule {#2}{#3}\else
\mpr@inferrule [{\mpr@rulename}]{#2}{#3}\fi
\box \mpr@right \mpr@vdots$
\ifmpr@vcenter \aftergroup \mpr@vcentertrue \fi}
\ifmpr@vcenter
\box0
\else
\setbox1 \hbox {\strut}
\@tempdima \dp0 \advance \@tempdima by -\dp1
\raise \@tempdima \box0
\fi
\endgroup}
\def \mpr@infer {\@ifnextchar *{\mpr@inferstar}{\mpr@inferrule}}
\newcommand \mpr@err@skipargs[3][]{}
\def \mpr@inferstar*{\ifmmode
\let \@do \mpr@inferstar@
\else
\let \@do \mpr@err@skipargs
\PackageError {mathpartir}
{\string\inferrule* can only be used in math mode}{}%
\fi \@do}
%%% Exports
% Envirnonment mathpar
\let \inferrule \mpr@infer
% make a short name \infer is not already defined
\@ifundefined {infer}{\let \infer \mpr@infer}{}
\def \TirNameStyle #1{\small \textsc{#1}}
\def \LeftTirNameStyle #1{\TirNameStyle {#1}}
\def \RightTirNameStyle #1{\TirNameStyle {#1}}
\def \lefttir@name #1{\hbox {\small \LeftTirNameStyle{#1}}}
\def \righttir@name #1{\hbox {\small \RightTirNameStyle{#1}}}
\let \TirName \lefttir@name
\let \LeftTirName \lefttir@name
\let \DefTirName \lefttir@name
\let \LabTirName \lefttir@name
\let \RightTirName \righttir@name
%%% Other Exports
% \let \listcons \mpr@cons
% \let \listsnoc \mpr@snoc
% \let \listhead \mpr@head
% \let \listmake \mpr@makelist
\endinput

1
src/CubicalHott/Chapter1.lagda.md
View file

@ -31,6 +31,7 @@ record Σ {ℓ ℓ'} (A : Type ℓ) (B : A → Type ℓ') : Type (ℓ ⊔ ℓ')
open Σ public
{-# BUILTIN SIGMA Σ #-}
infixr 4 _,_
```
Unit type:

87
src/CubicalHott/Chapter2.lagda.md
View file

@ -149,43 +149,40 @@ A ≃ B = Σ (A → B) isequiv
```
module lemma2∙4∙12 where
id-equiv : {l : Level} → (A : Type l) → A ≃ A
id-equiv A = id , e
where
e : isequiv id
e = mkIsEquiv id (λ _ → refl) id (λ _ → refl)
id-equiv A = id , qinv-to-isequiv (mkQinv id (λ _ → refl) (λ _ → refl))
sym-equiv : {A B : Type} → (f : A ≃ B) → B ≃ A
sym-equiv {A} {B} (f , eqv) =
let (mkQinv g α β) = isequiv-to-qinv eqv
in g , qinv-to-isequiv (mkQinv f β α)
trans-equiv : {A B C : Type} → (f : A ≃ B) → (g : B ≃ C) → A ≃ C
trans-equiv {A} {B} {C} (f , f-eqv) (g , g-eqv) =
let
(mkQinv f-inv f-inv-left f-inv-right) = isequiv-to-qinv f-eqv
(mkQinv g-inv g-inv-left g-inv-right) = isequiv-to-qinv g-eqv
-- trans-equiv : {A B C : Type} → (f : A ≃ B) → (g : B ≃ C) → A ≃ C
-- trans-equiv {A} {B} {C} (f , f-eqv) (g , g-eqv) =
-- let
-- (mkQinv f-inv f-inv-left f-inv-right) = isequiv-to-qinv f-eqv
-- (mkQinv g-inv g-inv-left g-inv-right) = isequiv-to-qinv g-eqv
open ≡-Reasoning
-- open ≡-Reasoning
forward : ((g ∘ f) ∘ (f-inv ∘ g-inv)) ∼ id
forward c =
begin
((g ∘ f) ∘ (f-inv ∘ g-inv)) c ≡⟨ ap (λ f → f c) (composite-assoc (f-inv ∘ g-inv) f g) ⟩
(g ∘ (f ∘ f-inv) ∘ g-inv) c ≡⟨ ap g (f-inv-left (g-inv c)) ⟩
(g ∘ id ∘ g-inv) c ≡⟨⟩
(g ∘ g-inv) c ≡⟨ g-inv-left c ⟩
id c ∎
-- forward : ((g ∘ f) ∘ (f-inv ∘ g-inv)) ∼ id
-- forward c =
-- begin
-- ((g ∘ f) ∘ (f-inv ∘ g-inv)) c ≡⟨ ap (λ f → f c) (composite-assoc (f-inv ∘ g-inv) f g) ⟩
-- (g ∘ (f ∘ f-inv) ∘ g-inv) c ≡⟨ ap g (f-inv-left (g-inv c)) ⟩
-- (g ∘ id ∘ g-inv) c ≡⟨⟩
-- (g ∘ g-inv) c ≡⟨ g-inv-left c ⟩
-- id c ∎
backward : ((f-inv ∘ g-inv) ∘ (g ∘ f)) ∼ id
backward a =
begin
((f-inv ∘ g-inv) ∘ (g ∘ f)) a ≡⟨ ap (λ f → f a) (composite-assoc (g ∘ f) g-inv f-inv) ⟩
(f-inv ∘ (g-inv ∘ (g ∘ f))) a ≡⟨ ap f-inv (g-inv-right (f a)) ⟩
(f-inv ∘ (id ∘ f)) a ≡⟨⟩
(f-inv ∘ f) a ≡⟨ f-inv-right a ⟩
id a ∎
-- backward : ((f-inv ∘ g-inv) ∘ (g ∘ f)) ∼ id
-- backward a =
-- begin
-- ((f-inv ∘ g-inv) ∘ (g ∘ f)) a ≡⟨ ap (λ f → f a) (composite-assoc (g ∘ f) g-inv f-inv) ⟩
-- (f-inv ∘ (g-inv ∘ (g ∘ f))) a ≡⟨ ap f-inv (g-inv-right (f a)) ⟩
-- (f-inv ∘ (id ∘ f)) a ≡⟨⟩
-- (f-inv ∘ f) a ≡⟨ f-inv-right a ⟩
-- id a ∎
in ?
-- in {! !}
-- in g ∘ f , qinv-to-isequiv (mkQinv (f-inv ∘ g-inv) forward backward)
```
@ -194,27 +191,39 @@ module lemma2∙4∙12 where
### Lemma 2.10.1
```
idtoeqv : {l : Level} {A B : Type l}
→ (A ≡ B)
→ (A ≃ B)
idtoeqv {l} {A} {B} refl = lemma2∙4∙12.id-equiv A
-- idtoeqv : {l : Level} {A B : Type l}
-- → (A ≡ B)
-- → (A ≃ B)
-- idtoeqv {l} {A} {B} p = transport {! !} {! !} {! p !} , qinv-to-isequiv (mkQinv {! !} {! !} {! !})
```
### Axiom 2.10.3 (Univalence)
```
module axiom2∙10∙3 where
postulate
ua : {l : Level} {A B : Type l} → (A ≃ B) → (A ≡ B)
Glue : ∀ {l l2} (A : Type l)
→ {φ : I}
→ (Te : Partial φ (Σ (Type l2) (λ T → T ≃ A)))
→ Type l2
forward : {l : Level} {A B : Type l} → (eqv : A ≃ B) → (idtoeqv ∘ ua) eqv ≡ eqv
-- forward eqv = {! !}
id-equiv : isequiv id
backward : {l : Level} {A B : Type l} → (p : A ≡ B) → (ua ∘ idtoeqv) p ≡ p
-- backward p = {! !}
ua : ∀ {l} {A B : Type l} → A ≃ B → A ≡ B
ua {A = A} {B} eqv i = Glue B λ
{ (i = i0) → A , eqv
; (i = i1) → B , _ , id-equiv
}
-- postulate
-- ua : {l : Level} {A B : Type l} → (A ≃ B) → (A ≡ B)
ua-eqv : {l : Level} {A : Type l} {B : Type l} → (A ≃ B) ≃ (A ≡ B)
ua-eqv = ua , qinv-to-isequiv (mkQinv idtoeqv backward forward)
-- forward : {l : Level} {A B : Type l} → (eqv : A ≃ B) → (idtoeqv ∘ ua) eqv ≡ eqv
-- -- forward eqv = {! !}
-- backward : {l : Level} {A B : Type l} → (p : A ≡ B) → (ua ∘ idtoeqv) p ≡ p
-- -- backward p = {! !}
-- ua-eqv : {l : Level} {A : Type l} {B : Type l} → (A ≃ B) ≃ (A ≡ B)
-- ua-eqv = ua , qinv-to-isequiv (mkQinv idtoeqv backward forward)
open axiom2∙10∙3 hiding (forward; backward)
```

56
src/VanDoornDissertation/Preliminaries.lagda.md
View file

@ -1,41 +1,14 @@
```
{-# OPTIONS --cubical #-}
module VanDoornDissertation.Preliminaries where
open import Agda.Primitive
open import Agda.Primitive.Cubical
open import CubicalHott.Chapter1
open import CubicalHott.Chapter2
```
### 2.2.1 Paths
```
Path : {ℓ : Level} (A : Set ℓ) → A → A → Set ℓ
Path A = PathP (λ i → A)
infix 4 _≡_
_≡_ : {ℓ : Level} {A : Set ℓ} → A → A → Set ℓ
_≡_ {A = A} = Path A
private
to-path : {ℓ : Level} {A : Set ℓ} → (f : I → A) → Path A (f i0) (f i1)
to-path f i = f i
refl : {ℓ : Level} {A : Set ℓ} {x : A} → x ≡ x
refl {x = x} = to-path (λ i → x)
id : {l : Level} {A : Set l} → A → A
id x = x
ap : {l1 l2 : Level} {A : Set l1} {B : Set l2} {x y : A}
→ (f : A → B)
→ (p : x ≡ y)
→ f x ≡ f y
ap {l1} {l2} {A} {B} {x} {y} f p i = f (p i)
-- J (λ x y p → f x ≡ f y) (λ x → refl) x y p
transport : {l₁ l₂ : Level} {A : Set l₁} {x y : A}
→ (P : A → Set l₂)
→ (p : x ≡ y)
→ P x → P y
transport {l₁} {l₂} {A} {x} {y} P p = primTransp (λ i → P (p i)) i0
```
### 2.2.3 More on paths
@ -43,17 +16,17 @@ transport {l₁} {l₂} {A} {x} {y} P p = primTransp (λ i → P (p i)) i0
#### Pathovers
```
dependent-path : {A : Set}
→ (P : A → Set)
dependent-path : {A : Type}
→ (P : A → Type)
→ {x y : A}
→ (p : x ≡ y)
→ (u : P x) → (v : P y) → Set
→ (u : P x) → (v : P y) → Type
dependent-path P p u v = transport P p u ≡ v
syntax dependent-path P p u v = u ≡[ P , p ] v
-- https://git.mzhang.io/school/type-theory/issues/16
apd : ∀ {a b} {A : I → Set a} {B : (i : I) → A i → Set b}
apd : ∀ {a b} {A : I → Type a} {B : (i : I) → A i → Type b}
→ (f : (i : I) → (a : A i) → B i a)
→ {x : A i0}
→ {y : A i1}
@ -65,14 +38,13 @@ apd f p i = f i (p i)
#### Squares
```
data square {A : Set} {a00 : A} : {a20 a02 a22 : A}
→ a00 ≡ a20
→ a02 ≡ a22
→ a00 ≡ a02
→ a20 ≡ a22
→ Set
where
reflₛ : square refl refl refl refl
Square : {A : Type} {a00 a10 a01 a11 : A}
→ (p : a00 ≡ a01)
→ (q : a00 ≡ a10)
→ (s : a01 ≡ a11)
→ (r : a10 ≡ a11)
→ Type
Square p q s r = PathP (λ i → p i ≡ r i) q s
```
#### Squareovers and cubes

22
tsconfig.json Normal file
View file

@ -0,0 +1,22 @@
{
"compilerOptions": {
"lib": ["ESNext"],
"target": "ESNext",
"module": "ESNext",
"moduleDetection": "force",
"jsx": "react-jsx",
"allowJs": true,
/* Bundler mode */
"moduleResolution": "bundler",
"allowImportingTsExtensions": true,
"verbatimModuleSyntax": true,
"noEmit": true,
/* Linting */
"skipLibCheck": true,
"strict": true,
"noFallthroughCasesInSwitch": true,
"forceConsistentCasingInFileNames": true
}
}