-
Notifications
You must be signed in to change notification settings - Fork 2
/
p2.lagda
2453 lines (2207 loc) · 102 KB
/
p2.lagda
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
\documentclass[authoryear,preprint]{sigplanconf}
\usepackage{agda}
%% \usepackage{fixltx2e}
\usepackage{fix2col}
\usepackage{ucs}
\usepackage[utf8x]{inputenc}
\usepackage{tikz}
\usepackage[all]{xy}
\usepackage{amsthm}
\usepackage{latexsym}
\usepackage{courier}
\usepackage{thmtools}
\usepackage{bbold}
\usepackage{url}
\usepackage{bbm}
\usepackage{proof}
\usepackage{amstext}
\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{comment}
\usepackage{stmaryrd}
\usepackage{listings}
\usepackage{graphicx}
\usepackage{textgreek}
\usepackage{extarrows}
\usepackage{multicol}
\newtheorem{theorem}{Theorem}
% XY-Pic definitions for making ``wire charts''
\newcommand{\sep}{\hspace{2em}}
\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}}
\renewcommand{\AgdaCodeStyle}{\small}
\newcommand{\nodet}[2]{\fcolorbox{black}{white}{$#1$}\fcolorbox{black}{gray!20}{$#2$}}
\newcommand{\cubt}{\mathbb{T}}
\newcommand{\ztone}{\mathbb{0}}
\newcommand{\otone}{\mathbb{1}}
\newcommand{\eqdef}{\stackrel{\triangle}{=}}
\newcommand{\ptone}[2]{#1 \boxplus #2}
\newcommand{\ttone}[2]{#1 \boxtimes #2}
\newcommand{\isoone}{\Leftrightarrow}
\newcommand{\lolli}{\multimap}
\newcommand{\pointed}[2]{\AgdaSymbol{•}\AgdaSymbol{[} #1 \AgdaSymbol{,} #2 \AgdaSymbol{]}}
\newcommand{\AgdaArgument}[1]{#1}
\newcommand{\inl}[1]{\textsf{inl}~#1}
\newcommand{\inr}[1]{\textsf{inr}~#1}
\newcommand{\idv}[3]{#2 \xrightarrow{#1} #3}
\newcommand{\cp}[3]{#1\stackrel{#2}{\bullet}#3}
\newcommand{\idt}[3]{#2 \equiv_{#1} #3}
\newcommand{\idrt}[3]{#3 \equiv_{#1} #2}
\newcommand{\refl}[1]{\textsf{refl}~#1}
\newcommand{\lid}{\textsf{lid}}
\newcommand{\rid}{\textsf{rid}}
\newcommand{\linv}{l!}
\newcommand{\rinv}{r!}
\newcommand{\invinv}{!!}
\newcommand{\assoc}{\circ}
\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{\iso}{\leftrightarrow}
\newcommand{\proves}{\vdash}
\newcommand{\idc}{\mathit{id}}
\newcommand{\ap}[2]{\mathit{ap}~#1~#2}
\newcommand{\alt}{~|~}
\newcommand{\evalone}[2]{#1~\triangleright~#2}
\newcommand{\evaloneb}[2]{#1~\triangleleft~#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}}
\newcommand{\pc}{\fatsemi} % path composition
\newenvironment{floatrule}
{\hrule width \hsize height .33pt \vspace{.5pc}}
{\par\addvspace{.5pc}}
\DeclareUnicodeCharacter{9678}{$\circledcirc$}
\DeclareUnicodeCharacter{8644}{$\rightleftarrows$}
\DeclareUnicodeCharacter{10231}{$\leftrightarrow$}
\DeclareUnicodeCharacter{10214}{$\llbracket$}
\DeclareUnicodeCharacter{10215}{$\rrbracket$}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Comments
\newif\ifcomments\commentstrue
\ifcomments
\newcommand{\authornote}[3]{\textcolor{#1}{[#3 ---#2]}}
\newcommand{\todo}[1]{\textcolor{red}{[TODO: #1]}}
\else
\newcommand{\authornote}[3]{}
\newcommand{\todo}[1]{}
\fi
\newcommand{\jc}[1]{\authornote{purple}{JC}{#1}}
\newcommand{\as}[1]{\authornote{magenta}{AS}{#1}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{document}
\special{papersize=8.5in,11in}
\setlength{\pdfpageheight}{\paperheight}
\setlength{\pdfpagewidth}{\paperwidth}
\title{A Computational Reconstruction of \\
Homotopy Type Theory for Finite Types}
\authorinfo{}{}{}
\maketitle
\begin{abstract}
Homotopy type theory (HoTT) relates some aspects of topology, algebra,
%% geometry, physics,
logic, and type theory, in a unique novel way that
promises a new and foundational perspective on mathematics and
computation. The heart of HoTT is the \emph{univalence axiom}, which
informally states that isomorphic structures can be identified. One of the
major open problems in HoTT is a computational interpretation of this axiom.
We propose that, at least for the special case of finite types, reversible
computation via type isomorphisms \emph{is} the computational interpretation
of univalence.
\end{abstract}
\AgdaHide{
\begin{code}
{-# OPTIONS --without-K #-}
module p2 where
open import Level
open import Data.Empty
open import Data.Unit
open import Data.Sum
open import Data.Bool
open import Data.Product
open import Data.Nat hiding (_⊔_)
open import Function
open import Groupoid
infixr 30 _⟷_
infixr 10 _◎_
infix 4 _≡_ -- propositional equality
infix 4 _∼_ -- homotopy between two functions (the same as ≡ by univalence)
infix 4 _≃_ -- type of equivalences
infix 2 _□ -- equational reasoning for paths
infixr 2 _⟷⟨_⟩_ -- equational reasoning for paths
--infix 2 _▤ -- equational reasoning for paths
--infixr 2 _⇔⟨_⟩_ -- equational reasoning for paths
\end{code}
}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Introduction}
Homotopy type theory (HoTT)~\cite{hottbook} has a convoluted treatment of
functions. It starts with a class of arbitrary functions, singles out a
smaller class of ``equivalences'' via extensional methods, and then asserts
via the \emph{univalence} \textbf{axiom} that the class of functions just
singled out is equivalent to paths. Why not start with functions that are, by
construction, equivalences?
The idea that computation should be based on ``equivalences'' is an old one
and is motivated by physical considerations. Because physics requires various
conservation principles (including conservation of information) and because
computation is fundamentally a physical process, every computation is
fundamentally an equivalence that preserves information. This idea fits well
with the HoTT philosophy that emphasizes equalities, isomorphisms,
equivalences, and their computational content.
In more detail, a computational world in which the laws of physics are
embraced and resources are carefully maintained (e.g., quantum
computing~\cite{NC00,Abramsky:2004:CSQ:1018438.1021878}), programs must be
reversible. Although this is apparently a limiting idea, it turns out that
conventional computation can be viewed as a special case of such
resource-preserving reversible programs. This thesis has been explored for
many years from different
perspectives~\cite{fredkin1982conservative,Toffoli:1980,bennett2010notes,bennett2003notes,Bennett:1973:LRC,Landauer:1961,Landauer}
and more recently in the context of type
isomorphisms~\cite{James:2012:IE:2103656.2103667}.
This paper explores the basic ingredients of HoTT from the perspective that
computation is all about type isomorphisms. Because the issues involved are
quite subtle, the paper is an executable \texttt{Agda 2.4.0} file with the
global \AgdaComment{without-K} option enabled. The main body of the paper
reconstructs the main features of HoTT for the limited universe of finite
types consisting of the empty type, the unit type, and sums and products of
types. Sec.~\ref{intc} outlines directions for extending the result to richer
types.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Condensed Background on HoTT}
\label{hott}
Informally, and as a first approximation, one may think of HoTT as a
variation on Martin-L\"of type theory in which all equalities are given
\emph{computational content}. We explain the basic ideas below.
%%%%%%%%%%%%%%%%%%
\subsection{Paths}
Formally, Martin-L\"of type theory, is based on the principle that every
proposition, i.e., every statement that is susceptible to proof, can be
viewed as a type\footnote{but the converse is not part of the principle.
This is frequently misunderstood.}.
Indeed, if a proposition $P$ is true, the corresponding
type is inhabited and it is possible to provide evidence or proof for $P$
using one of the elements of the type~$P$. If, however, a proposition $P$ is
false, the corresponding type is empty and it is impossible to provide a
proof for $P$. The type theory is rich enough to express the standard logical
propositions denoting conjunction, disjunction, implication, and existential
and universal quantifications. In addition, it is clear that the question of
whether two elements of a type are equal is a proposition, and hence that
this proposition must correspond to a type. We encode this type in Agda
as follows,
\smallskip
\begin{code}
data _≡_ {ℓ} {A : Set ℓ} : (a b : A) → Set ℓ where
refl : (a : A) → (a ≡ a)
\end{code}
\smallskip
\noindent where we make the evidence explicit. In Agda, one may write proofs
of such propositions as shown in the two examples below:
\begin{multicols}{2}
\begin{code}
i0 : 3 ≡ 3
i0 = refl 3
i1 : (1 + 2) ≡ (3 * 1)
i1 = refl 3
\end{code}
\end{multicols}
\noindent More generally, given two values \AgdaBound{m} and \AgdaBound{n} of
type \AgdaPrimitiveType{ℕ}, it is possible to construct an element
\AgdaInductiveConstructor{refl} \AgdaBound{k} of the type \AgdaBound{m}
\AgdaDatatype{≡} \AgdaBound{n} if and only if \AgdaBound{m}, \AgdaBound{n},
and \AgdaBound{k} are all ``equal.'' As shown in example \AgdaFunction{i1},
this notion of \emph{propositional equality} is not just syntactic equality
but generalizes to \emph{definitional equality}, i.e., to equality that can
be established by normalizing the values to their normal forms. This is
also known as ``up to $\beta\eta$.''
An important question from the HoTT perspective is the following: given two
elements \AgdaBound{p} and \AgdaBound{q} of some type \AgdaBound{x}
\AgdaDatatype{≡} \AgdaBound{y} with
\AgdaBound{x}~\AgdaBound{y}~\AgdaSymbol{:}~\AgdaBound{A}, what can we say
about the elements of type \AgdaBound{p} \AgdaDatatype{≡} \AgdaBound{q}. Or,
in more familiar terms, given two proofs of some proposition $P$, are these
two proofs themselves ``equal.'' In some situations, the only interesting
property of proofs is their existence. This therefore suggests that the exact
sequence of logical steps in the proof is irrelevant, and ultimately that all
proofs of the same proposition are equivalent. This is however neither
necessary nor desirable. A twist that dates back to a paper by
\citet{Hofmann96thegroupoid} is that proofs actually possess a structure of
great combinatorial complexity.
\jc{Surely proof theory predates this by decades? Lukasiewicz and Gentzen?}
HoTT builds on this idea by interpreting
types as topological spaces or weak $\infty$-groupoids, and interpreting
identities between elements of a type
\AgdaBound{x}~\AgdaDatatype{≡}~\AgdaBound{y} as \emph{paths} from the point
\AgdaBound{x} to the point \AgdaBound{y}. If \AgdaBound{x} and \AgdaBound{y}
are themselves paths, the elements of
\AgdaBound{x}~\AgdaDatatype{≡}~\AgdaBound{y} become paths between paths
(2-paths), or homotopies in topological language. To be explicit, we will
often refer to types as \emph{spaces} which consist of \emph{points}, paths,
2-paths, etc. and write $\AgdaDatatype{≡}_\AgdaBound{A}$ for the type of paths
in space \AgdaBound{A}.
\jc{We know that once we have polymorphism, we have no interpretations in
Set anymore -- should perhaps put more warnings in the next paragraph?}
As a simple example, we are used to thinking of (simple) types as sets of
values. So we typically view the type \AgdaPrimitiveType{Bool} as the figure on
the left. In HoTT we should instead think about it as the figure on the
right where there is a (trivial) path \AgdaInductiveConstructor{refl}
\AgdaBound{b} from each point \AgdaBound{b} to itself:
\[
\begin{tikzpicture}[scale=0.7]
\draw (0,0) ellipse (2cm and 1cm);
\draw[fill] (-1,0) circle (0.025);
\node[below] at (-1,0) {false};
\draw[fill] (1,0) circle (0.025);
\node[below] at (1,0) {true};
\end{tikzpicture}
\qquad\qquad
\begin{tikzpicture}[scale=0.7]
\draw (0,0) ellipse (2cm and 1cm);
\draw[fill] (-1,0) circle (0.025);
\draw[->,thick,cyan] (-1,0) arc (0:320:0.2);
\node[above right] at (-1,0) {false};
\draw[fill] (1,-0.2) circle (0.025);
\draw[->,thick,cyan] (1,-0.2) arc (0:320:0.2);
\node[above right] at (1,-0.2) {true};
\end{tikzpicture}
\]
In this particular case, it makes no difference, but in general we may have a
much more complicated path structure. The classical such example is the
topological \emph{circle} which is a space consisting of a point
\AgdaFunction{base} and a \emph{non trivial} path \AgdaFunction{loop} from
\AgdaFunction{base} to itself. As stated, this does not amount to
much. However, because paths carry additional structure (explained below),
that space has the following non-trivial structure:
\begin{center}
\begin{tikzpicture}[scale=0.74]
\draw (-0.2,0) ellipse (5.5cm and 2.5cm);
\draw[fill] (0,0) circle (0.025);
\draw[->,thick,red] (0,0) arc (90:440:0.2);
\node[above,red] at (0,0) {refl};
\draw[->,thick,cyan] (0,0) arc (-180:140:0.7);
\draw[->,thick,cyan] (0,0) arc (-180:150:1.2);
\node[left,cyan] at (1.4,0) {loop};
\node[right,cyan] at (2.4,0) {loop \AgdaSymbol{⊙} loop $\ldots$};
\draw[->,thick,blue] (0,0) arc (360:40:0.7);
\draw[->,thick,blue] (0,0) arc (360:30:1.2);
\node[right,blue] at (-1.4,0) {!~loop};
\node[left,blue] at (-2.3,0) {$\ldots$ !~loop \AgdaSymbol{⊙} !~loop};
\end{tikzpicture}
\end{center}
The additional structure of types is formalized as follows. Let
\AgdaBound{x}, \AgdaBound{y}, and \AgdaBound{z} be elements of some space
\AgdaBound{A}:
\begin{itemize}
\item For every path \AgdaBound{p} \AgdaSymbol{:} \AgdaBound{x}
$\AgdaDatatype{≡}_\AgdaBound{A}$ \AgdaBound{y}, there exists a path
\AgdaSymbol{!} \AgdaBound{p} \AgdaSymbol{:} \AgdaBound{y}
$\AgdaDatatype{≡}_\AgdaBound{A}$ \AgdaBound{x};
\item For every pair of paths \AgdaBound{p} \AgdaSymbol{:} \AgdaBound{x}
$\AgdaDatatype{≡}_\AgdaBound{A}$ \AgdaBound{y} and \AgdaBound{q}
\AgdaSymbol{:} \AgdaBound{y} $\AgdaDatatype{≡}_\AgdaBound{A}$
\AgdaBound{z}, there exists a path \AgdaBound{p} \AgdaSymbol{⊙}
\AgdaBound{q} \AgdaSymbol{:} \AgdaBound{x} $\AgdaDatatype{≡}_\AgdaBound{A}$
\AgdaBound{z};
\item Subject to the following conditions:
\begin{itemize}
\item \AgdaBound{p} \AgdaSymbol{⊙} \AgdaInductiveConstructor{refl}
\AgdaBound{y} $\AgdaDatatype{≡}_{(\AgdaBound{x} \AgdaDatatype{≡}_A
\AgdaBound{y})}$ \AgdaBound{p};
\item \AgdaBound{p} $\AgdaDatatype{≡}_{(\AgdaBound{x} \AgdaDatatype{≡}_A
\AgdaBound{y})}$ \AgdaInductiveConstructor{refl} \AgdaBound{x}
\AgdaSymbol{⊙} \AgdaBound{p}
\item \AgdaSymbol{!} \AgdaBound{p} \AgdaSymbol{⊙} \AgdaBound{p}
$\AgdaDatatype{≡}_{(\AgdaBound{y} \AgdaDatatype{≡}_A \AgdaBound{y})}$
\AgdaInductiveConstructor{refl} \AgdaBound{y}
\item \AgdaBound{p} \AgdaSymbol{⊙} \AgdaSymbol{!} \AgdaBound{p}
$\AgdaDatatype{≡}_{(\AgdaBound{x} \AgdaDatatype{≡}_A \AgdaBound{x})}$
\AgdaInductiveConstructor{refl} \AgdaBound{x}
\item \AgdaSymbol{!} (\AgdaSymbol{!} \AgdaBound{p})
$\AgdaDatatype{≡}_{(\AgdaBound{x} \AgdaDatatype{≡}_A \AgdaBound{y})}$
\AgdaBound{p}
\item \AgdaBound{p} \AgdaSymbol{⊙} (\AgdaBound{q} \AgdaSymbol{⊙}
\AgdaBound{r}) $\AgdaDatatype{≡}_{(\AgdaBound{x} \AgdaDatatype{≡}_A
\AgdaBound{z})}$ (\AgdaBound{p} \AgdaSymbol{⊙} \AgdaBound{q})
\AgdaSymbol{⊙} \AgdaBound{r}
\end{itemize}
\item This structure repeats one level up and so on ad infinitum.
\end{itemize}
\noindent A space that satisfies the properties above for $n$ levels is
called an $n$-groupoid.
%%%%%%%%%%%%%%%%%%
\subsection{Univalence}
\jc{Do you mean Set or U for the universe? In HoTT the latter is standard,
while Set is really a weird Agda-ism}
In addition to paths between the points within a space like
\AgdaPrimitiveType{Bool}, it is also possible to consider paths between the
space \AgdaPrimitiveType{Bool} and itself by considering
\AgdaPrimitiveType{Bool} as a ``point'' in the universe
\AgdaPrimitiveType{Set} of types. As usual, we have the trivial path which is
given by the constructor \AgdaInductiveConstructor{refl}:
\smallskip
\begin{code}
p : Bool ≡ Bool
p = refl Bool
\end{code}
\smallskip
\noindent There are, however, other (non trivial) paths between
\AgdaPrimitiveType{Bool} and itself and they are justified by the
\emph{univalence} \textbf{axiom}. As an example, the remainder of this
section justifies that there is a path between \AgdaPrimitiveType{Bool} and
itself corresponding to the boolean negation function.
We begin by formalizing the equivalence of functions
\AgdaSymbol{∼}. Intuitively, two functions are equivalent if their results
are propositionally equal for all inputs. A function \AgdaBound{f}
\AgdaSymbol{:} \AgdaBound{A} \AgdaSymbol{→} \AgdaBound{B} is called an
\emph{equivalence} if there are functions \AgdaBound{g} and \AgdaBound{h}
with whom its composition is the identity. Finally two spaces \AgdaBound{A}
and \AgdaBound{B} are equivalent, \AgdaBound{A} \AgdaSymbol{≃} \AgdaBound{B},
if there is an equivalence between them:
\smallskip
\begin{code}
_∼_ : ∀ {ℓ ℓ'} → {A : Set ℓ} {P : A → Set ℓ'} →
(f g : (x : A) → P x) → Set (ℓ ⊔ ℓ')
_∼_ {ℓ} {ℓ'} {A} {P} f g = (x : A) → f x ≡ g x
record isequiv {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} (f : A → B)
: Set (ℓ ⊔ ℓ') where
constructor mkisequiv
field
g : B → A
α : (f ∘ g) ∼ id
h : B → A
β : (h ∘ f) ∼ id
_≃_ : ∀ {ℓ ℓ'} (A : Set ℓ) (B : Set ℓ') → Set (ℓ ⊔ ℓ')
A ≃ B = Σ (A → B) isequiv
\end{code}
\smallskip
We can now formally state the univalence axiom:
\smallskip
\begin{code}
postulate univalence : {A B : Set} → (A ≡ B) ≃ (A ≃ B)
\end{code}
\smallskip
\noindent For our purposes, the important consequence of the univalence axiom
is that equivalence of spaces implies the existence of a path between the
spaces. In other words, in order to assert the existence of a path
\AgdaFunction{notpath} between \AgdaPrimitiveType{Bool} and itself, we need
to prove that the boolean negation function is an equivalence between the
space \AgdaPrimitiveType{Bool} and itself. This is easy to show:
\smallskip
\begin{code}
not2∼id : (not ∘ not) ∼ id
not2∼id false = refl false
not2∼id true = refl true
notequiv : Bool ≃ Bool
notequiv = (not ,
record {
g = not ; α = not2∼id ; h = not ; β = not2∼id })
notpath : Bool ≡ Bool
notpath with univalence
... | (_ , eq) = isequiv.g eq notequiv
\end{code}
\smallskip
\noindent Although the code asserting the existence of a non trivial path
between \AgdaPrimitiveType{Bool} and itself ``compiles,'' it is no longer
executable as it relies on an Agda postulate. In the next section, we analyze
this situation from the perspective of reversible programming languages based
on type isomorphisms~\cite{James:2012:IE:2103656.2103667,rc2011,rc2012}.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Computing with Type Isomorphisms}
\label{pi}
The main syntactic vehicle for the technical developments in this paper is a
simple language called $\Pi$ whose only computations are isomorphisms between
finite types~\citeyearpar{James:2012:IE:2103656.2103667}. After reviewing the
motivation for this language and its relevance to HoTT, we present its syntax
and semantics.
\begin{figure*}[ht]
\[\begin{array}{cc}
\begin{array}{rrcll}
\identlp :& 0 + \tau & \iso & \tau &: \identrp \\
\swapp :& \tau_1 + \tau_2 & \iso & \tau_2 + \tau_1 &: \swapp \\
\assoclp :& \tau_1 + (\tau_2 + \tau_3) & \iso & (\tau_1 + \tau_2) + \tau_3
&: \assocrp \\
\identlt :& 1 * \tau & \iso & \tau &: \identrt \\
\swapt :& \tau_1 * \tau_2 & \iso & \tau_2 * \tau_1 &: \swapt \\
\assoclt :& \tau_1 * (\tau_2 * \tau_3) & \iso & (\tau_1 * \tau_2) * \tau_3
&: \assocrt \\
\distz :&~ 0 * \tau & \iso & 0 &: \factorz \\
\dist :&~ (\tau_1 + \tau_2) * \tau_3 &
\iso & (\tau_1 * \tau_3) + (\tau_2 * \tau_3)~ &: \factor
\end{array}
&
\begin{minipage}{0.5\textwidth}
\begin{center}
\Rule{}
{}
{\jdg{}{}{\idc : \tau \iso \tau}}
{}
~
\Rule{}
{\jdg{}{}{c_1 : \tau_1 \iso \tau_2} \quad \vdash c_2 : \tau_2 \iso \tau_3}
{\jdg{}{}{c_1 \fatsemi c_2 : \tau_1 \iso \tau_3}}
{}
\qquad
\Rule{}
{\jdg{}{}{c_1 : \tau_1 \iso \tau_2} \quad \vdash c_2 : \tau_3 \iso \tau_4}
{\jdg{}{}{c_1 \oplus c_2 : \tau_1 + \tau_3 \iso \tau_2 + \tau_4}}
{}
\qquad
\Rule{}
{\jdg{}{}{c_1 : \tau_1 \iso \tau_2} \quad \vdash c_2 : \tau_3 \iso \tau_4}
{\jdg{}{}{c_1 \otimes c_2 : \tau_1 * \tau_3 \iso \tau_2 * \tau_4}}
{}
\end{center}
\end{minipage}
\end{array}\]
\caption{$\Pi$-combinators~\cite{James:2012:IE:2103656.2103667}
\label{pi-combinators}}
\end{figure*}
%%%%%%%%%%%%%%%%%%%%%
\subsection{Reversibility}
The relevance of reversibility to HoTT is based on the following
analysis. The conventional HoTT approach starts with two, a priori, different
notions: functions and paths, and then postulates an equivalence between a
particular class of functions and paths. As illustrated above, some functions
like \AgdaFunction{not} correspond to paths. Most functions, however, are
evidently unrelated to paths. In particular, any function of type
\AgdaBound{A}~\AgdaSymbol{→}~\AgdaBound{B} that does not have an inverse of
type \AgdaBound{B}~\AgdaSymbol{→}~\AgdaBound{A} cannot have any direct
correspondence to paths as all paths have inverses. An interesting question
then poses itself: since reversible computational models --- in which all
functions have inverses --- are known to be universal computational models,
what would happen if we considered a variant of HoTT based exclusively on
reversible functions? Presumably in such a variant, all functions --- being
reversible --- would potentially correspond to paths and the distinction
between the two notions would vanish making the univalence postulate
unnecessary. This is the precise technical idea we investigate in detail in
the remainder of the paper.
%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Syntax and Semantics of $\Pi$}
\label{opsempi}
The $\Pi$ family of languages is based on type isomorphisms. In the variant
we consider, the set of types $\tau$ includes the empty type 0, the unit type
1, and conventional sum and product types. The values classified by these
types are the conventional ones: $()$ of type 1, $\inl{v}$ and $\inr{v}$ for
injections into sum types, and $(v_1,v_2)$ for product types:
\[\begin{array}{lrcl}
(\textit{Types}) &
\tau &::=& 0 \alt 1 \alt \tau_1 + \tau_2 \alt \tau_1 * \tau_2 \\
(\textit{Values}) &
v &::=& () \alt \inl{v} \alt \inr{v} \alt (v_1,v_2) \\
(\textit{Combinator types}) &&& \tau_1 \iso \tau_2 \\
(\textit{Combinators}) &
c &::=& [\textit{see Fig.~\ref{pi-combinators}}]
\end{array}\]
The interesting syntactic category of $\Pi$ is that of \emph{combinators}
which are witnesses for type isomorphisms $\tau_1 \iso \tau_2$. They consist
of base combinators (on the left side of Fig.~\ref{pi-combinators}) and
compositions (on the right side of the same figure). Each line of the figure
on the left introduces a pair of dual constants\footnote{where $\swapp$ and
$\swapt$ are self-dual.} that witness the type isomorphism in the
middle. This set of isomorphisms is known to be
complete~\cite{Fiore:2004,fiore-remarks} and the language is universal for
hardware combinational
circuits~\cite{James:2012:IE:2103656.2103667}.\footnote{If recursive types
and a trace operator are added, the language becomes Turing
complete~\cite{James:2012:IE:2103656.2103667,rc2011}. We will not be
concerned with this extension in the main body of this paper but it will be
briefly discussed in the conclusion.\jc{but don't we need trace for the Int
construction?}}
From the perspective of category theory, the language $\Pi$ models what is
called a \emph{symmetric bimonoidal category} or a \emph{commutative rig
category}. These are categories with two binary operations and satisfying the
axioms of a commutative rig (i.e., a commutative ring without negative
elements also known as a commutative semiring) up to coherent
isomorphisms. And indeed the types of the $\Pi$-combinators are precisely the
commutative semiring axioms. A formal way of saying this is that $\Pi$ is the
\emph{categorification}~\cite{math/9802029} of the natural numbers. A simple
(slightly degenerate) example of such categories is the category of finite
sets and permutations in which we interpret every $\Pi$-type as a finite set,
interpret the values as elements in these finite sets, and interpret the
combinators as permutations.
\begin{figure}[ht]
\[\begin{array}{r@{\!}lcl}
\evalone{\identlp}{&(\inr{v})} &=& v \\
\evalone{\identrp}{&v} &=& \inr{v} \\
\evalone{\swapp}{&(\inl{v})} &=& \inr{v} \\
\evalone{\swapp}{&(\inr{v})} &=& \inl{v} \\
\evalone{\assoclp}{&(\inl{v})} &=& \inl{(\inl{v})} \\
\evalone{\assoclp}{&(\inr{(\inl{v})})} &=& \inl{(\inr{v})} \\
\evalone{\assoclp}{&(\inr{(\inr{v})})} &=& \inr{v} \\
\evalone{\assocrp}{&(\inl{(\inl{v})})} &=& \inl{v} \\
\evalone{\assocrp}{&(\inl{(\inr{v})})} &=& \inr{(\inl{v})} \\
\evalone{\assocrp}{&(\inr{v})} &=& \inr{(\inr{v})} \\
\evalone{\identlt}{&((),v)} &=& v \\
\evalone{\identrt}{&v} &=& ((),v) \\
\evalone{\swapt}{&(v_1,v_2)} &=& (v_2,v_1) \\
\evalone{\assoclt}{&(v_1,(v_2,v_3))} &=& ((v_1,v_2),v_3) \\
\evalone{\assocrt}{&((v_1,v_2),v_3)} &=& (v_1,(v_2,v_3)) \\
\evalone{\dist}{&(\inl{v_1},v_3)} &=& \inl{(v_1,v_3)} \\
\evalone{\dist}{&(\inr{v_2},v_3)} &=& \inr{(v_2,v_3)} \\
\evalone{\factor}{&(\inl{(v_1,v_3)})} &=& (\inl{v_1},v_3) \\
\evalone{\factor}{&(\inr{(v_2,v_3)})} &=& (\inr{v_2},v_3) \\
\evalone{\idc}{&v} &=& v \\
\evalone{(c_1 \fatsemi c_2)}{&v} &=&
\evalone{c_2}{(\evalone{c_1}{v})} \\
\evalone{(c_1\oplus c_2)}{&(\inl{v})} &=&
\inl{(\evalone{c_1}{v})} \\
\evalone{(c_1\oplus c_2)}{&(\inr{v})} &=&
\inr{(\evalone{c_2}{v})} \\
\evalone{(c_1\otimes c_2)}{&(v_1,v_2)} &=&
(\evalone{c_1}v_1, \evalone{c_2}v_2)
\end{array}\]
\caption{\label{opsem}Operational Semantics}
\end{figure}
In the remainder of this paper, we will be more interested in a model based
on groupoids. But first, we give an operational semantics for $\Pi$.
Operationally, the semantics consists of a pair of mutually recursive
evaluators that take a combinator and a value and propagate the value in the
``forward'' $\triangleright$ direction or in the
``backwards''~$\triangleleft$ direction. We show the complete forward
evaluator in Fig.~\ref{opsem}; the backwards evaluator differs in trivial
ways.
%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Groupoid Model}
Instead of modeling the types of $\Pi$ using sets and the combinators using
permutations we use a semantics that identifies $\Pi$-combinators with
\emph{paths}. More precisely, we model the universe of $\Pi$-types as a space
\AgdaFunction{U} whose points are the individual $\Pi$-types (which are
themselves spaces \AgdaBound{t} containing points). We then postulate that
there is path between the spaces \AgdaBound{t₁} and \AgdaBound{t₂} if there
is a $\Pi$-combinator $c : t_1 \iso t_2$. Our postulate is similar in spirit
to the univalence axiom but, unlike the latter, it has a simple computational
interpretation. A path directly corresponds to a type isomorphism with a
clear operational semantics as presented in the previous section. As we will
explain in more detail below, this approach replaces the datatype
\AgdaSymbol{≡} modeling propositional equality with the datatype
\AgdaSymbol{⟷} modeling type isomorphisms. With this switch, the
$\Pi$-combinators of Fig.~\ref{pi-combinators} become \emph{syntax} for the
paths in the space $U$. Put differently, instead of having exactly one
constructor \AgdaInductiveConstructor{refl} for paths with all other paths
discovered by proofs (see Secs. 2.5--2.12 of the HoTT
book~\citeyearpar{hottbook}) or postulated by the univalence axiom, we have
an \emph{inductive definition} that completely specifies all the paths in the
space $U$.
We begin with the datatype definition of the universe \AgdaFunction{U} of finite
types which are constructed using \AgdaInductiveConstructor{ZERO},
\AgdaInductiveConstructor{ONE}, \AgdaInductiveConstructor{PLUS}, and
\AgdaInductiveConstructor{TIMES}. Each of these finite types will correspond
to a set of points with paths connecting some of the points. The underlying
set of points is computed by \AgdaSymbol{⟦}\_\AgdaSymbol{⟧} as follows:
\AgdaInductiveConstructor{ZERO} maps to the empty set~\AgdaSymbol{⊥},
\AgdaInductiveConstructor{ONE} maps to the singleton set \AgdaSymbol{⊤},
\AgdaInductiveConstructor{PLUS} maps to the disjoint union \AgdaSymbol{⊎},
and \AgdaInductiveConstructor{TIMES} maps to the cartesian product
\AgdaSymbol{×}.
\smallskip
\begin{code}
data U : Set where
ZERO : U
ONE : U
PLUS : U → U → U
TIMES : U → U → U
⟦_⟧ : U → Set
⟦ ZERO ⟧ = ⊥
⟦ ONE ⟧ = ⊤
⟦ PLUS t₁ t₂ ⟧ = ⟦ t₁ ⟧ ⊎ ⟦ t₂ ⟧
⟦ TIMES t₁ t₂ ⟧ = ⟦ t₁ ⟧ × ⟦ t₂ ⟧
\end{code}
\smallskip
We now want to identify paths with $\Pi$-combinators. There is a small
complication however: paths are ultimately defined between points but the
$\Pi$-combinators of Fig.~\ref{pi-combinators} are defined between spaces. We
can bridge this gap using a popular HoTT concept, that of \emph{pointed
spaces}. A pointed space \pointed{\AgdaBound{t}}{\AgdaBound{v}} is a space
\AgdaBound{t} \AgdaSymbol{:} \AgdaFunction{U} with a distinguished value
\AgdaBound{v} \AgdaSymbol{:} \AgdaSymbol{⟦} \AgdaBound{t} \AgdaSymbol{⟧}:
\smallskip
\begin{code}
record U• : Set where
constructor •[_,_]
field
∣_∣ : U
• : ⟦ ∣_∣ ⟧
\end{code}
\smallskip
\AgdaHide{
\begin{code}
open U•
\end{code}
}
\begin{figure*}[ht]
\begin{multicols}{2}
\begin{code}
data _⟷_ : U• → U• → Set where
unite₊ : ∀ {t v} → •[ PLUS ZERO t , inj₂ v ] ⟷ •[ t , v ]
uniti₊ : ∀ {t v} → •[ t , v ] ⟷ •[ PLUS ZERO t , inj₂ v ]
swap1₊ : ∀ {t₁ t₂ v₁} →
•[ PLUS t₁ t₂ , inj₁ v₁ ] ⟷ •[ PLUS t₂ t₁ , inj₂ v₁ ]
swap2₊ : ∀ {t₁ t₂ v₂} →
•[ PLUS t₁ t₂ , inj₂ v₂ ] ⟷ •[ PLUS t₂ t₁ , inj₁ v₂ ]
assocl1₊ : ∀ {t₁ t₂ t₃ v₁} →
•[ PLUS t₁ (PLUS t₂ t₃) , inj₁ v₁ ] ⟷
•[ PLUS (PLUS t₁ t₂) t₃ , inj₁ (inj₁ v₁) ]
assocl2₊ : ∀ {t₁ t₂ t₃ v₂} →
•[ PLUS t₁ (PLUS t₂ t₃) , inj₂ (inj₁ v₂) ] ⟷
•[ PLUS (PLUS t₁ t₂) t₃ , inj₁ (inj₂ v₂) ]
assocl3₊ : ∀ {t₁ t₂ t₃ v₃} →
•[ PLUS t₁ (PLUS t₂ t₃) , inj₂ (inj₂ v₃) ] ⟷
•[ PLUS (PLUS t₁ t₂) t₃ , inj₂ v₃ ]
assocr1₊ : ∀ {t₁ t₂ t₃ v₁} →
•[ PLUS (PLUS t₁ t₂) t₃ , inj₁ (inj₁ v₁) ] ⟷
•[ PLUS t₁ (PLUS t₂ t₃) , inj₁ v₁ ]
assocr2₊ : ∀ {t₁ t₂ t₃ v₂} →
•[ PLUS (PLUS t₁ t₂) t₃ , inj₁ (inj₂ v₂) ] ⟷
•[ PLUS t₁ (PLUS t₂ t₃) , inj₂ (inj₁ v₂) ]
assocr3₊ : ∀ {t₁ t₂ t₃ v₃} →
•[ PLUS (PLUS t₁ t₂) t₃ , inj₂ v₃ ] ⟷
•[ PLUS t₁ (PLUS t₂ t₃) , inj₂ (inj₂ v₃) ]
unite⋆ : ∀ {t v} → •[ TIMES ONE t , (tt , v) ] ⟷ •[ t , v ]
uniti⋆ : ∀ {t v} → •[ t , v ] ⟷ •[ TIMES ONE t , (tt , v) ]
swap⋆ : ∀ {t₁ t₂ v₁ v₂} →
•[ TIMES t₁ t₂ , (v₁ , v₂) ] ⟷ •[ TIMES t₂ t₁ , (v₂ , v₁) ]
assocl⋆ : ∀ {t₁ t₂ t₃ v₁ v₂ v₃} →
•[ TIMES t₁ (TIMES t₂ t₃) , (v₁ , (v₂ , v₃)) ] ⟷
•[ TIMES (TIMES t₁ t₂) t₃ , ((v₁ , v₂) , v₃) ]
assocr⋆ : ∀ {t₁ t₂ t₃ v₁ v₂ v₃} →
•[ TIMES (TIMES t₁ t₂) t₃ , ((v₁ , v₂) , v₃) ] ⟷
•[ TIMES t₁ (TIMES t₂ t₃) , (v₁ , (v₂ , v₃)) ]
distz : ∀ {t v absurd} →
•[ TIMES ZERO t , (absurd , v) ] ⟷ •[ ZERO , absurd ]
factorz : ∀ {t v absurd} →
•[ ZERO , absurd ] ⟷ •[ TIMES ZERO t , (absurd , v) ]
dist1 : ∀ {t₁ t₂ t₃ v₁ v₃} →
•[ TIMES (PLUS t₁ t₂) t₃ , (inj₁ v₁ , v₃) ] ⟷
•[ PLUS (TIMES t₁ t₃) (TIMES t₂ t₃) , inj₁ (v₁ , v₃) ]
dist2 : ∀ {t₁ t₂ t₃ v₂ v₃} →
•[ TIMES (PLUS t₁ t₂) t₃ , (inj₂ v₂ , v₃) ] ⟷
•[ PLUS (TIMES t₁ t₃) (TIMES t₂ t₃) , inj₂ (v₂ , v₃) ]
factor1 : ∀ {t₁ t₂ t₃ v₁ v₃} →
•[ PLUS (TIMES t₁ t₃) (TIMES t₂ t₃) , inj₁ (v₁ , v₃) ] ⟷
•[ TIMES (PLUS t₁ t₂) t₃ , (inj₁ v₁ , v₃) ]
factor2 : ∀ {t₁ t₂ t₃ v₂ v₃} →
•[ PLUS (TIMES t₁ t₃) (TIMES t₂ t₃) , inj₂ (v₂ , v₃) ] ⟷
•[ TIMES (PLUS t₁ t₂) t₃ , (inj₂ v₂ , v₃) ]
id⟷ : ∀ {t v} → •[ t , v ] ⟷ •[ t , v ]
_◎_ : ∀ {t₁ t₂ t₃ v₁ v₂ v₃} → (•[ t₁ , v₁ ] ⟷ •[ t₂ , v₂ ]) →
(•[ t₂ , v₂ ] ⟷ •[ t₃ , v₃ ]) → (•[ t₁ , v₁ ] ⟷ •[ t₃ , v₃ ])
_⊕1_ : ∀ {t₁ t₂ t₃ t₄ v₁ v₂ v₃ v₄} →
(•[ t₁ , v₁ ] ⟷ •[ t₃ , v₃ ]) → (•[ t₂ , v₂ ] ⟷ •[ t₄ , v₄ ]) →
(•[ PLUS t₁ t₂ , inj₁ v₁ ] ⟷ •[ PLUS t₃ t₄ , inj₁ v₃ ])
_⊕2_ : ∀ {t₁ t₂ t₃ t₄ v₁ v₂ v₃ v₄} →
(•[ t₁ , v₁ ] ⟷ •[ t₃ , v₃ ]) → (•[ t₂ , v₂ ] ⟷ •[ t₄ , v₄ ]) →
(•[ PLUS t₁ t₂ , inj₂ v₂ ] ⟷ •[ PLUS t₃ t₄ , inj₂ v₄ ])
_⊗_ : ∀ {t₁ t₂ t₃ t₄ v₁ v₂ v₃ v₄} →
(•[ t₁ , v₁ ] ⟷ •[ t₃ , v₃ ]) → (•[ t₂ , v₂ ] ⟷ •[ t₄ , v₄ ]) →
(•[ TIMES t₁ t₂ , (v₁ , v₂) ] ⟷ •[ TIMES t₃ t₄ , (v₃ , v₄) ])
\end{code}
\end{multicols}
\caption{Pointed version of $\Pi$-combinators or inductive definition of paths
\label{pointedcomb}}
\end{figure*}
\noindent Pointed spaces are often necessary in homotopy theory as various
important properties of spaces depend on the chosen basepoint. In our
setting, pointed spaces allow us to re-express the $\Pi$-combinators in a way
that unifies their status as isomorphisms between \emph{types} and as paths
between \emph{points} as shown in Fig.~\ref{pointedcomb}. The new
presentation of combinators directly relates points to points and in fact
subsumes the operational semantics of Fig.~\ref{opsem}. For example, note
that the $\Pi$-combinator $\swapp : \tau_1 + \tau_2 \iso \tau_2 + \tau_1$
requires two clauses in the interpreter:
\[\begin{array}{r@{\!}lcl}
\evalone{\swapp}{&(\inl{v})} &=& \inr{v} \\
\evalone{\swapp}{&(\inr{v})} &=& \inl{v}
\end{array}\]
These two clauses give rise to two path constructors
\AgdaInductiveConstructor{swap1₊} and \AgdaInductiveConstructor{swap2₊}. When
viewed as maps between unpointed spaces, both constructors map from
\AgdaInductiveConstructor{PLUS} \AgdaBound{t₁} \AgdaBound{t₂} to
\AgdaInductiveConstructor{PLUS} \AgdaBound{t₂} \AgdaBound{t₁}. When, however,
viewed as maps between points spaces, each constructor specifies in addition
its action on the point in a way that mirrors the semantic evaluation
rule. The situation is the same for all other $\Pi$-constructors. \jc{The
operational semantics have $24$ rules, while the groupoid model has $26$.
This is because of the 2 rules with \emph{absurd} in them. How shall they
be explained?}
We note that the refinement of the $\Pi$-combinators to combinators on
pointed spaces is given by an inductive family for \emph{heterogeneous}
equality that generalizes the usual inductive family for propositional
equality. Put differently, what used to be the only constructor for paths
\AgdaInductiveConstructor{refl} is now just one of the many constructors
(named \AgdaInductiveConstructor{id⟷} in the figure). Among the new
constructors we have \AgdaInductiveConstructor{◎} that constructs path
compositions. By construction, every combinator has an inverse calculated as
shown in Fig.~\ref{sym}. These constructions are sufficient to guarantee that
the universe~\AgdaFunction{U} is a groupoid \jc{point to the proof in
some accompanying full Agda code?}. Additionally, we have paths that
connect values in different but isomorphic spaces like
\pointed{{\AgdaInductiveConstructor{TIMES} \AgdaBound{t₁}
\AgdaBound{t₂}}}{{\AgdaSymbol{(} \AgdaBound{v₁} \AgdaSymbol{,} \AgdaBound{v₂}
\AgdaSymbol{)}}} and \pointed{{\AgdaInductiveConstructor{TIMES}
\AgdaBound{t₂} \AgdaBound{t₁}}}{{\AgdaSymbol{(} \AgdaBound{v₂} \AgdaSymbol{,}
\AgdaBound{v₁} \AgdaSymbol{)}}}.
\begin{figure}[ht]
\setlength{\columnsep}{12pt}
\begin{multicols}{2}
\begin{code}
! : {t₁ t₂ : U•} → (t₁ ⟷ t₂) → (t₂ ⟷ t₁)
! unite₊ = uniti₊
! uniti₊ = unite₊
! swap1₊ = swap2₊
! swap2₊ = swap1₊
! assocl1₊ = assocr1₊
! assocl2₊ = assocr2₊
! assocl3₊ = assocr3₊
! assocr1₊ = assocl1₊
! assocr2₊ = assocl2₊
! assocr3₊ = assocl3₊
! unite⋆ = uniti⋆
! uniti⋆ = unite⋆
! swap⋆ = swap⋆
! assocl⋆ = assocr⋆
! assocr⋆ = assocl⋆
! distz = factorz
! factorz = distz
! dist1 = factor1
! dist2 = factor2
! factor1 = dist1
! factor2 = dist2
! id⟷ = id⟷
! (c₁ ◎ c₂) = ! c₂ ◎ ! c₁
! (c₁ ⊕1 c₂) = ! c₁ ⊕1 ! c₂
! (c₁ ⊕2 c₂) = ! c₁ ⊕2 ! c₂
! (c₁ ⊗ c₂) = ! c₁ ⊗ ! c₂
\end{code}
\end{multicols}
\caption{\label{sym}Pointed Combinators (or paths) inverses}
\end{figure}
The example \AgdaFunction{notpath} which earlier required the use of the
univalence axiom can now be directly defined using
\AgdaInductiveConstructor{swap1₊} and \AgdaInductiveConstructor{swap2₊}. To
see this, note that \AgdaPrimitiveType{Bool} can be viewed as a shorthand for
\AgdaInductiveConstructor{PLUS} \AgdaInductiveConstructor{ONE}
\AgdaInductiveConstructor{ONE} with \AgdaInductiveConstructor{true} and
\AgdaInductiveConstructor{false} as shorthands for
\AgdaInductiveConstructor{inj₁} \AgdaInductiveConstructor{tt} and
\AgdaInductiveConstructor{inj₂} \AgdaInductiveConstructor{tt}. With this in
mind, the path corresponding to boolean negation consists of two ``fibers'',
one for each boolean value as shown below:
\AgdaHide{
\begin{code}
_⟷⟨_⟩_ : (t₁ : U•) {t₂ : U•} {t₃ : U•} →
(t₁ ⟷ t₂) → (t₂ ⟷ t₃) → (t₁ ⟷ t₃)
_ ⟷⟨ α ⟩ β = α ◎ β
_□ : (t : U•) → {t : U•} → (t ⟷ t)
_□ t = id⟷
\end{code}
}
\smallskip
\begin{code}
data Path (t₁ t₂ : U•) : Set where
path : (c : t₁ ⟷ t₂) → Path t₁ t₂
ZERO• : {absurd : ⟦ ZERO ⟧} → U•
ZERO• {absurd} = •[ ZERO , absurd ]
ONE• : U•
ONE• = •[ ONE , tt ]
BOOL : U
BOOL = PLUS ONE ONE
TRUE FALSE : ⟦ BOOL ⟧
TRUE = inj₁ tt
FALSE = inj₂ tt
BOOL•F : U•
BOOL•F = •[ BOOL , FALSE ]
BOOL•T : U•
BOOL•T = •[ BOOL , TRUE ]
NOT•T : BOOL•T ⟷ BOOL•F
NOT•T = swap1₊
NOT•F : BOOL•F ⟷ BOOL•T
NOT•F = swap2₊
notpath•T : Path BOOL•T BOOL•F
notpath•T = path NOT•T
notpath•F : Path BOOL•F BOOL•T
notpath•F = path NOT•F
\end{code}
\smallskip
\noindent In other words, a path between spaces is really a collection of
paths connecting the various points. Note however that we never need to
``collect'' these paths using a universal quantification.
\jc{Shouldn't we also show that \AgdaPrimitiveType{Bool} contains
exactly $2$ things, and that TRUE and FALSE are ``different'' ?}
\jc{The other thing is, whereas not used to be a path between Bool and
Bool, we no longer have that. Shouldn't we show that, somehow,
BOOL and BOOL.F 'union' BOOL.T are somehow ``equivalent''? And there
there is a coherent notpath built the same way? Especially since I
am sure it is quite easy to build incoherent sets of paths!}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Computing with Paths}
The previous section presented a language $\Pi$ whose computations are all
the possible isomorphisms between finite types. (Recall that the commutative
semiring structure is sound and complete for isomorphisms between finite
types~\cite{Fiore:2004,fiore-remarks}.) Instead of working with arbitrary
functions, then restricting them to equivalences, and then postulating that
these equivalences give rise to paths, the approach based on $\Pi$ starts
directly with the full set of possible isomorphisms and encodes it as an
inductive datatype of paths between pointed spaces. The resulting structure
is evidently a 1-groupoid as the isomorphisms are closed under inverses and
composition. We now investigate the higher groupoid structure.