f.tex

\documentclass[11pt]{article}
\usepackage{fullpage}
\usepackage{tikz}
\usepackage{url}
\usepackage{stmaryrd}
\usepackage{amssymb}
\usepackage[sans]{dsfont}
\usepackage{color, colortbl}
\usepackage{courier}
\usepackage{graphicx}
\usepackage[all]{xy}
\xyoption{line}

\newcommand{\amr}[1]{\fbox{Amr says:} \textbf{#1}}

% ----------------------------------------------------------------------
% XY-Pic definitions for making ``wire charts''

\def\wirechart#1#2{\let\labelstyle\objectstyle\xy*[*1.0]\xybox{\small%
\xymatrix@C=10mm@R=4mm#1{#2}}\endxy}
\def\wire#1#2{\ar@{-}[#1]^<>(.5){#2}}
\def\wireright#1#2{\wire{#1}{#2}\ar@{}[#1]|<>(.5)/.6ex/{\dir2{>}}}
\def\wireleft#1#2{\wire{#1}{#2}\ar@{}[#1]|<>(.5)/-.6ex/{\dir2{<}}}
\def\wwblank#1{*=<#1,0mm>{~}}
\def\wblank{\wwblank{11mm}}
\def\blank{\wwblank{8mm}}
\def\vublank{*=<0mm,2.3mm>!D{}}
\def\vdblank{*=<0mm,2.3mm>!U{}}
\def\vsblank{*=<0mm,5.6mm>{}}
\def\wirecross#1{\save[]!L;[#1]!R**@{-}\restore}
\def\wirebraid#1#2{\save[]!L;[#1]!R**{}?(#2)**@{-}\restore\save[#1]!R;[]!L**{}?(#2)**@{-}\restore}
\def\wireopen#1{\save[]!R;[#1]!R**\crv{[]!C&[#1]!C}\restore}
\def\wireclose#1{\save[]!L;[#1]!L**\crv{[]!C&[#1]!C}\restore}
\def\wireopenlabel#1#2{\save[]!R;[#1]!R**\crv{[]!C&[#1]!C}?<>(.5)*^+!R{#2}\restore}
\def\wirecloselabel#1#2{\save[]!L;[#1]!L**\crv{[]!C&[#1]!C}?<>(.5)*^+!L{#2}\restore}
\def\wireid{\blank\save[]!L*{};[]!R*{}**@{-}\restore}
\def\wwireid{\wblank\save[]!L*{};[]!R*{}**@{-}\restore}
\def\wwwireid#1{\wwblank{#1}\save[]!L*{};[]!R*{}**@{-}\restore}
\newcommand{\corner}{\rule{2.5mm}{2.5mm}}
\def\minheight{8mm}
\def\addheight{8mm}
\def\cornerbox#1#2#3{  % draw a box with a marked corner around
                   % the object #1. #2=label
                   % usage:   \ulbox{[ll].[].[ul]}{f}
  \save#1="box";
  "box"!C*+<0mm,\addheight>+=<0mm,\minheight>[|(5)]\frm{-}="box1";
  "box1"*{#2};
  ={"box1"!LU*!LU[]{\corner}}"ul";
  ={"box1"!RU*!RU[]{\corner}}"ur";
  ={"box1"!LD*!LD[]{\corner}}"dl";
  ={"box1"!RD*!RD[]{\corner}}"dr";
  #3
  \restore
}
\def\nnbox#1#2{\cornerbox{#1}{#2}{}}
\def\ulbox#1#2{\cornerbox{#1}{#2}{"ul"}}
\def\urbox#1#2{\cornerbox{#1}{#2}{"ur"}}
\def\dlbox#1#2{\cornerbox{#1}{#2}{"dl"}}
\def\drbox#1#2{\cornerbox{#1}{#2}{"dr"}}
\def\ubox#1#2{\cornerbox{#1}{#2}{"ul","ur"}}
\def\dbox#1#2{\cornerbox{#1}{#2}{"dl","dr"}}
\def\lbox#1#2{\cornerbox{#1}{#2}{"ul","dl"}}
\def\rbox#1#2{\cornerbox{#1}{#2}{"ur","dr"}}
\def\circbox#1{*+[o][F-]{#1}}

\newtheorem{definition}{Definition}
\newtheorem{n-lemma}{Lemma}[section]
\newtheorem{n-example}[n-lemma]{Example}
\newenvironment{example}{\begin{n-example}}{\end{n-example}}

\newcommand{\br}{\mathit{Br}}
\newcommand{\ssep}{\hspace{1em}} 
\newcommand{\sym}{c}       % braid: could be \sigma or c or \gamma
\newcommand{\cp}{\circ}                 % composition
\newcommand{\pc}{\fatsemi}                 % path composition
\newcommand{\symi}{\sym\inv}
\newcommand{\inv}{^{-1}}
\newcommand{\lolli}{\multimap} 
\newcommand{\id}{\textrm{\rm id}}       % identity
\newcommand{\x}{\otimes}
\newcommand{\boolt}{\mathit{bool}}
\newcommand{\ffv}{\mathit{false}}
\newcommand{\ttv}{\mathit{true}}
\newcommand{\notb}{\mathit{not}}
\newcommand{\union}{\cup}
\newcommand{\transport}[2]{\overline{#1}(#2)}
\newcommand{\refl}{\mathit{refl}}
\renewcommand{\path}{\leadsto}
\newcommand{\paths}[1]{\mathds{P}(#1)}
%% \renewcommand{\circ}{\circlearrowleft}
\newcommand{\alt}{~|~}
\newcommand{\dt}[1]{\llbracket #1 \rrbracket}
\newcommand{\leftv}[1]{\textsf{left}~#1}
\newcommand{\rightv}[1]{\textsf{right}~#1}
\newcommand{\iso}{\leftrightarrow}
\newcommand{\identlp}{\mathit{identl}_+}
\newcommand{\identrp}{\mathit{identr}_+}
\newcommand{\swapp}{\mathit{swap}_+}
\newcommand{\assoclp}{\mathit{assocl}_+}
\newcommand{\assocrp}{\mathit{assocr}_+}
\newcommand{\identlt}{\mathit{identl}_*}
\newcommand{\identrt}{\mathit{identr}_*}
\newcommand{\swapt}{\mathit{swap}_*}
\newcommand{\assoclt}{\mathit{assocl}_*}
\newcommand{\assocrt}{\mathit{assocr}_*}
\newcommand{\distz}{\mathit{dist}_0}
\newcommand{\factorz}{\mathit{factor}_0}
\newcommand{\dist}{\mathit{dist}}
\newcommand{\factor}{\mathit{factor}}
\newcommand{\idc}{\mathit{id}}
\newcommand{\wedgesum}{\vee}
\newcommand{\smashproduct}{\wedge}
\newcommand{\symc}[1]{\mathit{sym}~#1}
\newcommand{\proves}{\vdash}
\newcommand{\ap}[2]{\mathit{ap}~#1~#2}
\newcommand{\Rule}[4]{
\makebox{{\rm #1}
$\displaystyle
\frac{\begin{array}{l}#2\\\end{array}}
{\begin{array}{l}#3\\\end{array}}$
 #4}}
\newcommand{\jdg}[3]{#2 \proves_{#1} #3}
\newcommand{\adjoint}[1]{#1^{\dagger}}

\begin{document}
\begin{titlepage}
\begin{center}
\vfill
{\LARGE Isomorphisms as Groupoids: \\ 
  Homotopy Type Theory and Fractional Types} \\[1.5cm]
\vfill
\end{center}
\vfill
\noindent\textbf{Abstract.} 

\vfill
\vfill
\end{titlepage}

\title{Isomorphisms as Groupoids: \\ 
  Homotopy Type Theory and Fractional Types}
\author{?}
\date{\today}
\maketitle

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Introduction}

HoTT cannot really deal with functions. The starting point is that paths
explain and witness identities. This works for all the usual types but not
for functions or universes. For functions, the HoTT treatment is to allow
arbitrary functions, single out the isos via classical extensional methods,
and then assert via an axiom that the class of singled out functions is
equivalent to paths. This is a convoluted way. Why not start with functions
that are, by construction, isos. This was the programme we started earlier,
inspired by physical considerations. Because physics requires various
conservation principles (including conservation of information) and because
computation is fundamentally a physical process, the argument (originally due
to Feynman etc.) was that computation should be based on reversible
processes, or in abstract terms, on isomorphisms. That fits very well with
the HoTT philosophy that makes isos first-class. Except that HoTT does not
deal exclusively with isos, the functions are generally not isos. So let's
investigate the radical idea that all functions are isos in the HoTT
framework. What we get is a notion of first-class functions that by
construction are isos and obey the usual path rules etc. The technical device
is the notion of fractional types which are dual to products. A function
(iso) $A \rightarrow B$ is represented as an element of the type
$(\frac{1}{A} \times B)$. The construction shows the essential nature of the
$\infty$-groupoid structure. The more higher-order functions we have the
higher we have to go in the groupoid structure. We also have something
significant in the realm of reversible computing. We finally have
higher-order functions. Of course we need to show that we have constructed a
monoidal closed category (a concrete one) and then we can inherit all the
fancy constructions. Finally we have a very interesting operational
interpretation of paths and we outline various applications.

Need a clear explanation of why we can't deal with the usual functions that
are not isomorphisms. Regular function spaces obey $1^A = 1$ for all $A$. In
terms of fractionals this gives $\frac{1}{A} = 1$ for all $A$ which is not
true. However if we restrict to isomorphisms then the only functions we can
write are $A \rightarrow B$ where $A$ and $B$ are isomorphic types and hence
the only functions we can write in the space $1^A$ are to types $A$ that are
isomorphic to 1 and in that case we do indeed get that $\frac{1}{A} =
1$. See~\cite{fiore-remarks} for more details. The benefit is that we fit
squarely in the physically motivated notion that isomorphisms are the
foundational computational mechanism as well as the HoTT approach that is
essentially all about isomorphisms. Of course we don't lose anything by
restricting our attention to isomorphisms because we know that general
(irreversible) functions can be obtained from isomorphisms via
\emph{information effects}~\cite{James:2012:IE:2103656.2103667}.

We are witnessing a convergence of ideas from several distinct research
communities (physics, mathematics, and computer science) towards replacing
\emph{equalities} by \emph{isomorphisms}. The combined programme has sparked
a significant amount of research that unveiled new and surprising connections
between geometry, algebra, logic, and computation (see~\cite{baez2011physics}
for an overview of some of the connections).

In the physics community, Landauer~\cite{Landauer:1961,Landauer},
Feynman~\cite{springerlink:10.1007/BF02650179}, and others have interpreted
the laws of physics as fundamentally related to computation. The great
majority of these laws are formulated as equalities between different
physical observables which is unsatisfying: \emph{different} physical
observables should not be related by an \emph{equality}. It is more
appropriate to relate them by an \emph{isomorphism} that witnesses, explains,
and models the process of transforming one observable to the other.

In the mathematics and logic community, Martin-L\"of developed an extension
of the simply typed $\lambda$-calculus originally intended to provide a
rigorous framework for constructive
mathematics~\cite{citeulike:7374951}. This theory has been further extended
with \emph{identity types} representing the proposition that two terms are
``equal.'' (See~\cite{streicher,warren} for a survey.) Briefly speaking,
given two terms $a$ and $b$ of the same type $A$, one forms the type
$\texttt{Id}_A(a,b)$ representing the proposition that~$a$ and~$b$ are equal:
in other words, a term of type $\texttt{Id}_A(a,b)$ witnesses, explains, and
models the process of transforming $a$ to $b$ and vice-versa.

In the computer science community, the theory and practice of type
isomorphisms is well-established. Originally, such type isomorphisms were
motivated by the pragmatic concern of searching large libraries of functions
by providing one of the many possible isomorphic types for the desired
function~\cite{Rittri:1989:UTS:99370.99384}. More recently, type isomorphisms
have taken a more central role as \emph{the} fundamental computational
mechanism from which more conventional, i.e., irreversible computation, is
derived. In our own previous
work~\cite{James:2012:IE:2103656.2103667,rc2011,rc2012} we started with the
notion of type isomorphism and developed from it a family of programming
languages, $\Pi$ with various superscripts, in which computation is an
isomorphism preserving the information-theoretic entropy.

A major open problem remains, however: a higher-order extension of
$\Pi$. This extension is of fundamental importance in all the originating
research areas. In physics, it allows for quantum states to be viewed as
processes and processes to be viewed as states, such as with the
Choi-Jamiolkowski
isomorphism~\cite{choi1975completely,jamiolkowski1972linear}.  In mathematics
and logic, it allows the equivalence between different proofs of type
$\texttt{Id}_A(a,b)$ to itself be expressed as an isomorphism (of a higher
type) $\texttt{Id}_{\texttt{Id}_A(a,b)}(p,q)$. Finally, in computer science,
higher-order types allow code to abstract over other code fragments as well
as the manipulation of code as data and data as code.

Technically speaking, obtaining a higher-order extension requires the
construction of a \emph{closed category} from the underlying monoidal
category for~$\Pi$. Although the general idea of such a construction is
well-understood, the details of adapting it to an actual programming language
are subtle.  Our main novel technical device to achieving the higher-order
extension is a \emph{fractional type} which represents \emph{negative
information} and which is so named because of its duality with conventional
product types.

From the wikipedia page on homeomorphism: 
\begin{quote}
The intuitive criterion of stretching, bending, cutting and gluing back
together takes a certain amount of practice to apply correctly—it may not be
obvious from the description above that deforming a line segment to a point
is impermissible, for instance. It is thus important to realize that it is
the formal definition given above that counts.

This characterization of a homeomorphism often leads to confusion with the
concept of homotopy, which is actually defined as a continuous deformation,
but from one function to another, rather than one space to another. In the
case of a homeomorphism, envisioning a continuous deformation is a mental
tool for keeping track of which points on space X correspond to which points
on Y—one just follows them as X deforms. In the case of homotopy, the
continuous deformation from one map to the other is of the essence, and it is
also less restrictive, since none of the maps involved need to be one-to-one
or onto. Homotopy does lead to a relation on spaces: homotopy equivalence.

There is a name for the kind of deformation involved in visualizing a
homeomorphism. It is (except when cutting and regluing are required) an
isotopy between the identity map on X and the homeomorphism from X to Y.
\end{quote}

It is strange for homotopy type theory to be all about isomorphisms and then
not insist on isomorphisms between spaces.

If we focus on homeomorphisms, the higher-order space is a \emph{torsor}.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Intuitive Ideas and Examples} 
\label{sec:intuition}

%% the next figures are taken from Selinger's paper on graphical languages
%% for monoidal categories; if we use them make sure it's ok with him and
%% acknowledge him

Univalence says:
\[ 
(A \simeq B) \quad\simeq\quad (A \equiv B)
\]
where $\simeq$ is a strong form of isomorphism witnessed by functions from
$A$ to $B$ and vice versa that are inverses and $\equiv$ is the propositional
equality in type theoretic terms or a path (homotopy) in topological
terms. The axiom relates two notions that are a priori different: functions
and paths. However if we define functions from the outset as paths then there
is no need for this axiom.

So what would it take to have each function correspond to a path and
higher-order functions correspond to paths between paths etc.? Since paths
form an equivalence relation, the first immediate observation is that all
functions must be reversible. Formally we need the following properties of
paths to be satisfied by functions. (We write $\path$ for paths instead of
$\equiv$.)

\begin{itemize}
\item For each $A$, there is function $\id : A \path A$, 

\item for each function $f: A \path B$, there exists a function $\adjoint{f}
  : B \path A$, and

\item for each functions $f : A \path B$ and $g : B \path C$, there exists a
  function $g \cp f : A \path C$, such that:

\begin{itemize}
\item $f \path f \cp \id$;
\item $f \path \id \cp f$;
\item $\adjoint{f} \cp f \path \id$;
\item $f \cp \, \adjoint{f} \path \id$;
\item $\adjoint{(\adjoint{f})} \path f$;
\item $f \cp (g \cp h) \path (f \cp g) \cp h$
\end{itemize}
\end{itemize}
Similar equivalences hold are higher-levels. A good starting point for this
notion of functions are the $\Pi$-combinators we previously developed. Each
combinator in that setting had an \emph{adjoint} going in the other direction
that acts as the inverse. Moreover if $f : A \path B$ then $A$ must be
isomorphic to $B$ and $f$ is permutation. We use $!p$ for the inverse of a
path.

But first, let's examine the structure of a path $f : A \path B$. A natural
representation for a path representing a function is a collection of paths
(called \emph{fibers}) one for each $a : A$. So for example, if $A$ is the
set $\{ x , y , z \}$ and $B$ is the set $\{ a , b , c \}$ (remember that $A$
and $B$ must be isomorphic), and $f$ is the function mapping $x$ to $a$, $y$
to $b$, and $z$ to $c$, then $f : A \path B$ is the collection of paths $f_x
: x \path a$, $f_y : y \path b$, and $f_z : z \path c$.

Assuming this representation of functions, let's see what properties are
induced for these functions. 

The first property is that functions should preserve paths, i.e., if there is
a path between $x$ and~$y$ then there should be a path between $f(x)$
and~$f(y)$. From the figure below it is clear that:
\[ 
\ap{f}{p} = \, !f_x \pc p \pc f_y
\]

\begin{center}
\begin{tikzpicture}
  \draw (-3,0) ellipse (1.5cm and 3cm);
  \draw (3,0) ellipse (1.5cm and 3cm);
  \draw[fill] (-3,1.5) circle [radius=0.025];
  \draw[fill] (-3,-1.5) circle [radius=0.025];
  \node[above] at (-3,1.5) {$x$};
  \node[below] at (-3,-1.5) {$y$};
  \draw[fill] (3,1.5) circle [radius=0.025];
  \draw[fill] (3,-1.5) circle [radius=0.025];
  \node[above] at (3,1.5) {$f(x)$};
  \node[below] at (3,-1.5) {$f(y)$};
  \draw[->,cyan,thick] (-3,1.5) -- (-3,-1.5);
  \node[left,cyan] at (-3,0) {$p$};
  \draw[->,dashed,cyan,thick] (3,1.5) -- (3,-1.5);
  \node[right,cyan] at (3,0) {$\mathit{ap}~f~p$};
  \draw[->,red,thick] (-3,1.5) -- (3,1.5);
  \draw[->,red,thick] (-3,-1.5) -- (3,-1.5);
  \node[red,below] at (0,1.5) {$f_x$};
  \node[red,below] at (0,-1.5) {$f_y$};
\end{tikzpicture}
\end{center}

Let $p : x \path y$ and $q : y \path z$, then the following properties 
hold:
\begin{itemize}
\item $\ap{f}{(p \pc q)} \path \ap{f}{p} \pc \ap{f}{q}$:
\[\begin{array}{rcl}
LHS &=& \, !f_x \pc (p \pc q) \pc f_z \\
    &\path& ! f_x \pc p \pc f_y \pc \, ! f_y \pc q \pc f_z \\
    &\path& (! f_x \pc p \pc f_y) \pc (! f_y \pc q \pc f_z) \\
    &=& RHS
\end{array}\]
\item $\ap{f}{!p} \path \, !(\ap{f}{p})$
\[\begin{array}{rcl}
LHS &=& \, !f_y \pc (!p) \pc f_x \\
    &\path& \, !(!f_x \pc p \pc f_y) \\
    &=& RHS
\end{array}\]
\item $\ap{g}{(\ap{f}{p})} \path \ap{(g \cp f)}{p}$
\[\begin{array}{rcl}
LHS &=& \, !g_{f_x} \pc !f_x \pc p \pc f_y \pc g_{f_y} \\
    &\path& \, ! (f_x \pc g_{f_x}) \pc p \pc (f_y \pc g_{f_y}) \\
    &=& RHS
\end{array}\]
\item $\ap{\id}{p} \path p$
\[\begin{array}{rcl}
LHS &=& \, !\id_x \pc p \pc \id_y \\
    &\path& p \\
    &=& RHS
\end{array}\]
\end{itemize}

A homotopy between functions $f$ and $g$ is a 2-path between each pair of
fibers $f_x$ and $g_x$. These 2-paths are induced by the following diagram:

\begin{center}
\begin{tikzpicture}
  \draw[fill] (-3,0) circle [radius=0.025];
  \node[below] at (-3,0) {$x$};
  \draw[fill] (3,1.5) circle [radius=0.025];
  \node[above] at (3,1.5) {$a$};
  \draw[fill] (3,-1.5) circle [radius=0.025];
  \node[below] at (3,-1.5) {$b$};
  \draw[->,cyan,thick] (-3,0) -- (3,1.5);
  \draw[->,cyan,thick] (-3,0) -- (3,-1.5);
  \draw[->,red,thick] (3,1.5) -- (3,-1.5);
  \node[red,above] at (0,0.5) {$f_x$};
  \node[red,below] at (0,-0.5) {$f_y$};
  \draw[->,double,dashed,blue,thick] (1.5,1) to [out=225, in=135] (1.5,-1);
  \node[blue,right] at (1.5,0) {$H_x$};
\end{tikzpicture}
\end{center}

Here is something more interesting. Let $p : y \path z$ in $A$. Let $f$ and
$g$ be functions from $A$ to $B$. Let $H$ be a 2-path between $f_y$ and
$g_y$. If we are given a path $f(y) \path g(y)$ in B, then we can construct a
2-path between $f_z$ and $g_z$. (This is Thm 2.11.3 in the book.) We do this
going backwards along $f_z$, backwards along $p$, then follow $f_y$ and the
path to $g(y)$, and backwards along $g_y$, forwards along $p$, and finally
forwards along $g_z$:

\begin{center}
\begin{tikzpicture}
  \draw[fill] (-3,0) circle [radius=0.025];
  \node[below] at (-3,0) {$x$};
  \draw[fill] (3,1.5) circle [radius=0.025];
  \node[above] at (3,1.5) {$a$};
  \draw[fill] (3,-1.5) circle [radius=0.025];
  \node[below] at (3,-1.5) {$b$};
  \draw[->,cyan,thick] (-3,0) -- (3,1.5);
  \draw[->,cyan,thick] (-3,0) -- (3,-1.5);
  \draw[->,red,thick] (3,1.5) -- (3,-1.5);
  \node[red,above] at (0,0.5) {$f_x$};
  \node[red,below] at (0,-0.5) {$f_y$};
  \draw[->,double,dashed,blue,thick] (1.5,1) to [out=225, in=135] (1.5,-1);
  \node[blue,right] at (1.5,0) {$H_x$};
  \draw[fill] (-3,-5) circle [radius=0.025];
  \node[below] at (-3,-5) {$x$};
  \draw[fill] (3,-3.5) circle [radius=0.025];
  \node[above] at (3,-3.5) {$a$};
  \draw[fill] (3,-6.5) circle [radius=0.025];
  \node[below] at (3,-6.5) {$b$};
  \draw[->,cyan,thick] (-3,-5) -- (3,-3.5);
  \draw[->,cyan,thick] (-3,-5) -- (3,-6.5);
  \draw[->,red,thick] (3,-3.5) -- (3,-6.5);
  \node[red,above] at (0,-4.5) {$f_x$};
  \node[red,below] at (0,-5.5) {$f_y$};
\end{tikzpicture}
\end{center}

Now the most interesting question is whether we can internalize functions as
objects. Given $f$ a function from $A$ to $B$, what we can do below is to
represent each fiber $f_x$ as an element of the type $(\frac{1}{A} \times
B)$. As an example, let $A$ be the set $\{x,y,z\}$ and let $B$ be
$\{a,b,c\}$, the type $\frac{1}{A}$ has one element $\frac{1}{3}$ which is
one point that has three self loops labeled $x \path$, $y \path$, and $z
\path$. A value $(\frac{1}{3},a)$ is a fiber of the function that produces
$a$ as the second component indicates. The first component states that the
$a$ could have come from $x$ along the path $x \path$, or from $y$ along the
path $y \path$ or from $z$ along the path $z \path$.






\newpage

What can we say in pi about these two combinators:
\begin{verbatim}
Let f : A -> C and G : B -> D

(id x g) o (f x id)  :  A x B -> C x D

(f x id) o (id x g)  :  A x B -> C x D
\end{verbatim}
Are they the ``same''? We can reason extensionally to check that for all
inputs these two combinators produce the same results. In other words, we
reason from the axioms of category theory which includes things like
\verb|f o id = f| which are extensional equalities. (If we had weak
$n$-categories here what would happen, perhaps this is where we are leading
with the next sentence.) Better is to reason topologically exploiting the
original connections established by Joyal and
Street~\cite{planardiagrams,geometrytensor}. One can in this case show the
equivalence of these combinators by using the graphical language and noticing
that there is a \emph{planar isotopy} between the two diagrams, that moves
things around without crossing, cutting, or gluing any wires. 

More formally, we view each type as a topological space and each function as
a deformation of the space expressed as a (sequential, parallel, etc.)
composition of primitive deformations (id, swap, unit, assoc, distribute,
factor, etc.). If we have a planar monoidal category, then there isn't much
you can do: the types are collections of lines grouped in bundles. The only
deformations that functions can do are to re-associate the bundles and get
rid of unit wires. (If the ambient space is a plane, i.e., if we restrict our
``hardware model'' to be a 2D model in which wires can't cross over each
other, then we can't even equate the functions that apply id to different
bundles. If the ambient space is 3D then we can. Eq. 3.2 in Selinger's survey
of graphical languages for monoidal categories.) An example of two functions
we can show to be the same in the planar model is the one above in the
verbatim block. An isotopy exists between the two combinators because we can
move things around in the plane as long as we don't cross or cut any wires.

If we allow braiding (i.e, commutativity) we must move to ambient isotopies
in 3D. In particular, the two versions of not that cross true over false or
vice versa are not isotopic.

If we also want, the composition of not and not to be expressible directly as
a twist, we must move to \emph{framed} isotopies in 3 dimensions, where the
lines are represented as flat ribbons.

A symmetric monoidal category requires ambient isotopy in 4 dimensions so
we're not going to consider it.

If we are going to have higher-order functions, we need to move up, i.e., we
need to build a space in which the types are the functions of the lower
level, and in which the functions are the isotopies of the lower level. In
other words, we need to be able to express the lower level functions as
topological spaces and we need to be able to express the lower level
isotopies as functions. 

Think of a function as a map connecting points from one space to points in
the other space (respecting paths etc.). This map gives a geometric shape. We
will think of one line in that shape as solid with all the other lines dashed.

Another unrelated observation is that Pi gives us an inductive
characterization of functions! If that whole thing with fractionals
works out we will have an inductive characterization of higher-order
functions! 

In homotopy type theory, there is a focus on isomorphisms: for most of the
spaces an isomorphism between $A$ and $B$ is represented by a path denoting a
particular proof of the identify $A \equiv B$. Different proofs yield
different paths and these proofs can be related by 2-paths to reason about
proof equivalence and so on. Yet in the middle of all these identities and
isomorphisms, conventional homotopy type theory deals with arbitrary
functions, then defines what it means \emph{extensionally} for functions to
be isomorphic, and \emph{then} postulates an axiom that extensionally
equivalent functions are identical in the sense of having a path between
them. This treatment gives no insight about the nature paths between
functions and is undesirable for many reasons. 

We propose to just consider functions that are isomorphisms by
construction. This doesn't lose anything in terms of computability because we
know that we could do everything with reversible functions if we wanted
to. There are actually many advantages of doing so as we and others have
argued at length before. Anyway, the point is that if we have
isomorphisms-by-construction functions then the function itself becomes
naturally a collection of paths. We illustrate this point with examples.

Consider the function $\notb$ from the space $\boolt$ to itself. We can
represent this function as a pair of paths. Since we are in a topological
world, we should care about how the paths cross over each other.  In the
diagram below, we chose for the top path to cross over the bottom one:
\begin{center}
  \begin{tabular}{@{}llc@{}}
    $\notb : \boolt \rightarrow \boolt$ & & 
    $\vcenter{\wirechart{@C=1.5cm@R=0.8cm}{
        *{}\wireright{r}{\ffv}&\blank\wirecross{d}\wireright{r}{\ffv}&\\
        *{}\wireright{r}{\ttv}&\blank\wirebraid{u}{.3}\wireright{r}{\ttv}&
        }}$ 
  \end{tabular}
\end{center}
It is important to note that the two paths must be taken together
because there is a constraint between them. If the top path takes $\ffv$ to
$\ttv$ then the bottom path cannot take $\ttv$ to $\ttv$: it \emph{has} to
lead to $\ffv$. In other words, it is incorrect to focus only on the top path
and conclude that there is an identity between $\ffv$ and $\ttv$. What is
correct is that, collectively, there is an identity between $\boolt$ and
$\boolt$ that permutes the elements of $\boolt$. Technically we have a
\emph{braid}. 

We will return to this point later. But for now, consider the functions:
\[\begin{array}{rcl}
\idc^1 &=& \lambda x.x \\
\idc^2 &=& \lambda x. \notb~(\notb~x)
\end{array}\]
These two functions are evidently extensionally equivalent and hence in the
conventional treatment of homotopy type theory, they are also treated as
propositionally equivalent by the function extensionality axiom. When the
functions themselves are represented as paths, however, we get the following
situation for the second function:
\[
\idc^2 = \lambda x.\notb~(\notb~x) \qquad
\vcenter{\wirechart{@C=1.5cm@R=0.8cm}{
    *{}\wireright{r}{\ffv}&
    \blank\wirecross{d}\wireright{r}{\ffv}&
    \blank\wirecross{d}\wireright{r}{\ffv}&
    \\
    *{}\wireright{r}{\ttv}&
    \blank\wirebraid{u}{.3}\wireright{r}{\ttv}&
    \blank\wirebraid{u}{.3}\wireright{r}{\ttv}&
    \\
    }}
\]
Repeating the $\notb$ operation results in a twisted braid that extensionally
behaves like the trivial braid but that is evidently not identical to
it. Formally to find a (2-)path between the functions requires us to find an
\emph{isotopy} between the two braids, where loosely speaking an isotopy is
essentially homotopy in the case of bijections. The two braids for $\idc^1$
and $\idc^2$ are \emph{not} isotopic so there is no path between them in our
world. What is interesting is that the braid isotopy problem has efficient
solutions and hence we are in a situation where function equivalence has
efficient algorithms.

Note that one can define another version of boolean negation $\notb'$ in
which the bottom path is the one that crosses over the top one. Using this
version, the function $\idc^3 = \lambda x.\notb'~(\notb~x)$ would look like:
\[
\idc^3 = \lambda x.\notb'~(\notb~x) \qquad
\vcenter{\wirechart{@C=1.5cm@R=0.8cm}{
     *{}\wireright{r}{\ffv}&
     \blank\wirecross{d}\wireright{r}{\ffv}&
     \blank\wirebraid{d}{.3}\wireright{r}{\ffv}&
     \\
     *{}\wireright{r}{\ttv}&
     \blank\wirebraid{u}{.3}\wireright{r}{\ttv}&
     \blank\wirecross{u}\wireright{r}{\ttv}&
     \\
     }}
\]
And this version is isotopic to the trivial braid, and hence we would have a
(2-)path between $\idc^1$ and $\idc^3$.

To summarize, if we restrict our attention to a certain class of functions,
these functions are naturally described as braids and function equivalence
(i.e, paths between functions) are generated by braid isotopy. This is
already quite neat but note that we have only talked about functions
\emph{between} spaces and modeled these as braids. What we have not done yet
is describe the space of functions itself. In our running example, we need to
describe some space $\boolt \lolli \boolt$ that represents the various
functions we discussed from $\boolt$ to $\boolt$.

%%%%%%%%%%%%%%%%%
\subsection{Pointed Spaces} 

We will construct this in steps. First we note that a function is a ``large''
object that can be applied to many possible arguments. Each application is
however associated with exactly one argument. Thus, in this first step, we do
not model functions in their entirety; we only model functions \emph{at one
  particular point}. We will return to the issue of modeling the entire
function object later. For now, we have technically moved from \emph{spaces}
to \emph{pointed spaces}. Let's revisit our previous discussion from the
perspective of pointed spaces.

The type $\boolt$ is now split in two types: the type $(\boolt,\ffv)$ with
$\ffv$ as the distinguished point and $(\boolt,\ttv)$ with $\ttv$ as the
distinguished point. We now have two copies of the function $\notb$, a
version $\notb_{\ffv} : (\boolt,\ffv) \rightarrow (\boolt,\ttv)$ and a
version $\notb_{\ttv} : (\boolt,\ttv) \rightarrow (\boolt,\ffv)$ depending on
the starting basepoint. Indeed functions must respect the basepoints, i.e.,
map basepoints to basepoints. The function is still a braid on the complete
$\boolt$ space but in the first case, the distinguished point $\ffv$ tells us
that the function is ``applied'' to $\ffv$ and hence that the top branch is
the one in focus.

Concretely then we want spaces (i.e., groupoids) $(\boolt,\ffv) \lolli
(\boolt,\ffv)$, $(\boolt,\ffv) \lolli (\boolt,\ttv)$, $(\boolt,\ttv) \lolli
(\boolt,\ffv)$, and $(\boolt,\ttv) \lolli (\boolt,\ttv)$. As examples, the
first space will contain $\idc^1_{\ffv}$ and $\idc^3{\ffv}$; the second space
will contain $\notb_{\ffv}$ and $\notb'_{\ffv}$; the third space will contain
$\notb_{\ttv}$, and the last space will contain $\idc^1_{\ttv}$. In the first
space, there will be a path between $\idc^1_{\ffv}$ and $\idc^3{\ffv}$ as
there is an isotopy between them etc. To describe these spaces fully, we need
introduction rules, elimination rules, computation rules, and induction
principles, etc. It should be clear that we can't just use
$\lambda$-expressions as introduction rules: they are not refined enough to
capture all the invariants we want.

Let's start with some basic observations. How many points (i.e., functions or
braids) are there in the space $(\boolt,\ffv) \lolli (\boolt,\ffv)$. These
are all the twists on two elements with the paths starting and ending at
$\ffv$ highlighted: by giving a twist in one direction the value $+1$ and a
twist in the other direction the value $-1$, we see that this is isomorphic
to the integers under addition. We would like to argue that this space has
groupoid cardinality 1 and if we succeed then it is natural to think of it as
the product of a space with fractional cardinality $\frac{1}{2}$ and the
space $\boolt$ with cardinality 2. Think of all the words over the alphabet
$\{ 0, 1, -1\}$ with rules $0x\rightarrow x$, $x0\rightarrow x$,
$1(-1)\rightarrow\epsilon$ and $(-1)1\rightarrow\epsilon$. This produces
equivalence classes which describe the connected components (isotopy
equivalences) of the space $\boolt\lolli\boolt$. Let's denote by $V_n$ the
size of the equivalence class of words whose value is $n$ where the value is
the sum of the elements. The groupoid cardinality of the space is therefore
$\Sigma_{n\in\mathbb{Z}} \frac{1}{A_n}$. Does this thing have value 1???
Plausible. Assume yes for now and proceed under the assumption that it is 1
and hence that it makes sense to decompose the space into the product of
something of cardinality $\frac{1}{2}$ and something of cardinality $2$. So
what kind of groupoid would have cardinality $\frac{1}{2}$. This actually is
something well studied. Talk about groupoid cardinality and give an example
of how the cardinality of a group of order $n$ is $\frac{1}{n}$. Some
intuition about the paths reducing the number of elements and the Euler
characteristic.

%%%%%%%%%%%%%%%%%
\subsection{Fractionals} 

As an example, let's focus now on building the type
$\frac{1}{(\boolt,\ffv)}$: it will correspond to the braid group $\br_2$ on
two strands. This type will have an infinite number of points each
representing one element of the braid group $\br_2$. Mathematically, for $n$
strands, the braid group $\br_n$ is generated by $\sigma_1, \ldots,
\sigma_{n-1}$ and the following relations:
\begin{itemize}
\item $\sigma_i\sigma_{i+1}\sigma_i = \sigma_{i+1}\sigma_{i}\sigma_{i+1}$, 
\item $\sigma_i\sigma_j = \sigma_j\sigma_i$ if $|i-j| \geq 2$.
\end{itemize}
So for the particular case of $\br_2$, we have one generator $\sigma$ and no
relations. The generator corresponds to one non-trivial twist in one
direction. The group elements (i.e., the elements of
$\frac{1}{(\boolt,\ffv)}$) are the trivial braid, the $n$-fold compositions
of $\sigma$ for all $n$, and the $n$-fold compositions of $\sigma^{-1}$ for
all $n$. 

So generally speaking $\eta_n$ will produce a product of $\br_n$ and $n$ and
$\epsilon_n$ will be the group action of the group on $\br_n$ on the
particular strand $n$. A function will have a particular wiring; this wiring
is reflected as a first class value using the group generators. For booleans,
the group generators can be represented as id, not, and not'; every wiring is
a sequence of these. So values of type $1/bool$ are (id), (not o not'), (not'
o not'), (not o not o not), etc. or in other words the code for the circuits
becomes represented as a value. (Is that related to the encode/decode method
in the HoTT book?) How about functions: T1 -> T2. The types T1 and T2 must be
connected by paths so we might as well think about T1 -> T1.

So B has value f and t
1/B has values id; not; not'; and their compositions (semantically
represented as elements of the group Br2. 

eta : (1,()) -> ((B,1/B),(f,id))
eta () = (f , id)

eta : (1,()) -> ((B,1/B),(f,not))
eta () = (t , not)

...

epsilon : ((B,1/B),(f,not)) -> (1,())
epsilon (t , not) = ()

...


%%%%%%%%%%%%%%%%%
\subsection{Negatives?} 

Need operations to change the basepoint. Would these be the negatives?

%% \begin{center}
%%   \begin{tabular}{@{}llc@{}}
%%     Braiding & $\sym_{A,B}$ &
%%     $\vcenter{\wirechart{@C=1.5cm@R=0.8cm}{
%%         *{}\wireright{r}{B}&\blank\wirecross{d}\wireright{r}{A}&\\
%%         *{}\wireright{r}{A}&\blank\wirebraid{u}{.3}\wireright{r}{B}&
%%         }}$ \\
%%   \end{tabular}
%% \end{center}

%% Note that the braiding satisfies
%% $\sym_{A,B}\cp\symi_{A,B}=\id_{A\x B}$, but not
%% $\sym_{A,B}\cp\sym_{B,A}=\id_{A\x B}$. Graphically:

%% \[\vcenter{\wirechart{@C=1.5cm@R=0.8cm}{
%%     *{}\wireright{r}{B}&
%%     \blank\wirecross{d}\wireright{r}{A}&
%%     \blank\wirebraid{d}{.3}\wireright{r}{B}&
%%     \\
%%     *{}\wireright{r}{A}&
%%     \blank\wirebraid{u}{.3}\wireright{r}{B}&
%%     \blank\wirecross{u}\wireright{r}{A}&
%%     \\
%%     }}
%% = \id_{A\x B},
%% \]
%% \[\vcenter{\wirechart{@C=1.5cm@R=0.8cm}{
%%     *{}\wireright{r}{B}&
%%     \blank\wirecross{d}\wireright{r}{A}&
%%     \blank\wirecross{d}\wireright{r}{B}&
%%     \\
%%     *{}\wireright{r}{A}&
%%     \blank\wirebraid{u}{.3}\wireright{r}{B}&
%%     \blank\wirebraid{u}{.3}\wireright{r}{A}&
%%     \\
%%     }}
%% \neq \id_{A\x B}.
%% \]

%% \begin{example}
%%   The hexagon axiom translates into the following in the graphical
%%   language:

%%   \[ (\id_B\x\sym_{A,C}) \cp \alpha_{B,A,C} \cp (\sym_{A,B}\x\id_C)
%%   = \alpha_{B,C,A} \cp (\sym_{B,C\x A}) \cp \alpha_{A,B,C}
%%   \]
%%   \[\vcenter{\wirechart{@R=6mm}{
%%     \wireright{r}{C}&
%%     \wireid\wireright{r}{C}&
%%     \blank\wirecross{d}{.3}\wireright{r}{A}&
%%     \\
%%     \wireright{r}{B}&
%%     \blank\wirecross{d}{.3}\wireright{r}{A}&
%%     \blank\wirebraid{u}{.3}\wireright{r}{C}&
%%     \\
%%     \wireright{r}{A}&
%%     \blank\wirebraid{u}{.3}\wireright{r}{B}&
%%     \wireid\wireright{r}{B}&
%%     \\
%%     }}
%%   \ssep=\ssep
%%   \vcenter{\wirechart{@R=6mm}{
%%     \wireright{r}{C}&
%%     \blank\wirecross{d}{.3}\wireright{r}{A}&
%%     \\
%%     \wireright{r}{B}&
%%     \blank\wirecross{d}{.3}\wireright{r}{C}&
%%     \\
%%     \wireright{r}{A}&
%%     \blank\wirebraid{uu}{.2}\wireright{r}{B}&
%%     \\
%%     }}
%%   \]
%% \end{example}

%% \begin{example}
%%   The {\em Yang-Baxter equation} is the following equation, which is a
%%   consequence of the hexagon axiom and naturality:
%%   \[ (\sym_{B,C}\x\id_A)\cp(\id_B\x\sym_{A,C})\cp(\sym_{A,B}\x\id_C) =
%%   (\id_C\x\sym_{A,B})\cp(\sym_{A,C}\x\id_B)\cp(\id_A\x\sym_{B,C}).
%%   \]
%%   In the graphical language, it becomes:
%%   \[\vcenter{\wirechart{@C-4mm@R=6mm}{
%%     \wireright{r}{C}&
%%     \wireid\wireright{r}{C}&
%%     \blank\wirecross{d}{.3}\wireright{r}{A}&
%%     \wireid\wireright{r}{A}&
%%     \\
%%     \wireright{r}{B}&
%%     \blank\wirecross{d}{.3}\wireright{r}{A}&
%%     \blank\wirebraid{u}{.3}\wireright{r}{C}&
%%     \blank\wirecross{d}{.3}\wireright{r}{B}&
%%     \\
%%     \wireright{r}{A}&
%%     \blank\wirebraid{u}{.3}\wireright{r}{B}&
%%     \wireid\wireright{r}{B}&
%%     \blank\wirebraid{u}{.3}\wireright{r}{C}&
%%     \\
%%     }}
%%   \ssep=\ssep
%%   \vcenter{\wirechart{@C-4mm@R=6mm}{
%%     \wireright{r}{C}&
%%     \blank\wirecross{d}{.3}\wireright{r}{B}&
%%     \wireid\wireright{r}{B}&
%%     \blank\wirecross{d}{.3}\wireright{r}{A}&
%%     \\
%%     \wireright{r}{B}&
%%     \blank\wirebraid{u}{.3}\wireright{r}{C}&
%%     \blank\wirecross{d}{.3}\wireright{r}{A}&
%%     \blank\wirebraid{u}{.3}\wireright{r}{B}&
%%     \\
%%     \wireright{r}{A}&
%%     \wireid\wireright{r}{A}&
%%     \blank\wirebraid{u}{.3}\wireright{r}{C}&
%%     \wireid\wireright{r}{C}&
%%     \\
%%     }}
%%   \]
%% \end{example}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{The Category of Pointed Groupoids}

%%%%%%%%%%%%%%%%%
\subsection{Paths} 

\begin{definition}[Path]
A \emph{path} $p : x \path y$ between two points $x$ and $y$ in some space
$A$ is a directed edge $p$ from $x$ to $y$. We denote the set of paths of the
space $A$ as $\paths{A}$.
\end{definition}

\begin{definition}[Disjoint union of paths]
Given $\paths{A}$ and $\paths{B}$ in spaces $A$ and $B$ respectively, we
construct $\paths{A} \uplus^p \paths{B}$ in space $A \uplus B$, the disjoint
union of $A$ and $B$, as follows:
\[ 
  \{ \leftv{p} : \leftv{x} \path \leftv{y} ~|~ 
    (p : x \path y) \in \paths{A} \}
  \union
  \{ \rightv{q} : \rightv{x} \path \rightv{y} ~|~ 
    (q : x \path y) \in \paths{B} \}
\]
\end{definition}
We will sometimes write this as $\leftv{(\paths{A})} \union
\rightv{(\paths{B})}$.

\begin{definition}[Product of paths]
Given $\paths{A}$ and $\paths{B}$ in spaces $A$ and $B$
respectively, we construct $\paths{A} \times^p \paths{B}$ in
space $A \times B$, the cartesian product of $A$ and $B$, as follows: 
\[ 
\{ (p,q) : (x,z) \path (y,w) ~|~ (p : x \path y) \in \paths{A}, 
   (q : z \path w) \in \paths{B} \}
\]
\end{definition}
We will sometimes write this as $(\paths{A},\paths{B})$.

%%%%%%%%%%%%%%%%%
\subsection{Pointed Groupoids} 

\begin{definition}[Groupoid]
A \emph{groupoid} $G = (G_0, \paths{G_0})$ is a set $G_0$ together
with a collection of paths $x \path y$, between elements $x$ and $y$ of $G_0$
that satisfies the following conditions:
\begin{itemize}
\item for every $x \in G_0$, there is a path $\refl_x : x \path x$,
\item every path $p : x \path y$, there is an inverse path $! p : y \path x$, 
\item for every paths $p : x \path y$ and $q : y \path z$ there is a path $p
  \circ q : x \path z$, and
\item for every paths $p : x \path y$, $q : y \path z$, and $r : z \path w$,
  we have:
  \begin{itemize}
  \item $\refl_x \circ p = p$;
  \item $p \circ \refl_y = p$;
  \item $(p \circ q) \circ r = (p \circ (q \circ r))$;
  \item $p \,\circ\, !p = \refl_x$;
  \item $!p \,\circ\, p = \refl_y$.
  \end{itemize}
\end{itemize}
\end{definition}
When introducing a groupoid, we only explicitly mention a collection of
non-trivial ``generating'' paths. The equivalence closure under $\refl$, $!$,
and $\circ$ with the appropriate conditions is implicitly
assumed.\footnote{For higher groupoids, the five equivalences in the last
  condition will be witnessed by paths between paths and not by the
  extensional equivalence relation $=$.}

\begin{definition}[Pointed groupoid]
A pointed groupoid $G_{\bullet} = (G_0, \bot_{G_0}, \paths{G_0})$ is
a groupoid $(G_0, \paths{G_0})$ with a distinguished element
$\bot_{G_0} \in G_0$.
\end{definition}

\begin{definition}[Wedge sum]
The \emph{wedge sum} of two pointed groupoids $G_\bullet$ and $H_\bullet$,
written $G_\bullet \wedgesum H_\bullet$ is defined as follows:
\[\begin{array}{l}
(G_0, \bot_{G_0}, \paths{G_0}) \wedgesum 
(H_0, \bot_{H_0}, \paths{H_0}) = \\
((G_0 \uplus H_0) \union \{ \bot \},
 \bot,
 (\paths{G_0} \uplus^p \paths{H_0}) \union
 \{ L: \leftv{\bot_{G_0}} \path \bot, 
    R: \rightv{\bot_{H_0}} \path \bot \})
\end{array}\]
where $\uplus$ is the disjoint union operation on sets and $\bot$ is a new
distinguished element that is related by new paths to the distinguished
elements of $G_\bullet$ and $H_\bullet$.
\end{definition}

\begin{definition}[Smash product]
The \emph{smash product} of two pointed groupoids $G_\bullet$ and
$H_\bullet$, written $G_\bullet \smashproduct H_\bullet$ is defined as
follows:
\[\begin{array}{l}
(G_0, \bot_{G_0}, \paths{G_0}) \smashproduct
(H_0, \bot_{H_0}, \paths{H_0}) = \\
((G_0 \times H_0) \union \{ \bot \},
 \bot,
 (\paths{G_0} \times^p \paths{H_0}) \union
 \{ F_h: (\bot_{G_0},h) \path \bot \} \union 
 \{ S_g: (g,\bot_{H_0}) \path \bot \} 
\end{array}\]
where $\times$ is the cartesian product operation on sets and $\bot$ is a new
distinguished element that is related by new paths to every pair of elements
that includes either $\bot_{G_0}$ or $\bot_{H_0}$. 
\end{definition}

\begin{definition}[Denotation of types]
Each type $b$ is mapped to a \emph{pointed groupoid} $(\dt{b}, \bot_b,
\paths{b})$ as follows:
\[\begin{array}{rcl@{\qquad}l}
\dt{0} &=& (\{ \bot_0 \}, \bot_0, \{ \mathit{loop}_0 : \bot_0 \path \bot_0 \}) &
           (\mbox{circle}) \\
\dt{1} &=& (\{ \bullet, \bot_1 \}, \bot_1, 
           \{ \mathit{loop}_1 : \bot_1 \path \bot_1 \}) &\\
\dt{(b_1 + b_2)} &=& \dt{b_1} \wedgesum \dt{b_2} & 
           (\mbox{wedge~sum}) \\
\dt{(b_1 * b_2)} &=& \dt{b_1} \smashproduct \dt{b_2} & 
           (\mbox{smash~product})
\end{array}\]
\end{definition} 

Topologically $\dt{0}$ corresponds to the circle $S^1$ which has Euler
characteristic (which generalizes the notion of set cardinality) of 0. As a
groupoid, the space $\dt{0}$ includes this infinite collection of paths from
$\bot_0 \path \bot_0$:
\[\begin{array}{l}
\refl_{\bot_0} \\
\mathit{loop}_0 \\
!~\mathit{loop}_0 \\
\mathit{loop}_0 \circ \mathit{loop}_0 \\
!~(\mathit{loop}_0 \circ \mathit{loop}_0) \\
\mathit{loop}_0 \circ \mathit{loop}_0 \circ \mathit{loop}_0 \\
!~(\mathit{loop}_0 \circ \mathit{loop}_0 \circ \mathit{loop}_0) \\
\vdots
\end{array}\]
and hence, using the definition introduced by Baez and
Dolan~\cite{groupoidcard}, has groupoid cardinality 0. We will abbreviate
this collection of paths as $\mathit{loop}^n_0$ for integer $n$, where
$\mathit{loop}^0_0$ is $\refl$, and $\mathit{loop}^n_0$ abbreviates the
$n$-fold composition in one direction for positive $n$ and in the opposite
direction for negative $n$.

Note that all our pointed spaces have a similar structure: a collection of
``regular elements'' forming several connected components and a separate
isolated connected component that includes the distinguished element
$\bot$. The distinguished element $\bot$ has the infinite collection of loops
on it and, in general, may be connected to the distinguished elements of the
subspaces used in the construction. That entire cluster including $\bot$ has
Euler characteristic and groupoid cardinality 0.

We now check that the wedge sum of any of our pointed groupoids $G_\bullet$
with $\dt{0}$ is ``essentially'' $G_\bullet$ itself, i.e., that $\dt{0}$ is
the additive unit in our space of pointed groupoids. Consider:
\[\begin{array}{l}
G_\bullet \wedgesum \dt{0} = \\
(G_0, \bot_{G_0}, \paths{G_0}) \wedgesum 
  (\{ \bot_0 \}, \bot_0, \{ \mathit{loop}_0 : \bot_0 \path \bot_0 \}) = \\
((\leftv{G_0} \union \{ \rightv{\bot_0}, \bot \}, 
 \bot,
 (\leftv{\paths{G_0}} \union \{ \rightv{\mathit{loop}^n_0} , 
 \leftv{\bot_{G_0}} \path \bot, \rightv{\bot_0} \path \bot \})
\end{array}\]
One can see that this space consists of $\leftv{G_0}$ with whatever structure
is on it and another connected component consisting of $\leftv{\bot_{G_0}}$,
$\rightv{\bot_0}$, and the new $\bot$ for the entire space. This cluster has
cardinality 0 and hence the new space is ``equivalent'' to the original
$G\bullet$ as we have essentially only changed the representation of 0. 

Therefore, since the wedge sum is evidently commutative and associative, it
is at least plausible that the structure $(\wedgesum, \dt{0}$ is a symmetric
monoidal category. All of that will be formalized later. The categorical
morphisms must obviously map distinguished elements to distinguished elements
and preserve the structure of the path. It is also reasonably easy to see
that the structure $(\smashproduct, \dt{1})$ is another symmetric monoidal
category. Even better one can check that for any pointed groupoid
$G_\bullet$, we have $G_\bullet \smashproduct \dt{0}$ gives us a very
complicated 0 but still a 0. I didn't check distributivity but I suspect it
holds too.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Finite Types as Pointed Groupoids} 

We review our language $\Pi$ providing the necessary background and context
for our higher-order extension.\footnote{The presentation in this section
  focuses on the simplest version of $\Pi$. Other versions include recursive
  types and trace operators but these extensions are orthogonal to the
  higher-order extension emphasized in this document.} Even though the
semantics of $\Pi$ could be explained using plain sets, we express it using
the groupoid terminology to facilitate the transition to fractionals and
higher-order functions. 

%%%%%%%%%%%%%%%%%
\subsection{Syntax and Types} 

The terms of $\Pi$ are not classical values and functions; rather, the terms
are isomorphism witnesses.  In other words, the terms of $\Pi$ are proofs
that certain ``shapes of values'' are isomorphic.  And, in classical
Curry-Howard fashion, our operational semantics shows how these proofs can be
directly interpreted as actions on ordinary values which effect this shape
transformation. Of course, ``shapes of values'' are very familiar already:
they are usually called \emph{types}.  But frequently one designs a type
system as a method of classifying terms, with the eventual purpose to show
that certain properties of well-typed terms hold, such as safety.  Our
approach is different: we start from a type system, and then present a term
language which naturally inhabits these types, along with an appropriate
operational and denotational semantics.

\paragraph*{Data.}
We view $\Pi$ as having two levels: it has traditional values classified by
ordinary types:
\[\begin{array}{rcl} 
\textit{values}, v &::=& () \alt \leftv{v} \alt \rightv{v} \alt (v,v) \\
\textit{value types}, b &::=& 0 \alt 1 \alt b+b \alt b * b
\end{array}\]

Types include the empty type $0$, the unit type $1$, sum types $b_1+b_2$, and
product types $b_1*b_2$.  Values include $()$ which is the only value of type
$1$, $\leftv{v}$ and $\rightv{v}$ which inject $v$ into a sum type, and
$(v_1,v_2)$ which builds a value of product type.

\paragraph*{Isomorphisms.} The terms of $\Pi$ witness
type isomorphisms of the form $b \iso b$. They consist of base isomorphisms,
as defined below, and their composition.
\[\begin{array}{rrcll}
\identlp :&  0 + b & \iso & b &: \identrp \\
\swapp :&  b_1 + b_2 & \iso & b_2 + b_1 &: \swapp \\
\assoclp :&  b_1 + (b_2 + b_3) & \iso & (b_1 + b_2) + b_3 &: \assocrp \\
\identlt :&  1 * b & \iso & b &: \identrt \\
\swapt :&  b_1 * b_2 & \iso & b_2 * b_1 &: \swapt \\
\assoclt :&  b_1 * (b_2 * b_3) & \iso & (b_1 * b_2) * b_3 &: \assocrt \\
\distz :&~ 0 * b & \iso & 0 &: \factorz \\
\dist :&~ (b_1 + b_2) * b_3 & \iso & (b_1 * b_3) + (b_2 * b_3)~ &: \factor
\end{array}\]

Each line of the above table introduces a pair of dual
constants\footnote{where $\swapp$ and $\swapt$ are self-dual.} that witness
the type isomorphism in the middle.  These are the base (non-reducible) terms
of the second, principal level of $\Pi$. Note how the above has two readings:
first as a set of typing relations for a set of constants. Second, if these
axioms are seen as universally quantified, orientable statements, they also
induce transformations of the (traditional) values. The (categorical or
homotopical) intuition here is that these axioms have computational content
because they witness isomorphisms rather than merely stating an extensional
equality.

The isomorphisms are extended to form a congruence relation by adding the
following constructors that witness equivalence and compatible closure:

\begin{table}[t]
\hrule\medskip
\begin{center} 
\Rule{}
{}
{\jdg{}{}{\idc : b \iso b}}
{}
\quad 
\Rule{}
{\jdg{}{}{c : b_1 \iso b_2}}
{\jdg{}{}{\symc{c} : b_2 \iso b_1}}
{}
\quad
\Rule{}
{\jdg{}{}{c_1 : b_1 \iso b_2} \quad c_2 : b_2 \iso b_3}
{\jdg{}{}{c_1 \fatsemi c_2 : b_1 \iso b_3}}
{}
\\ \bigskip
\Rule{}
{\jdg{}{}{c_1 : b_1 \iso b_2} \quad c_2 : b_3 \iso b_4}
{\jdg{}{}{c_1 \oplus c_2 : b_1 + b_3 \iso b_2 + b_4}}
{}
\quad 
\Rule{}
{\jdg{}{}{c_1 : b_1 \iso b_2} \quad c_2 : b_3 \iso b_4}
{\jdg{}{}{c_1 \otimes c_2 : b_1 * b_3 \iso b_2 * b_4}}
{}
\end{center}
\caption{Combinators\label{pi-combinators}}
\medskip\hrule
\end{table}

It is important to note that ``values'' and ``isomorphisms'' are completely
separate syntactic categories which do not intermix. The semantics of the
language come when these are made to interact at the ``top level'' via
\emph{application}: 
\[\begin{array}{lrcl}
\textit{top level term}, l &::=& c~v
\end{array}\]

%%%%%%%%%%%%%%%%%
\subsection{Groupoid Semantics}

The language presented above, at the type level, models a \emph{commutative
  semiring} (occasionally called a \emph{commutative rig}) where we replace
equality by isomorphism.  Semantically, $\Pi$ models a \emph{bimonoidal
  category} whose simplest example is the category of finite sets and
bijections. In that interpretation, each value type denotes a finite set of a
size calculated by viewing the types as natural numbers and each combinator
$c : b_1 \iso b_2$ denotes a bijection between the sets denoted by $b_1$ and
$b_2$. Instead of presenting such a semantics, we present a more involved
semantics using groupoids. 

The semantics of $\Pi$ is given using two mutually recursive interpreters:
one going forward and one going backwards. The use of $\symc{}$ switches
control from one evaluator to the other.

\[\begin{array}{rcl}
\mathit{eval} &:& (a \iso b) \rightarrow \dt{a} \rightarrow \dt{b} \\
\mathit{eval}~\idc~a &=& a \\
\mathit{eval}~(\symc{f})~b &=& \mathit{evalR}~f~b \\
\mathit{eval}~(f \fatsemi g)~a &=& \mathit{eval}~g~(\mathit{eval}~f~a) \\
\mathit{eval}~(f \otimes g)~(a,b) &=& (\mathit{eval}~f~a, \mathit{eval}~g~b) \\
\mathit{eval}~(f \oplus g)~(\leftv{a}) &=& \leftv{(\mathit{eval}~f~a)} \\
\mathit{eval}~(f \oplus g)~(\rightv{b}) &=& \rightv{(\mathit{eval}~g~b)} \\
\mathit{eval}~\identlp~(\leftv{\circ}) &=& \circ \\
\mathit{eval}~\identlp~(\rightv{a}) &=& a \\
\mathit{eval}~\identrp~a &=& \rightv{a} \\
\mathit{eval}~\swapp~(\leftv{a}) &=& \rightv{a} \\
\mathit{eval}~\swapp~(\rightv{b}) &=& \leftv{b} \\
\mathit{eval}~\assoclp~(\leftv{a}) &=& \leftv{(\leftv{a})} \\
\mathit{eval}~\assoclp~(\rightv{(\leftv{b})}) &=& \leftv{(\rightv{b})} \\
\mathit{eval}~\assoclp~(\rightv{(\rightv{c})}) &=& \rightv{c} \\
\mathit{eval}~\assocrp~(\leftv{(\leftv{a})}) &=& \leftv{a} \\
\mathit{eval}~\assocrp~(\leftv{(\rightv{b})}) &=& \rightv{(\leftv{b})} \\
\mathit{eval}~\assocrp~(\rightv{c}) &=& \rightv{(\rightv{c})} \\
\mathit{eval}~\identlt~((), a) &=& a \\
\mathit{eval}~\identrt~a &=& ((), a) \\
\mathit{eval}~\swapt~(a,b) &=& (b,a) \\
\mathit{eval}~\assoclt~(a,(b,c)) &=& ((a,b),c) \\
\mathit{eval}~\assocrt~((a,b),c)  &=& (a,(b,c)) \\
\mathit{eval}~\distz~(\rightv{c}, a) &=& \rightv{(c, a)} \\
\mathit{eval}~\factorz~(\leftv{(b, a)}) &=& (\leftv{b}, a) \\
\mathit{eval}~\dist~(\leftv{b}, a) &=& \leftv{(b, a)} \\
\mathit{eval}~\dist~(\rightv{c}, a) &=& \rightv{(c, a)} \\
\mathit{eval}~\factor~(\leftv{(b, a)}) &=& (\leftv{b}, a) \\
\mathit{eval}~\factor~(\rightv{(c, a)}) &=& (\rightv{c}, a) \\
\end{array}\]
\[\begin{array}{rcl}
\mathit{evalR} &:& (a \iso ) \rightarrow b \rightarrow a \\
\mathit{evalR}~\idc~a &=& a \\
\mathit{evalR}~(\symc{f}) b &=& \mathit{eval}~f b \\
\mathit{evalR}~(f \fatsemi g) a &=& \mathit{evalR}~f (\mathit{evalR}~g a) \\
\mathit{evalR}~(f \otimes g) (a,b) &=& 
  (\mathit{evalR}~f a, \mathit{evalR}~g b) \\
\mathit{evalR}~(f \oplus g) (\leftv{a}) &=& \leftv{(\mathit{evalR}~f a)} \\
\mathit{evalR}~(f \oplus g) (\rightv{b}) &=& \rightv{(\mathit{evalR}~g b)} \\
\mathit{evalR}~\identlp~a &=& \rightv{a} \\
\mathit{evalR}~\identrp~(\rightv{a}) &=& a \\
\mathit{evalR}~\swapp~(\leftv{a}) &=& \rightv{a} \\
\mathit{evalR}~\swapp~(\rightv{b}) &=& \leftv{b} \\ 
\mathit{evalR}~\assoclp~(\leftv{(\leftv{a})}) &=& \leftv{a} \\
\mathit{evalR}~\assoclp~(\leftv{(\rightv{b})}) &=& \rightv{(\leftv{b})} \\
\mathit{evalR}~\assoclp~(\rightv{c}) &=& \rightv{(\rightv{c})} \\
\mathit{evalR}~\assocrp~(\leftv{a}) &=& \leftv{(\leftv{a})} \\
\mathit{evalR}~\assocrp~(\rightv{(\leftv{b})}) &=& \leftv{(\rightv{b})} \\
\mathit{evalR}~\assocrp~(\rightv{(\rightv{c})}) &=& \rightv{c} \\
\mathit{evalR}~\identlt~a &=& ((), a) \\
\mathit{evalR}~\identrt~((), a) &=& a \\
\mathit{evalR}~\swapt~(a,b) &=& (b,a) \\
\mathit{evalR}~\assoclt~((a,b),c)  &=& (a,(b,c)) \\
\mathit{evalR}~\assocrt~(a,(b,c)) &=& ((a,b),c) \\
\mathit{eval}~\distz~(\rightv{c}, a) &=& \rightv{(c, a)} \\
\mathit{eval}~\factorz~(\leftv{(b, a)}) &=& (\leftv{b}, a) \\
\mathit{evalR}~\dist~(\leftv{(b, a)}) &=& (\leftv{b}, a) \\
\mathit{evalR}~\dist~(\rightv{(c, a)}) &=& (\rightv{c}, a) \\
\mathit{evalR}~\factor~(\leftv{b}, a) &=& \leftv{(b, a)} \\
\mathit{evalR}~\factor~(\rightv{c}, a) &=& \rightv{(c, a)}
\end{array}\]

We state without proof that the evaluation of well-typed combinators always
terminates and that $\Pi$ is logically reversible, i.e., that for all
combinators $c : b_1 \iso b_2$ and values $v_1 : b_1$ and $v_2 : b_2$ we have
the forward evaluation of $c v_1$ produces $v_2$ iff the backwards evaluation
of $c v_2$ produces $v_1$.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Fractional Types as Groupoids} 

In the previous section, every type was modeled by a collection of values
(including a special ``unusable'' value $\bot$) and a collection of trivial
paths. In this section, non-trivial paths will emerge to model ``fractional
values.'' The intuition is that two values that are connected by a path
should not be counted twice as the path induces an equivalence between these
two values: ``they are the same.'' As illustrated in
Sec.~\ref{sec:intuition}, this idea generalizes to conclude that a value
connected to itself using several paths corresponds to a ``fraction.''

We begin by investigating the special situation of a type $\frac{1}{A}$ where
$A$ is a 0-type (i.e., where $A$ does not contain any fractional components).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Rank-1 Isomorphisms as 1-Groupoids}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Rank-$n$ Isomorphisms as $n$-Groupoids}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Operational Semantics via Backtracking Constraints} 

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Connections to Type Theory} 

\begin{quote} 
As usual, something funny happens at the left of the arrow. John Reynolds,
Aarhus, June 27, 2000.~\cite{danvypage} 
\end{quote}

No more! We finally have an inductive characterization of functions
(isomorphisms). No negative occurrences of types. No positivity
checks. Nothing funny.

There are also deep connections with algebraic types, the seven trees in one,
and the Fiore papers.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Connections to Semantics} 

Now that functions are a proper inductive type, we can use conventional
induction to reason about functions. There are also probably connections to
logical relations and parametricity that are essentially some kind of
isomorphism which might be expressible as a higher-order path.

Are higher-order inductive types something like ADTs where we have equations
or something like graphs where we can build interesting shapes inductively or
perhaps both somehow?

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Connections to Logic} 

Similar to double negation proof of $A \vee \neg A$. Make a guess and if
wrong backtrack and choose the other branch.

Double negation vs. braids and twists. Any insights from category theory or
topology that can be used to understand classical proofs?

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Connections to Programming Practice} 

Our construction can be interpreted in the context of speculative concurrent
programming. A thread can at any time create, out of nothing, a value of type
$A$ and proceed with it, generating in the process a value of type
$\frac{1}{A}$ that a concurrent process can be manipulate. When an actual
value of type $A$ is produced, the fractional value is used to coordinate a
backtracking mechanism that communicates the actual value of type $A$ to the
original process. This is very similar to how we use logical variables and
unification.

Because we are \emph{not} in the context of the full $\lambda$-calculus,
which allows arbitrary duplication and erasure of information, values of
fractional types are first-class values that can flow anywhere. The
information-preserving computational infrastructure guarantees that, in a
complete program, every constraint imposed by a fractional value will also be
satisfied exactly once. This property is shared with systems that are based
on linear logic.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Connections to Reversible Computing}

We have higher-order reversible computations.

Consider a similar algebraic manipulation involving fractional types.
\begin{center}
\scalebox{1.1}{
\includegraphics{diagrams/thesis/algebra-wire2.pdf}
}
\end{center}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Connections to Category Theory} 

We have constructed a concrete closed monoidal category. We did not use the
Int-construction which requires an existing trace operator. We inherit a lot
of constructions for free: name, coname, trace, etc.

We have constructed a good candidate for pointed homotopy category.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Connections to Resource Interpretation} 

We can interpret $\times$ as parallel computations (i.e., as computations
occurring simultaneously in different regions in space). So a value of type
$A \times B$ consists of two values occupying two different space locations,
e.g., two different memory locations. With that perspective, a value of type
$\frac{1}{A}$ consists of a small dictionary that stores all the values of
type $A$ and can shuffle them around.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Connections to Homotopy Theory} 

The connection between type theory and homotopy theory raises some
interesting questions. What do the various shapes (spheres, tori, etc.) have
to go with programming? Our answer is that they represent a class
of \emph{functions}: isomorphisms.

We have constructed a good candidate for pointed homotopy category.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Connections to Physics and Quantum Computing} 

Connections between standard circuit model and topological quantum computing.

The dual vector space in quantum mechanics and its role in quantum
computing. The fact that $\eta$ and $\epsilon$ are dual is essentially the
teleportation algorithm. We can give it a computational interpretation in
terms of backtracking.

One understanding of quantum computing is that it exploits the laws of physics
to build faster machines (perhaps). Another more foundational understanding
is that it provides a computational interpretation of physics, and in
particular directly addresses the question of interpretation of quantum
mechanics. In a little known document, Rozas~\cite{Rozas:1987:CMO:889539}
uses continuations to implement the transactional interpretation of quantum
mechanics~\cite{transactional} which includes as its main ingredient a
fixpoint calculation between waves or particles traveling forwards and
backwards in time. Our work sheds no light on whether this interpretation is
the ``right one'' but it is interesting that we can directly realize it using
the primitives of our language.

The multiplicative structure has a direct connection to entangled quantum
particles, or perhaps entangled particles and anti-particles.  The idea of
entanglement, that an action on one particle is ``instantaneously''
communicated to the other, is analogous to how unifying one value affects its
dual pair which is possibly in another part of the computation.  Again our
model sheds no light on whether this is related to how nature computes but it
is again interesting that we can directly realize the idea.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Connections to Information Theory} 

We have given classic computational interpretations to negative
information~\cite{negative-information} and negative
entropy~\cite{negative-entropy}.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Speculative Connections} 

Negative types, square root types, and imaginary types have also appeared in
the literature: we proceed with a simple explanation. We have so far extended
the set of types to be the positive rational numbers. Now we will push this
and extend the set of types to algebraic numbers. In other words, we will
allow datatypes defined by arbitrary polynomials and allow the roots of such
polynomials to be types.

Consider first an example in which we want to compute with the sides of a
rectangle whose area is 91 and whose length is longer than its width by 6
units. One can solve the quadratic equation to determine that the sides are 7
and 13 and proceed. This however prematurely forces us to globally solve the
constraint. Instead we can let the two sides of the rectangle be $x$ and
$x+6$ and use the following equation to capture the desired constraint:
\[
x^2 + 6x - 91 = 0
\]
The equation introduces an isomorphism between the type $x^2 + 6x - 91$ and
the type $0$. We can now proceed to compute with the unknown $x$, being
assured that in a closed program, our computation will eventually be
consistent with the solution of the algebraic equation. 

Previously the most famous example of a similar nature is the puzzling
isomorphism that one can establish between seven binary trees and one.
A binary tree is defined by the datatype
\[
x = 1 + x * x 
\]
which can be rearranged to the polynomial equation $x^2 - x + 1 = 0$. By
algebraic manipulation we can reason as follows:
\[\begin{array}{rclclclcl}
x^3 &=& x^2 x &=& (x-1) x &=& x^2 - x &=& -1 \\
x^6 &=& 1 \\
x^7 &=& x^6 x &=& x
\end{array}\]
Fiore poses the question of why such algebraic manipulation would make sense
type theoretically but states that even though some of the intermediate steps
make no sense, the final equivalence is valid and can be used to actually
construct an isomorphism between $x^7$ the type of seven binary trees 
and $x$ the type of binary trees.

Discussion of possible polynomials:
\begin{itemize}
\item $b=1+1$. Boring.
\item $b=b+1$. That introduces the natural numbers. No solution for this
  polynomial over the algebraic numbers. We must extend the numbers with
  $\omega$ to get a solution. We reject this in this paper and prefer to
  stick to algebraic numbers. The advantage is that all the isomorphisms are
  valid numerically. With the above type we could subtract $b$ from both
  sides to show that $0=1$ which is nonsense. We can however have infinite
  types as long as they have algebraic solutions.
\item $b^2=2$ or $b = \pm \sqrt{2}$. We have introduced the square root of a
  boolean! If we had superpositions, we could then write a function that
  performs the square root of negation in the sense that applying it twice
  would be equivalent to boolean negation.
\end{itemize}

\paragraph*{Geometry of Interaction (GoI).}
Geometry of Interaction was developed by Girard~\cite{girard1989geometry} as
part of the development of linear logic. It was given a computational
interpretation by Abramsky and
Jagadeesan~\cite{Abramsky:1994:NFG:184662.184664}, and was developed into a
reversible model of computing by
Mackie~\cite{Mackie2011,DBLP:conf/popl/Mackie95}. Preliminary investigations
suggest that many of the GoI machine constructions can be simulated by
treating Mackie's bi-directional wires as pairs of wires and replacing the
machine's global state with a typed value on the wire that captures the
appropriate state. This connection is exciting because when viewed through a
Curry-Howard lens it suggests that the logical interpretation of would be a
linear-like logic with a notion of resource preservation and with a natural
computational interpretation.

\paragraph*{Computing in the Field of Algebraic Numbers.}
\label{sec:algebraic-field}
Algebraically, the addition of fractional types corresponds to a move from a
ring-like structure to a full field. Our language captures the structure of
one particular field: that of the rational numbers. As we have seen,
computation in this field is quite expressive and interesting and yet, it has
two fundamental limitations. First it cannot express any recursive type, and
second it cannot express any datatype definitions. We believe these to be two
orthogonal extensions: recursive types were considered in our previous
paper~\cite{James:2012:IE:2103656.2103667}; arbitrary datatypes are however
even more exciting that plain rationals as each datatype definition can be
viewed as a polynomial (see below) which essentially means that we start
computing in the field of algebraic numbers, which includes square roots and
imaginary numbers. As crazy as it might seem, the type $\sqrt{2}$ and even
the type $(1/2)+i(\sqrt{3}/2)$ ``make sense.''  In fact the latter type is
the solution to the polynomial $x^2-x+1=0$ which if re-arranged looks like
$x=1+x*x$ and perhaps more familiarly as the datatype of binary trees $\mu
x.(1+x*x)$. These types happen to have been studied extensively following a
paper by Blass~\cite{seventrees} which used the above datatype of trees to
infer an isomorphism between seven binary trees and one!

We have confirmed that we can extend our language with the datatype
declaration for binary trees and build a witness for this isomorphism that
works as expected. However not every isomorphism constructed from algebraic
manipulation is computationally meaningful. To understand the issue in more
detail, consider the following algebraically valid proof of the isomorphism
in question:
\[\begin{array}{rclclclcl}
x^3 &=& x^2 x &=& (x-1) x &=& x^2 - x &=& -1 \\
x^6 &=& 1 \\
x^7 &=& x^6 x &=& x
\end{array}\]
The question is why such an algebraic manipulation makes sense type
theoretically, even though the intermediate step asking for an isomorphism
between $x^6$ and $1$ has no computational context. In our setting, this
isomorphism can be constructed but it diverges on all inputs (in both
ways). This suggests that, in the field of algebraic numbers, some algebraic
manipulations are somehow ``more constructive'' than others.

A related issue is that not all meaningful recursive types are meaningful
polynomials. For instance $\textsf{nat}=\mu x.(1+x)$ implies the polynomial
$x=1+x$ which has no algebraic solutions without appeal to more complex
structures with limits etc.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Conclusions and Future Work} 

This is cool and deep.

\paragraph*{Declarative Continuations.} 
In his Masters thesis~\cite{Filinski:1989:DCI:648332.755574}, Filinski
proposes that continuations are a \emph{declarative} concept. He,
furthermore, introduces a symmetric extension of the $\lambda$-calculus in
which call-by-value is dual to call-by-name and values are dual to
continuations. In more detail, the symmetric calculus contains a ``value''
fragment and a ``continuation'' fragment which are mirror images. Pairs and
sums are treated as duals in the sense that the ``value'' fragment includes
pairs whose mirror image in the ``continuation'' fragment are sums. In
contrast, our language includes pairs and sums in the value fragment and two
symmetries: one that maps the pairs to fractions and another that maps the
sums to subtractions.

\paragraph*{The Duality of Computation.}
The duality between call-by-name and call-by-value was further investigated
by Selinger using control
categories~\cite{Selinger:2001:CCD:966910.966911}. Curien and
Herbelin~\cite{Curien:2000} also introduce a calculus that exhibits
symmetries between values and continuations and between call-by-value and
call-by-name. The calculus includes the type $A-B$ which is the dual of
implication, i.e., a value of type $A-B$ is a context expecting a function of
type $A \rightarrow B$. Alternatively a value of type $A-B$ is also explained
as a \emph{pair} consisting of a value of type $A$ and a continuation of type
$B$. This is to be contrasted with our interpretation of a value of that type
as \emph{either} a value of $A$ or a demand for a value of type $B$. This
calculus was further analyzed and extended by
Wadler~\cite{Wadler:2003,DBLP:conf/rta/Wadler05}. The extension gives no
interpretation to the subtraction connective and like the original symmetric
calculus of Filinski, introduces a duality that relates sums to products and
vice-versa.

\paragraph*{Subtractive Logic.} 
Rauszer~\cite{springerlink:10.1007/BF02120864,rauszer,rauszer2} introduced a
logic which contains a dual to implication. Her work has been distilled in
the form of \emph{subtractive logic}~\cite{Crolard01} which has recently been
related to coroutines~\cite{Crolard01082004} and delimited
continuations~\cite{Ariola:2009:TFD:1743339.1743381}.  In more detail,
Crolard explains the type $A-B$ as the type of \emph{coroutines} with a local
environment of type $A$ and a continuation of type $B$. The description is
complicated by what is essentially the desire to enforce linearity
constraints so that coroutines cannot access the local environment of other
coroutines. 

\paragraph*{Negation in Classical Linear Logic} 
Filinski~\cite{Filinski92} uses the negative types of linear logic to model
continuations. Reddy~\cite{Reddy91} generalizes this idea by interpreting the
negative types of linear logic as \emph{acceptors}, which are like
continuations in the sense that they take an input and return no
output. Acceptors however are also similar in flavor to logic variables:
they can be created and instantiated later once their context of use is
determined. Although a formal connection is lacking, it is clear that, at an
intuitive level, acceptors are entities that combine elements of our negative
and fractional types.

\paragraph*{The Lambek-Grishin Calculus.} The ``parsing-as-deduction'' style
of linguistic analysis uses the Lambek-Grishin calculus with the following
types: product, left division, right division, sum, right difference, and
left difference~\cite{Bernardi:2010:CSL:1749618.1749689}. The division and
difference types are similar to our types but because the calculus lacks
commutativity and associativity and only has limited notions of
distributivity, each connective needs a left and right version. The
Lambek-Grishin exhibits two notions of symmetry but they are unrelated to our
notions. In particular, the first notion of symmetry expresses commutativity
and the second relates products to sums and divisions to subtractions. In
contrast, our two symmetries relate sums to subtractions and products to
divisions.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section*{Acknowledgments}

This material is based upon work supported by the National Science Foundation
under Grant No. 1217454. We would like to specially thank Roshan James and
Zachary Sparks for their contributions to early stages of this work. 

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\bibliographystyle{plain}
\bibliography{cites}
\end{document}


{--

-- In our perspective isomorphisms are represented by paths; there are
-- 1! isomorphims from ? to itself so we expect exactly one path in
-- the space ? o-> ?, i.e., one path from ? to itself, i.e., the space
-- (? ? ?) should be isomorphic to ?. However we can't witness this
-- isomorphism yet until we postulate the ? and ? paths.
--
-- unitPath' : (? ? ?) ? ?
-- unitPath' = ?

-- functions and types should have their equivalences as paths NOT
-- extensional isomorphisms which are later postulated to be paths!!!

-- need some kind of ``vertical'' path that allows us to move one level up.

-- explore this: 1 -> 1/x * x goes to point x which has a higher
-- groupoid structure ``above it'', gives you the higher groupoid
-- structure as 1/x and the naked point as x. Epsilon can then
-- recombine a higher groupoid collection of paths with a
-- point. Recall the 3/4 example: the paths not attached to any points
-- are 3/4: they take 4 points and return 3 points.

-- to get 1/5
-- start with 5 points * * * * *
-- and paths that connect them so that they are identified to be 1 point
-- Separate the points from the paths: the paths represent 1/5: something that takes
-- 5 points and collapses them to 1 and so we get 1_{5} --> 1/5 * 5
-- The problem is that 5 now has no paths over it so it's a different 5 and 1/5 has
-- no points so it's not a groupoid or is it?

-- 1/x can switch the two components of •[_,_] so that it is an involution

We don't have pointed types. We have HITs. Each type is a collection
of points and a collection of non-trivial paths. (We get refl, !, ?,
associativity, etc. for tree and we also get the higher groupoid
structure for free which witnesses for example the pentagon and
triangle axioms, i.e., the coherence of assoc and the nice interplay
with !).

Start with the type 1 at 3 •[{a,b,c) , {(a==b),(b==c)}]. This type
represents ``1'' but uses three identical elements to express this fact.

The paths by themselves are some sort of function that takes three
points and identifies them; this can be represented by the type
1/3. The three points by themselves can be represented by the type 3.

So 3 is •[{a,b,c}, ?]

and 1/3 is •[{? a b c ? (a==b,b==c)}, ?] 
the ? is a mini one step function to express that the paths are not
attached to any end points. You give me the end points and I will connect them.

The only value of type 1/3 is that function. We can pass around it and
eventually we must apply to 3 points which become identified. So
eventually we recover 1 back.

So now what is 1/(1/3). Remember that to express 1/3. We started with
a version of 1 that had 3 elements and paths between them. So to do
1/(1/3) we need to start with a version of 1 that has 1/3 elements and
paths between them.

1 at 1/3 is •[{? a b c ? (a==b,b==c)}, 3 paths from this point to itself ]

so 1 at 1/3 can be split into 1/3 and and 1/(1/3) as follows:
1/3 = •[{? a b c ? (a==b,b==c)}, ?]
1/(1/3) = •[ ? a ? 3 paths from a to itself , ? ]

--

swapP : {A B : Set} ? A × B ? B × A
swapP {A} {B} = ?

It looks like I will need an axiom (not univalence necessarily but
something like it. We want to say that type isos from Pi correspond to
paths. So instead of saying (A ? B) ? (A ? B) we would say (A ? B) ?
(A ? B) where ? is the type of isos from Pi (making the types into a
field like structure).

Ok so there is an external map between A × B and B × A but because we
are monoidal closed there is also an internal map (1/(A × B)) × (B × A)
or more readably (A × B) -o (B × A). This map is defined as follows.

First let's start with 1 at A × B. This is:

•[ {(a0,b0),(a0,b1),(a1,b0),(a1,b1)} , {(a0,b0)?(a0,b1), (a0,b0)?(a1,b0), ... }]

Anyway the point is that we can build 1/(A×B). Now we know that every
(a0,b0)?(a1,b1) comes from (a0?a1) and (b0?b1) and hence we can
assemble them in the other direction to get (b0,a0)?(b1,a1). 

Now we can split using ? to 1/(A×B) and (A×B) where:

A×B = •[ {(a0,b0),(a0,b1),(a1,b0),(a1,b1)} , ?]
and
1/(A×B) = •[? (a0,b0) (a0,b1) (a1,b0) (a1,b1) ? 
             {(a0,b0)?(a0,b1), (a0,b0)?(a1,b0), ... } , 
           ?]

which is the same as:

1/(A×B) = •[? a0 a1 b0 b1 ? {a0?a1, b0?b1} , ?]
              
Now the map (A×B)-o(B×A) is represented by the type:

•[{((b0,a0),? a0 a1 b0 b1 ? {a0?a1, b0?b1}),
   ((b0,a1),? a0 a1 b0 b1 ? {a0?a1, b0?b1}),
   ((b1,a0),? a0 a1 b0 b1 ? {a0?a1, b0?b1}),
   ((b1,a1),? a0 a1 b0 b1 ? {a0?a1, b0?b1})}
  ?]

Now applying the function to (a0,b0) means pairing the above with (a0,b0):
              
•[{((b0,a0),(a0,b0),? a0 a1 b0 b1 ? {a0?a1, b0?b1}),
   ((b0,a1),(a0,b0),? a0 a1 b0 b1 ? {a0?a1, b0?b1}),
   ((b1,a0),(a0,b0),? a0 a1 b0 b1 ? {a0?a1, b0?b1}),
   ((b1,a1),(a0,b0),? a0 a1 b0 b1 ? {a0?a1, b0?b1})}
  ?]

--}

------------------------------------------------------------------------------

CS: Give computational content of science
  Logic: Curry-Howard
  Classical logic: Continuations
  Physics: Quantum information; computation
  cognition
  linguistics
  Construction of cellos

Mathematical proofs have computational content
Physical equations have computational content

Now at the heart of it all: EQUALITY has computational content and is the
most fundamental relation we use implicitly

Theory at the center of many many things: topology, algebra, geometry, type
theory, physics, etc. ==> Exciting

Conservation of information, energy, etc. 
Symmetry
F = m a
or E = m C^2
are not EQUALITIES. They are isomorphisms: go from one to the other
preserving various entitites. 
Get rid of equality ==> use isomorphisms exclusively

Turtles all the way down (or up in that case)


--

when are two structures "the same"
if their elements are the same

what is the structures are infinite? (i.e., described by a process); go
right, then right, then right, then right is the same as stay here but not
quite the same

E=mc2, F=ma

Leibnitz

--

 - topology of computation/evaluation: in addition to loops/circle,
   bernstein conditions for parallelism; or more accurately two
   computations are homotopic if one is sequential and is parallel and I
   can massage one to the other

 - univalence: (A \== B) isEquiv (A isEquiv B) fun. ext. (f \== g) -> (x
   : A) f(x) \== g(x) is an equivalence paths between complex types iff
   there are paths between the points: works for simple finite types;
   for infinite things can't be proved; need these two additional axioms

 - for my intro: what is hott; article about hott in magazine; 
   steve awodey's talk
   "http://www.andrew.cmu.edu/user/awodey/hott/CMUslides.pdf"
   formalize mathematics if you care about that: eckmann-hilton
   "http://blogs.scientificamerican.com/guest-blog/2013/10/01/voevodskys-mathematical-revolution/"
    Logic level -1
    Set theory level 0
    groupoid level 1
    ...
    The Propositions-as-Types conception of Martin-Löf type theory leads
   to a system of logic that is different from both classical and
   intuitionistic logic with respect to the statements that hold in the
   fragment of logical language that these three share, namely the
   quantifiers \Pi , \Sigma , equality \mathsf{Id} , conjunction \times
   , disjunction + , implication \rightarrow and negation \neg .  For
   example, it validates the “axiom of choice” but not the “law
   of excluded middle” — a combination that is impossible
   classically and intuitionistically.  Let us call this conception
   “constructive validity” following a paper by Dana Scott in
   which it was first introduced (Constructive Validity, Symposium on
   Automated Deduction, LNM 125, Springer (1970), pp. 237-275).

 - for class "http://math.ucr.edu/home/baez/eckmann_hilton.jpg"

 - circle ==> recursion: homotopy between path p and path q means
   if we can move from p to q without getting snagged in a loop, i.e.,
   without crossing over an infinite loop!!

 - Agda and homotopy type theory idea: Ulf showed us how to fill in
   "small" program fragments automatically. If we had more precise types
   can the compiler fill in different algorithms for us. Here is an
   idea: in HoTT we can control the isomorphisms and what we mean by
   them. For example, we can add paths between A and B to mean that B is
   a sorted version of A. Then different arrows would correspond to
   different sorting algorithms. If we maintain proof relevance then we
   can do actions depending on the particular sorting algorithm that is
   used to go from A to B. This might be doable in Pi actually.

- different levels correspond to fractal equality or perhaps each level gives
  you more precision

- Don't you think that these:
  "http://en.wikipedia.org/wiki/Loop_optimization"
  are homotopies. They do make some explicit connections to
  "geometry/topology". I think we have discovered a gold mine 


So I thought more about it and I think it holds more water. Here is the story:

- paths in HoTT represent computations; this is true in the conventional
  HoTT but even more or so in our context where all computations are
  isomorphisms; 

- paths that loop are therefore looping computations;

- the loop in a 2groupoid terminates after two iterations;

- the loop in S1 is an infinite loop;

- the loop in S2 is a double infinite loop (on two natural
  numbers); 

- the various geometric objects capture various patterns of iteration!

- Filinski's paper below shows that if you are given one simple infinite
  loop and continuations, then you can expression recursion.  So if we
  include S1 in our system and we figure out how to do higher-order
  functions (and their duals as delimited continuations), then we should
  be able to express recursion. A small hope would be that we can get
  away without full continuations and that we can get recursion from S1
  using just the groupoid structure but that's speculative.

I like it! --Amr

Check this out: "http://iml.univ-mrs.fr/geocal06/"=20

In particular this workshop:

Algebraic Topology, Concurrency and Rewriting

Organizers: =C3=89ric Goubault, Yves Lafont

The objective of the course is to give a general overview of the recent
developments of ``geometrical'' approaches to the theory of computation,
in particular concurrent and distributed computations, and rewriting.

The course will start by a general introduction to homotopy and
homology, classical on topological spaces, and generalize through
abstract homotopy theory and generalized homology theories. Then two
different applications will be developped.

The first one concerns concurrency theory. In this application, a
refined form of homotopy (dihomotopy) has to be designed, that takes
into account the direction of time. Similar methods as the ones on
ordinary topological spaces can be defined, in order to find
``invariants'' under dihomotopy, i.e. a way to classify directed shapes
under (directed) deformation. These invariants can in turn be used for
purposes of proofs or static analysis of algorithms or programs. We will
show such applications in the course. Other applications, of more
classical algebraic topological invariants will also be derived, in the
field of fault-tolerant distributed systems.

The second one concerns the rewriting theory. Since the pioneering work
by Squier, we know how to use homology to characterize the algebraic
objects presented by rewriting systems. Basically, words are seen as
objects of dimension one, rewriting rules are seen as of dimension two,
confluence diagrams as of dimension three etc. providing resolutions to
the algebraic objects they present. Extensions to term rewriting has
been recently solved, along similar lines, using more general homology
theories. Also higher-dimensional rewriting has gained wide interest and
its theory will be fully developped, in conjunction with the necessary
n-categorical (or polygraphic) theory.

mfsp paper by Fajstrup, Goubault, and Raussen

http://www.pps.univ-paris-diderot.fr/~laurent/geocal/slides/mellies.pdf‎

-- Repeat for monoids without using equivalences!

-- Let's build a monoidal category whose objects are ∞-groupoids using
-- Thorsten's trick perhaps. Or perhaps we only need 1-groupoids or
-- 2-groupoids... Or better use HITs: explicit constructors for points
-- and paths and let the whole ∞-groupoid structure be implicit and
-- generated by J on demand as needed. A morphim between such HITs
-- would map points to points and paths to paths LYING OVER the
-- original paths (using transport).

-- multiplicative monoid:
-- bifunctor ⊗ maps two types A and B to the type (A ⊗ B):
--   map a point in A and a point in B to a point in (A ⊗ B)
--   map a path in A and a path in B to a path in (A ⊗ B)
--   if paths p in A and q in B are respectively equal to paths p' in
--     A and q' in B then their images in (A ⊗ B) are also equal
-- associative up to ...
-- an object I which is both a left and right identity for ⊗ 
-- coherence conditions: pentagon and triangle
-- 
-- Now what is the structure on 1 and ⊗ in terms of paths on the
-- components

-- map points to points
-- map paths to paths
-- preserve ≡

apTensor : {A B C : Set} {x y : A × B} → (f : A × B → C) → (x ≡ y) → (f x ≡ f y)
apTensor {A} {B} {C} {x} {y} f p = 
  pathInd 
    (λ {x} {y} p → f x ≡ f y) 
    (λ x → refl (f x))
    {x} {y} p

-- monoid 0 and ⊕

-- do all these sections in Ch. 2 with monoidal categories instead of
-- the usual type constructors

-- imagine we had tensor products instead would be it possible to
-- convert a path : A × B → C × D to two sequential paths A → C with
-- refl on B followed by the path B → D and refl on C. So the
-- topological view of computation would express which dependencies
-- allow you to move computations around to make them more or less
-- parallel. Delooping sounds like it would allow you to make a loop
-- (sequential) into something that operates in parallel (say every
-- two iterations happen in parallel) but that can only happen if the
-- dependencies are "right".

loops/spaces; loop optimizations; cata/epi/etc-morphisms are also
patterns of recursion; probably even parametricity and logical
relations; all these things must be homotopies.

1/x gives you the pattern to define a clause
+ gives you the ability to write all the clauses
- gives you the ability to retract a clause
all functions are constructible from the identity by massaging it
functors between types internalized inside a type using 1/., +, and -

PI 

cardinality of these infinity groupoids

delooping: 1/Bool = 1/(delooping false) + 1/(deloopoing true) 

≡ {u+1} {Set u : Set (u+1)} (T1 : Set u) (T2 : Set u) -> Set (u+1)

CC : ∀ {u} → (A B : Set u) → _≡_ {L.suc u} {Set u} A B → Set (L.suc u)
CC {u} A B p = _≡_ {L.suc u} {Set u} (A × B) (B × A)

cc : ∀ {u} → (A : Set u) → _≡_ {L.suc u} {Set u} (A × A) (A × A)
cc A = refl

swapP : ∀ {u} → (A B : Set u) → _≡_ {L.suc u} {Set u} (A × B) (B × A) 
swapP {u} = pathIndU {u} {Set u} CC cc
  
t : ℕ × Bool ≡ Bool × ℕ
t = swapP ℕ Bool

How many elements are in this set:

{ Egyptian, American, Chinese }

It depends on the equivalence relation. If you think the trivial
relation, there are 3 elements. If you think the relation that
identifies Egyptian/American (Amr) then you have two elements only in
the set. We can make this equivalence relation depend on the
particular element in question and we can make it first-class. When
viewed by itself, it is like the fraction 2/3: it takes 3 elements and
identifies two of them giving you back two elements.


https://inf.ug.edu.pl/~stefan/AlgTop/

--

All programming only builds trees. 
Graphs require assignments and ugly things
HoTT allows us to build datatypes with "paths", "shapes", etc.

CS -> Topology: study shapes with inductive types
Topology -> CS: richer datatypes with cycles

Can I build types that solve polynomials ???

Define pointed types (A,a)

Reciprocal of a pointed type (A,a) is delooping (a=a,refl)

delooping of A is (B,b) such that loopspace(B,a) = A

our construction of fractionals is delooping: take n points connected by a
group stucture; turn them into a point with the group structure turned into
path composition.

A permutation is represented as

\begin{verbatim}
(1 2 3 4 5)
(2 5 4 3 1)
\end{verbatim}

We can decompose it in:

\begin{verbatim}
2

and 

1 with paths (2 3 4 5)
             (5 4 3 1)
\end{verbatim}

This is the decomposition of the function \verb|A -> A| into
\verb|A * 1/A|. A problem still with cardinality: there is exactly one
element into the latter type but presumably several functions in the
former. Perhaps all these functions are equivalent somewho up to homotopy?