forked from martinescardo/HoTT-UF-Agda-Lecture-Notes
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathHoTT-UF-Agda.lagda
7669 lines (6227 loc) · 300 KB
/
HoTT-UF-Agda.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
---
layout: default
title : Introduction to Homotopy Type Theory and Univalent Foundations (HoTT/UF) with Agda
date : 2019-03-04
---
<!--
* This file is not meant to be read by people.
* It is used to automatically generate the following files, which are
meant to be read by people:
- https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/HoTT-UF-Agda.html
- https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/HoTT-UF-Agda.pdf
- https://github.com/martinescardo/HoTT-UF-Agda-Lecture-Notes/tree/master/agda
The html file is better rendered and probably easier to read than the
pdf file, but both have internal links, including to the Agda
definitions.
-->
## <a id="lecturenotes">Introduction to Univalent Foundations of Mathematics with Agda</a>
4th March 2019, version of {{ "now" | date: "%d %B %Y, %H:%M" }}.
[Martín Hötzel Escardó](https://www.cs.bham.ac.uk/~mhe/),
[School of Computer Science](https://www.cs.bham.ac.uk/),
[University of Birmingham](http://www.bham.ac.uk/),
UK.
[<sub>Table of contents ⇓</sub>](HoTT-UF-Agda.html#contents)
**Abstract.** We introduce [Voevodsky](https://www.math.ias.edu/Voevodsky/)'s [univalent foundations](https://www.ams.org/journals/bull/2018-55-04/S0273-0979-2018-01616-9/) and
[univalent mathematics](https://github.com/UniMath/UniMath/blob/master/README.md), and explain how to develop them with the
computer system [Agda](https://wiki.portal.chalmers.se/agda/pmwiki.php), which is based on [Martin-Löf type theory](https://github.com/michaelt/martin-lof).
Agda allows us to write mathematical definitions, constructions,
theorems and proofs, for example in number theory, analysis, group
theory, topology, category theory or programming language theory, checking
them for logical and mathematical correctness.
Agda is a constructive mathematical system by default, which amounts
to saying that it can also be considered as a programming language for
manipulating mathematical objects. But we can assume the axiom of
choice or the principle of excluded middle for pieces of mathematics
that require them, at the cost of losing the implicit
programming-language character of the system. For a fully
constructive development of univalent mathematics in Agda, we would
need to use its new [cubical
flavour](https://homotopytypetheory.org/2018/12/06/cubical-agda/), and
we hope these notes provide a base for researchers interested in
learning Cubical Type Theory and Cubical Agda as the next step.
Compared to most expositions of the subject, we work with explicit
universe levels.
**Keywords.** Univalent mathematics. Univalent foundations. Univalent
type theory. Univalence axiom. `∞`-Groupoid. Homotopy type. Type
theory. Homotopy type theory. Intensional Martin-Löf type
theory. Dependent type theory. Identity type. Type
universe. Constructive mathematics. Agda. Cubical type
theory. Cubical Agda. Computer-verified mathematics.
**About this document.**
[This](https://github.com/martinescardo/HoTT-UF-Agda-Lecture-Notes) is a set
of so-called
[literate](https://agda.readthedocs.io/en/latest/tools/literate-programming.html)
Agda files, with the formal, verified, mathematical development within
*code* environments, and the usual mathematical discussion outside
them.
Most of this file is not Agda code, and is in markdown format, and the
html web page is generated automatically from it using Agda and other
tools. [Github](https://github.com/martinescardo/HoTT-UF-Agda-Lecture-Notes)
pull requests by students to fix typos or mistakes and clarify
ambiguities are welcome.
There is also a [pdf
version](https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/HoTT-UF-Agda.pdf)
automatically generated from the [html version](https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/index.html).
These notes were originally developed for the
[Midlands Graduate School 2019](http://events.cs.bham.ac.uk/mgs2019/). They will evolve for a while.
[<sub>Table of contents ⇓</sub>](HoTT-UF-Agda.html#contents)
### <a id="introduction"></a> Introduction
A univalent type theory is the underlying formal system for a
foundation of univalent mathematics as conceived by [Voevodsky](https://www.math.ias.edu/Voevodsky/).
In the same way as there isn't just one set theory (we have e.g. [ZFC](https://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_theory)
and [NBG](https://en.wikipedia.org/wiki/Von_Neumann%E2%80%93Bernays%E2%80%93G%C3%B6del_set_theory) among others), there isn't just one univalent type theory (we
have e.g. the underlying type theory used in [UniMath](https://github.com/UniMath/UniMath), [HoTT-book type
theory](https://homotopytypetheory.org/2015/01/07/the-hott-book-does-not-define-hott/), and [cubical type theory](https://arxiv.org/abs/1611.02108), among others, and more are expected
to come in the foreseeable future before the foundations of univalent
mathematics stabilize).
The salient differences between univalent mathematics and traditional,
set-based mathematics may be shocking at first sight:
1. The kinds of objects we take as basic.
- Certain things called types, or higher groupoids, rather than sets, are the primitive objects.
- Sets, also called 0-groupoids, are particular kinds of types.
- So we have more general objects as a starting point.
- E.g. the type `ℕ` of natural numbers is a set, and this is a theorem, not a definition.
- E.g. the type of monoids is not a set, but instead a `1`-groupoid, automatically.
- E.g. the type of categories is a `2`-groupoid, again automatically.
2. The treatment of logic.
- Mathematical statements are interpreted as types rather than truth values.
- Truth values are particular kinds of types, called `-1`-groupoids, with at most one element.
- Logical operations are particular cases of mathematical operations on types.
- The mathematics comes first, with logic as a derived concept.
- E.g. when we say "and", we are taking the cartesian product of two types, which may or may not be truth values.
3. The treatment of equality.
- The value of an equality `x ≡ y` is a type, called the *identity type*, which is not necessarily a truth value.
- It collects the ways in which the mathematical objects `x` and `y` are identified.
- E.g. it is a truth value for elements of `ℕ`, as there is at most one way for two natural numbers to be equal.
- E.g. for the [type of monoids](HoTT-UF-Agda.html#magmasandmonoids), it is a set, amounting to the type of monoid isomorphisms, automatically.
- E.g. for the type of categories, it is a `1`-groupoid, amounting to the type of equivalences of categories, again automatically.
The important word in the above description of univalent foundations
is *automatic*. For example, we don't *define* equality of monoids to
be isomorphism. Instead, we define the collection of monoids as the
large type of small types that are sets, equipped with a binary
multiplication operation and a unit satisfying associativity of
multiplication and neutrality of the unit in the usual way, and then
we *prove* that the native notion of equality that comes with
univalent type theory (inherited from Martin-Löf type theory) happens
to coincide with monoid isomorphism. Largeness and smallness are taken
as relative concepts, with type *universes* incorporated in the theory
to account for this distinction.
Voevodsky's way to achive this is to start with a Martin-Löf type
theory (MLTT), including identity types and type universes, and
postulate a single axiom, named *univalence*. This axiom stipulates a
[canonical](http://mathworld.wolfram.com/Canonical.html) bijection
between *type equivalences* (in a suitable sense defined by Voevodsky
in type theory) and *type identifications* (in the original sense of
Martin-Löf's identity type). Voevodsky's notion of type equivalence,
formulated in MLTT, is a refinement of the notion of isomorphism,
which works uniformly for all higher groupoids, i.e. types.
In particular, Voevodsky didn't design a new type theory, but instead
gave an axiom for an existing type theory (or any of a family of
possible type theories, to be more precise).
The main *technical* contributions in type theory by Voevodsky are:
<ol start="4">
<li>The definition of type levels in MLTT, classifying them as n-groupoids including the possibility n=∞.</li>
<li>The (simple and elegant) definition of type equivalence that works uniformly for all type levels in MLTT.</li>
<li> The formulation of the univalence axiom in MLTT.</li>
</ol>
Univalent mathematics begins within MLTT with (4) and (5) before we
postulate univalence. In fact, as the reader will see, we will do a
fair amount of univalent mathematics before we formulate or assume the
univalence axiom.
All of (4)-(6) crucially rely on Martin-Löf's identity
type. [Initially](https://faculty.math.illinois.edu/~dan/Papers/ITP-talk.pdf), Voevodsky thought that a new concept would be needed
in the type theory to achieve (4)-(6) and hence (1) and (3) above. But
he eventually discovered that Martin-Löf's identity type is precisely
what he needed.
It may be considered somewhat miraculous that the addition of the
univalence axiom alone to MLTT can achieve (1) and (3). Martin-Löf
type theory was designed to achieve (2), and, regarding (1), types
were imagined/conceived as sets (and even named *sets* in some of the
original expositions by Martin-Löf), and, regarding (3), the identity
type was imagined/conceived as having at most one element, even if
MLTT cannot prove or disprove this statement, as was eventually
shown by
[Hofmann](https://www.tcs.ifi.lmu.de/mitarbeiter/martin-hofmann) and
[Streicher](https://en.wikipedia.org/wiki/Thomas_Streicher) with their
[groupoid model of types](https://ieeexplore.ieee.org/document/316071)
in the early 1990's.
Another important aspect of univalent mathematics is the presence of
explicit mechanisms for distinguishing
<ol start="7">
<li>property (e.g. an unspecified thing exists),</li>
<li>data or structure (e.g. a designated thing exists or is given),</li>
</ol>
which are common place in current mathematical practice
(e.g. cartesian closedness of a category is a property in some sense
(up to isomorphism), whereas monoidal closedness is given structure).
In summary, univalent mathematics is characterized by (1)-(8) and not
by the univalence axiom alone. In fact, half of theses notes begin
*without* the univalence axiom (as measured by the number of lines in
these lecture notes until we formulate the univalence axiom and start
to use it).
Lastly, univalent type theories don't assume the axiom of choice or
the principle of excluded middle, and so in some sense they are
constructive by default. But we emphasize that these two axioms are
consistent and hence can be safely used as assumptions. However,
virtually all theorems of univalent mathematics, e.g. in
[UniMath](https://github.com/UniMath/UniMath/blob/master/README.md),
have been proved without assuming them, with natural mathematical
arguments. The formulations of theses principles in univalent
mathematics differ from their traditional formulations in MLTT, and
hence we sometimes refer to them as the *univalent* principle of
excluded middle and the *univalent* axiom of choice.
In these notes we will explore the above ideas, using Agda to write
MLTT definitions, constructions, theorems and proofs, with
univalence as an explicit assumption each time it is needed. We will
have a further assumption, the existence of certain subsingleton (or
propositional, or truth-value) truncations in order to be able to deal
with the distinction between property and data, and in particular with
the distinction between designated and unspecified existence (for
example to be able to define the notions of image of a function and of
surjective function). However, we will not assume them globally, so
that the students can see clearly when univalence or truncation are or
are not needed. In fact, the foundational definitions, constructions,
theorems and proofs of univalent mathematics don't require univalence
or propositional truncation, and so can be developed in a version of
the original Martin-Löf type theories, and this is what happens in
these notes, and what Voevodsky did in his brilliant [original
development in the computer system
Coq](https://github.com/UniMath/Foundations). Our use of Agda, rather
than Coq, is a personal matter of taste only, and the students are
encouraged to learn Coq, too.
[<sub>Table of contents ⇓</sub>](HoTT-UF-Agda.html#contents)
#### <a id="homotopytypetheory"></a> Homotopy type theory
Univalent type theory is often called *homotopy type theory*. Here we
are following Voevodsky, who coined the phrases *univalent
foundations* and *univalent mathematics*.
We regard the terminology *homotopy type theory* as probably more
appropriate for referring to the *synthetic* development of homotopy
theory within univalent mathematics, for which we refer the reader to
the [HoTT book](https://homotopytypetheory.org/book/).
However, the terminology *homotopy type theory* is also used as a
synonym for univalent type theory, not only because univalent type
theory has a model in homotopy types (as defined in homotopy theory),
but also because, without considering models, types do behave like
homotopy types, automatically. We will not discuss how to do homotopy
theory using univalent type theory in these notes. We refer the reader
to the HoTT book as a starting point.
A common compromise is to refer to the subject as [HoTT/UF](https://cas.oslo.no/hott-uf/).
[<sub>Table of contents ⇓</sub>](HoTT-UF-Agda.html#contents)
#### <a id="generalreferences"></a> General references
- [Papers](https://github.com/michaelt/martin-lof) by [Martin-Löf](https://en.wikipedia.org/wiki/Per_Martin-L%C3%B6f).
- Homotopy type theory website [references](https://homotopytypetheory.org/references/).
- [HoTT book](https://homotopytypetheory.org/book/).
- `ncatlab` [references](https://ncatlab.org/nlab/show/homotopy+type+theory#References).
It particular, it is recommended to read the concluding notes for each
chapter in the HoTT book for discussion of original sources. Moreover,
the whole HoTT book is a recommended complementary reading for this
course.
And, after the reader has gained enough experience:
- Voevodsky's original [foundations of univalent mathematics in Coq](https://github.com/vladimirias/Foundations).
- [UniMath project](https://github.com/UniMath/UniMath) in [Coq](https://coq.inria.fr/).
- [Coq HoTT library](https://github.com/HoTT/HoTT).
- [Agda HoTT library](https://github.com/HoTT/HoTT-Agda).
Regarding the computer language Agda, we recommend the following as
starting points:
- [Agda wiki](https://wiki.portal.chalmers.se/agda/pmwiki.php).
- [Dependent types at work](http://www.cse.chalmers.se/~peterd/papers/DependentTypesAtWork.pdf) by Ana Bove and Peter Dybjer.
- [Agda reference manual](https://agda.readthedocs.io/en/latest/getting-started/index.html).
- [Agda further references](https://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Documentation).
- [Cubical Agda blog post](https://homotopytypetheory.org/2018/12/06/cubical-agda/) by Anders Mörtberg.
- [Cubical Agda documentation](https://agda.readthedocs.io/en/latest/language/cubical.html#cubical).
Regarding the genesis of the subject:
- [A very short note on homotopy λ-calculus](http://math.ucr.edu/home/baez/Voevodsky_note.ps).
- [Notes on homotopy λ-calculus](https://github.com/vladimirias/2006_03_Homotopy_lambda_calculus/blob/master/homotopy_lambda_calculus_Mar_5_2006.pdf).
Voevodsky [says](https://www.math.ias.edu/vladimir/sites/math.ias.edu.vladimir/files/2014_04_22_slides.pdf)
that he was influenced by [Makkai](https://www.math.mcgill.ca/makkai/)'s thinking:
- [FOLDS](https://www.math.mcgill.ca/makkai/folds/foldsinpdf/FOLDS.pdf).
- [The theory of abstract sets based on first-order logic with dependent types](https://www.math.mcgill.ca/makkai/Various/MateFest2013.pdf).
An important foundational reference, by Steve Awodey and Michael A. Warren, is
- [Homotopy theoretic models of identity types](https://arxiv.org/abs/0709.0248).
Additional expository material:
- [An introduction to univalent foundations for mathematicians](https://www.ams.org/journals/bull/2018-55-04/S0273-0979-2018-01616-9/), a paper at the [Bulletin of the
AMS](https://www.ams.org/publications/journals/journalsframework/bull)
by [Dan Grayson](https://faculty.math.illinois.edu/~dan/).
- [Voevodsky's Memorial talk](https://faculty.math.illinois.edu/~dan/Talks/Voevodsky-memorial-talk.pdf)
by [Dan Grayson](https://faculty.math.illinois.edu/~dan/).
- [Univalent foundations - an introduction](https://benediktahrens.net/talks/6WFT.pdf) by Benedikt Ahrens.
- [Introduction to Homotopy Type Theory](https://github.com/EgbertRijke/HoTT-Intro) by Egbert Rijke.
- [A course on homotopy (type) theory](http://math.andrej.com/2019/05/08/a-course-on-homotopy-type-theory/) by Andrej Bauer and Jaka Smrekar.
- [15-819 Homotopy Type Theory](https://www.cs.cmu.edu/~rwh/courses/hott/) by Bob Harper.
- [Homotopy type theory: the logic of space](https://arxiv.org/abs/1703.03007) by Mike Shulman.
- [Logic in univalent type theory](https://www.newton.ac.uk/seminar/20170711100011001) by Martin Escardo.
More references as clickable links are given in the course of the notes.
We also have an [Agda development](https://www.cs.bham.ac.uk/~mhe/agda-new/)
of [univalent
foundations](https://www.cs.bham.ac.uk/~mhe/agda-new/UF.html) which is
applied to work on [injective
types](https://www.cs.bham.ac.uk/~mhe/agda-new/InjectiveTypes-article.html),
[compact (or searchable)
types](https://www.cs.bham.ac.uk/~mhe/agda-new/Compactness.html),
[compact
ordinals](https://www.cs.bham.ac.uk/~mhe/agda-new/Ordinals.html) and
[more](https://www.cs.bham.ac.uk/~mhe/agda-new/SafeModulesIndex.html).
[<sub>Table of contents ⇓</sub>](HoTT-UF-Agda.html#contents)
### <a id="plan"></a> Choice of material
This is intended as an introductory graduate course. We include what
we regard as the essence of univalent foundations and univalent
mathematics, but we are certainly omitting important material that is
needed to do univalent mathematics in practice, and the readers who wish
to practice univalent mathematics should consult the above references.
### <a id="contents"></a> Table of contents
1. [Front matter](HoTT-UF-Agda.html#lecturenotes)
1. [Title, abstract, keywords and about](HoTT-UF-Agda.html#lecturenotes)
1. [Introduction](HoTT-UF-Agda.html#introduction)
1. [Homotopy type theory](HoTT-UF-Agda.html#homotopytypetheory)
1. [General references](HoTT-UF-Agda.html#generalreferences)
1. [Choice of material](HoTT-UF-Agda.html#plan)
1. [MLTT in Agda](HoTT-UF-Agda.html#mlttinagda)
1. [A spartan Martin-Löf type theory (MLTT)](HoTT-UF-Agda.html#spartanmltt)
1. [What is Agda?](HoTT-UF-Agda.html#whatisagda)
1. [Getting started with Agda](HoTT-UF-Agda.html#gettingstartedagda)
1. [Universes `𝓤,𝓥,𝓦`](HoTT-UF-Agda.html#universes)
1. [The one-element type `𝟙`](HoTT-UF-Agda.html#onepointtype)
1. [The empty type `𝟘`](HoTT-UF-Agda.html#emptytype)
1. [The type `ℕ` of natural numbers](HoTT-UF-Agda.html#naturalnumbers)
1. [The binary sum type constructor `_+_`](HoTT-UF-Agda.html#binarysum)
1. [`Σ` types](HoTT-UF-Agda.html#sigmatypes)
1. [`Π` types](HoTT-UF-Agda.html#pitypes)
1. [The identity type former `Id`, also written `_≡_`](HoTT-UF-Agda.html#identitytype)
1. [Basic constructions with the identity type](HoTT-UF-Agda.html#basicidentity)
1. [Reasoning with negation](HoTT-UF-Agda.html#negation)
1. [Example: formulation of the twin-prime conjecture](HoTT-UF-Agda.html#twinprime)
1. [Remaining Peano axioms and basic arithmetic](HoTT-UF-Agda.html#basicarithmetic)
1. [Univalent Mathematics in Agda](HoTT-UF-Agda.html#uminagda)
1. [Our univalent type theory](HoTT-UF-Agda.html#axiomaticutt)
1. [Subsingletons (or propositions or truth values) and sets](HoTT-UF-Agda.html#subsingletonsandsets)
1. [The types of magmas and monoids](HoTT-UF-Agda.html#magmasandmonoids)
1. [The identity type in univalent mathematics](HoTT-UF-Agda.html#identitytypeuf)
1. [Identifications that depend on identifications](HoTT-UF-Agda.html#dependentequality)
1. [Equality in Σ types](HoTT-UF-Agda.html#sigmaequality)
1. [Voevodsky's notion of hlevel](HoTT-UF-Agda.html#hlevel)
1. [The univalent principle of excluded middle](HoTT-UF-Agda.html#em)
1. [Hedberg's Theorem](HoTT-UF-Agda.html#hedberg)
1. [A characterization of sets](HoTT-UF-Agda.html#setscharacterization)
1. [Subsingletons are sets](HoTT-UF-Agda.html#subsingletonsaresets)
1. [The types of hlevel 1 are the subsingletons](HoTT-UF-Agda.html#hlevel1subsingleton)
1. [The types of hlevel 2 are the sets](HoTT-UF-Agda.html#hlevel2set)
1. [The hlevels are upper closed](HoTT-UF-Agda.html#hlevelsupper)
1. [ℕ is a set](HoTT-UF-Agda.html#naturalsset)
1. [Retracts](HoTT-UF-Agda.html#retracts)
1. [Voevodsky' notion of type equivalence](HoTT-UF-Agda.html#fibersandequivalences)
1. [Voevodsky's univalence axiom](HoTT-UF-Agda.html#univalence)
1. [Example of a type that is not a set under univalence](HoTT-UF-Agda.html#notsets)
1. [Exercises](HoTT-UF-Agda.html#lefttothereader)
1. [Solutions](HoTT-UF-Agda.html#solutions)
1. [A characterization of univalence](HoTT-UF-Agda.html#unicharac)
1. [Equivalence induction](HoTT-UF-Agda.html#equivalenceinduction)
1. [Half adjoint equivalences](HoTT-UF-Agda.html#haes)
1. [Function extensionality from univalence](HoTT-UF-Agda.html#funextfromua)
1. [Variations of function extensionality and their logical equivalence](HoTT-UF-Agda.html#hfunext)
1. [Universes are map classifiers](HoTT-UF-Agda.html#typeclassifier)
1. [The univalence axiom is a (sub)singleton type](HoTT-UF-Agda.html#univalencesubsingleton)
1. [`hfunext` and `vvfunext` are subsingletons](HoTT-UF-Agda.html#hfunextsubsingleton)
1. [More consequences of function extensionality](HoTT-UF-Agda.html#morefunextuses)
1. [Propositional extensionality and the powerset](HoTT-UF-Agda.html#propositionalextensionality)
1. [Some constructions with types of equivalences](HoTT-UF-Agda.html#equivconstructions)
1. [Type embeddings](HoTT-UF-Agda.html#embeddings)
1. [The Yoneda Lemma for types](HoTT-UF-Agda.html#yoneda)
1. [Universe lifting](HoTT-UF-Agda.html#universelifting)
1. [The subtype classifier and other classifiers](HoTT-UF-Agda.html#subtypeclassifier)
1. [Magma equivalences](HoTT-UF-Agda.html#magmaequivalences)
1. [Subsingleton truncation, disjunction and existence](HoTT-UF-Agda.html#truncation)
1. [The univalent axiom of choice](HoTT-UF-Agda.html#choice)
1. [Propositional resizing](HoTT-UF-Agda.html#resizing)
1. [Summary of consistent axioms for univalent mathematics](HoTT-UF-Agda.html#summary)
1. [Appendix](HoTT-UF-Agda.html#appendix)
1. [Solutions to some exercises](HoTT-UF-Agda.html#someexercisessol)
1. [Additional exercises](HoTT-UF-Agda.html#moreexercises)
1. [Solutions to additional exercises](HoTT-UF-Agda.html#additionalexercisessol)
1. [Operator fixities and precedences](HoTT-UF-Agda.html#infixop)
1. [Agda files automatically extracted from these notes](https://github.com/martinescardo/HoTT-UF-Agda-Lecture-Notes/tree/master/agda)
1. [The sources for these notes](https://github.com/martinescardo/HoTT-UF-Agda-Lecture-Notes)
1. [License](LICENSE)
[<sub>Table of contents ⇑</sub>](HoTT-UF-Agda.html#contents)
## <a id="mlttinagda"></a> MLTT in Agda
### <a id="whatisagda"></a> What is Agda?
There are [two views](https://agda.readthedocs.io/en/latest/getting-started/what-is-agda.html):
1. Agda is a dependently-typed functional programming language.
2. Agda is a language for defining mathematical notions (e.g. group
or topological space), formulating constructions to be performed
(e.g. a type of real numbers, a group structure on the integers, a
topology on the reals), formulating theorems (e.g. a certain
construction is indeed a group structure, there are infinitely
many primes), and proving theorems (e.g. the infinitude of the
collection of primes with Euclid's argument).
This doesn't mean that Agda has two sets of features, one for (1) and
the other for (2). The same set of features account simultaneously for
(1) and (2). Programs are mathematical constructions that happen not
to use non-constructive principles such as excluded middle.
In these notes we study a minimal univalent type theory and do
mathematics with it using a minimal subset of the computer language Agda
as a vehicle.
Agda allows one to construct proofs interactively, but we will not
discuss how to do this in these notes. Agda is not an automatic
theorem prover. We have to come up with our own proofs, which Agda
checks for correctness. We do get some form of interactive help to
input our proofs and render them as formal objects.
[<sub>Table of contents ⇑</sub>](HoTT-UF-Agda.html#contents)
### <a id="spartanmltt"></a> A spartan Martin-Löf type theory (MLTT)
Before embarking into a full definition of our Martin-Löf type
theory in Agda, we summarize the particular Martin-Löf type
theory that we will consider, by naming the concepts that we will
include. We will have:
* An empty type [`𝟘`](HoTT-UF-Agda.html#emptytype).
* A one-element type [`𝟙`](HoTT-UF-Agda.html#onepointtype).
* A type of [`ℕ`](HoTT-UF-Agda.html#naturalnumbers) natural numbers.
* Type formers [`+`](HoTT-UF-Agda.html#binarysum) (binary sum),
[`Π`](HoTT-UF-Agda.html#pitypes) (product),
[`Σ`](HoTT-UF-Agda.html#sigmatypes) (sum),
[`Id`](HoTT-UF-Agda.html#identitytype) (identity type).
* [Universes](HoTT-UF-Agda.html#universes) (types of types), ranged
over by `𝓤,𝓥,𝓦`.
This is enough to do number theory, analysis, group theory, topology, category theory and more.
spartan
/ˈspɑːt(ə)n/
adjective:
showing or characterized by austerity or a lack of comfort or
luxury.
We will also be rather spartan with the subset of Agda that we choose
to discuss. Many things we do here can be written in more concise ways
using more advanced features. Here we introduce a minimal
subset of Agda where everything in our spartan MLTT can be expressed.
[<sub>Table of contents ⇑</sub>](HoTT-UF-Agda.html#contents)
### <a id="gettingstartedagda"></a> Getting started with Agda
We don't use any Agda library. For pedagogical purposes, we start from
scratch, and here are our first two lines of code:
\begin{code}
{-# OPTIONS --without-K --exact-split --safe #-}
module HoTT-UF-Agda where
\end{code}
* The option [`--without-K`](https://agda.readthedocs.io/en/latest/language/without-k.html) disables [Streicher's `K` axiom](https://ncatlab.org/nlab/show/axiom+K+%28type+theory%29), which we don't
want for univalent mathematics.
* The option [`--exact-split`](https://agda.readthedocs.io/en/latest/language/function-definitions.html#case-trees) makes Agda to only accept definitions
with the equality sign "`=`" that behave like so-called
*judgmental* or *definitional* equalities.
* The option [`--safe`](https://agda.readthedocs.io/en/latest/language/safe-agda.html#safe-agda) disables features that may make Agda
inconsistent,
such as `--type-in-type`, postulates and more.
* Every Agda file is a
[module](https://agda.readthedocs.io/en/latest/language/module-system.html).
These lecture notes are a set of Agda files, which are converted to
html by Agda after it successfully checks the mathematical
development for correctness.
[<sub>Table of contents ⇑</sub>](HoTT-UF-Agda.html#contents)
### <a id="universes"></a> Universes
A universe `𝓤` is a type of types.
* One use of universes is to define families of types indexed by a
type `X` as functions `X → 𝓤`.
* Such a function is [sometimes](HoTT-UF-Agda.html#twinprime) seen as a property of elements of `X`.
* Another use of universes, as we shall see, is to define types of
mathematical structures, such as
[monoids](HoTT-UF-Agda.html#magmasandmonoids), groups, topological
spaces, categories etc.
Sometimes we need more than one universe. For example, the type of
groups in a universe lives in a bigger universe, and given a category
in one universe, its presheaf category also lives in a larger universe.
We will work with a tower of type universes
> `𝓤₀, 𝓤₁, 𝓤₂, 𝓤₃, ...`
These are actually universe names (also called levels, not to be confused with [hlevels](HoTT-UF-Agda.html#hlevel)). We reference
the universes themselves by a deliberately almost-invisible
superscript dot. For example, we will have
> `𝟙 : 𝓤₀ ̇`
where `𝟙` is the one-point type to be defined shortly. We will sometimes
omit this superscript in our discussions, but are forced to write it
in Agda code. We have that the universe `𝓤₀` is a type in the universe
`𝓤₁`, which is a type in the universe 𝓤₂ and so on.
> `𝓤₀ ̇` `: 𝓤₁ ̇`
> `𝓤₁ ̇` `: 𝓤₂ ̇`
> `𝓤₂ ̇` `: 𝓤₃ ̇`
> ` ⋮ `
The assumption that `𝓤₀ : 𝓤₀` or that any universe is in itself or a
smaller universe [gives rise to a
contradiction](https://link.springer.com/article/10.1007/BF01995104),
similar to [Russell's
Paradox](https://plato.stanford.edu/entries/russell-paradox/).
Given a universe `𝓤`, we denote by
> `𝓤 ⁺`
its successor universe. For example, if `𝓤` is `𝓤₀` then `𝓤 ⁺` is
`𝓤₁`. The least upper bound of two universes `𝓤` and `𝓥` is written
> `𝓤 ⊔ 𝓥`.
For example, if `𝓤` is `𝓤₀` and `𝓥` is `𝓤₁`, then `𝓤 ⊔ 𝓥` is `𝓤₁`.
We now bring our notation for universes by importing our Agda file
[`Universes`](Universes.html). The Agda keyword
[`open`](https://agda.readthedocs.io/en/latest/language/module-system.html)
asks to make all definitions in the file `Universe` visible in our
file here. The Agda code in these notes has syntax highlighting and
links, so that we can navigate to the definition of a name or symbol by clicking at it.
\begin{code}
open import Universes public
\end{code}
The keyword `public` makes the contents of the file `Universes`
available to importers of our module `HoTT-UF-Agda`.
We will refer to universes by letters `𝓤,𝓥,𝓦,𝓣`:
\begin{code}
variable
𝓤 𝓥 𝓦 𝓣 : Universe
\end{code}
In some type theories, the universes are cumulative "on the nose", in
the sense that from `X : 𝓤` we derive that `X : 𝓤 ⊔ 𝓥`. We will
[instead](HoTT-UF-Agda.html#universelifting) have an embedding `𝓤 → 𝓤 ⊔
𝓥` of universes into larger universes.
[<sub>Table of contents ⇑</sub>](HoTT-UF-Agda.html#contents)
### <a id="onepointtype"></a> The one-element type `𝟙`
We place it in the first universe, and we name its unique element
"`⋆`". We use the `data` declaration in Agda to introduce it:
\begin{code}
data 𝟙 : 𝓤₀ ̇ where
⋆ : 𝟙
\end{code}
It is important that the point `⋆` lives in the type `𝟙` and in no other
type. There isn't dual citizenship in our type theory. When we create
a type, we also create freshly new elements for it, in this case
"`⋆`". (However, Agda has a limited form of overloading, which allows
us to sometimes use the same name for different things.)
Next we want to give a mechanism to prove that all points of the
type `𝟙` satisfy a given property `A`.
* The property is a function `A : 𝟙 → 𝓤` for some universe `𝓤`.
* The type `A(x)`, which we will write simply `A x`, doesn't need to
be a [truth value](HoTT-UF-Agda.html#subsingletonsandsets). It can be
any type. We will meet examples shortly.
* Mathematical statements are types, such as
> `Π (A : 𝟙 → 𝓤), A ⋆ → Π (x : 𝟙), A x`.
* We read this in natural language as "for any given property `A` of
elements of the type `𝟙`, if `A ⋆` holds, then it follows that `A
x` holds for all `x : 𝟙`".
* In Agda the above `Π` type is written as
> `(A : 𝟙 → 𝓤 ̇ ) → A ⋆ → (x : 𝟙) → A x`.
This is the type of functions with three arguments `A : 𝟙 → 𝓤 ̇`
and `a : A ⋆` and `x : 𝟙`, with values in the type `A x`.
* A proof of a mathematical statement rendered as a type is a
construction of an element of the type. In our example, we have
to construct a function, which we will name `𝟙-induction`.
We do this as follows in Agda, where we first declare the type of the
function `𝟙-induction` with "`:`" and then define the function by an
equation:
\begin{code}
𝟙-induction : (A : 𝟙 → 𝓤 ̇ )
→ A ⋆ → (x : 𝟙) → A x
𝟙-induction A a ⋆ = a
\end{code}
Notice that we supply `A` and `a` as arbitrary arguments, but instead of
an arbitrary `x : 𝟙` we have written "`⋆`". Agda accepts this because it
knows from the definition of `𝟙` that "`⋆`" is the only element of the
type `𝟙`. This mechanism is called *pattern matching*.
A particular case of `𝟙-induction` occurs when the family `A` is constant
with value `B`, which can be written variously as `A = λ (x : 𝟙) → B`,
or `A = λ x → B` if we want Agda to figure out the type of `x` by itself,
or `A = λ _ → B` if we don't want to name the argument of `A` because it
is not used. In usual mathematical practice, such a [lambda expression](https://plato.stanford.edu/entries/lambda-calculus/) is [often
written](https://en.wikipedia.org/wiki/Function_(mathematics)#Arrow_notation) `x ↦ B` (`x` is mapped to `B`) and so `A = (x ↦ B)`.
Given a type `B` and a point `b : B`, we construct the function `𝟙 → B`
that maps any given `x : 𝟙` to `b`.
\begin{code}
𝟙-recursion : (B : 𝓤 ̇ ) → B → (𝟙 → B)
𝟙-recursion B b x = 𝟙-induction (λ _ → B) b x
\end{code}
Not all types have to be seen as mathematical statements (for example
the type `ℕ` of natural numbers defined below). But the above definition
has a dual interpretation as a mathematical function, and as the
statement "`B` implies (*true* implies `B`)" where `𝟙` is the type encoding
the truth value *true*.
The unique function to `𝟙` will be named `!𝟙`. We define two versions
to illustrate [implicit
arguments](https://agda.readthedocs.io/en/latest/language/implicit-arguments.html),
which correspond in mathematics to "subscripts that are omitted when
the reader can safely infer them", as for example for the identity
function of a set or the identity arrow of an object of a category.
\begin{code}
!𝟙' : (X : 𝓤 ̇ ) → X → 𝟙
!𝟙' X x = ⋆
!𝟙 : {X : 𝓤 ̇ } → X → 𝟙
!𝟙 x = ⋆
\end{code}
This means that when we write `!𝟙 x` we have to recover the (uniquely
determined) missing type `X` with `x : X` "from the context". When
Agda can't figure it out, we need to supply it and write `!𝟙 {𝓤} {X}
x`. This is because `𝓤` is also an implicit argument (all things
declared with the Agda keyword *variable* [as above](https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/index.html#universes) are implicit
arguments). There are
[other](https://agda.readthedocs.io/en/latest/language/implicit-arguments.html),
non-positional, ways to indicate `X` without having to indicate `𝓤`
too. Occasionally, people define variants of a function with different
choices of "implicitness", as above.
[<sub>Table of contents ⇑</sub>](HoTT-UF-Agda.html#contents)
### <a id="emptytype"></a> The empty type `𝟘`
It is defined like `𝟙`, except that no elements are listed for it:
\begin{code}
data 𝟘 : 𝓤₀ ̇ where
\end{code}
That's the complete definition. This has a dual interpretation,
mathematically as the empty set (we can actually prove that this type
is a set, once we know the definition of set), and logically as the
truth value *false*. To prove that a property of elements of the empty
type holds for all elements of the empty type, we have to do nothing.
\begin{code}
𝟘-induction : (A : 𝟘 → 𝓤 ̇ )
→ (x : 𝟘) → A x
𝟘-induction A ()
\end{code}
When we write the pattern `()`, Agda checks if there is any case we
missed. If there is none, our definition is accepted. The expression
`()` corresponds to the mathematical phrase [vacuously
true](https://en.wikipedia.org/wiki/Vacuous_truth). The unique
function from `𝟘` to any type is a particular case of `𝟘-induction`.
\begin{code}
𝟘-recursion : (A : 𝓤 ̇ ) → 𝟘 → A
𝟘-recursion A a = 𝟘-induction (λ _ → A) a
\end{code}
We will use the following categorical notation for `𝟘-recursion`:
\begin{code}
!𝟘 : (A : 𝓤 ̇ ) → 𝟘 → A
!𝟘 = 𝟘-recursion
\end{code}
We give the two names `is-empty` and `¬` to the same function now:
\begin{code}
is-empty : 𝓤 ̇ → 𝓤 ̇
is-empty X = X → 𝟘
¬ : 𝓤 ̇ → 𝓤 ̇
¬ X = X → 𝟘
\end{code}
This says that a type is empty precisely when we have a function to
the empty type. Assuming [univalence](HoTT-UF-Agda.html#univalence),
once we have defined the identity type former
[`_≡_`](HoTT-UF-Agda.html#identitytype), we will be able to prove that
`(is-empty X) ≡ (X ≃ 𝟘)`, where `X ≃ 𝟘` is the type of bijections, or
[equivalences](HoTT-UF-Agda.html#fibersandequivalences), from `X` to
`𝟘`. We will also be able to prove things like `(2 + 2 ≡ 5) ≡ 𝟘` and
`(2 + 2 ≡ 4) ≡ 𝟙`.
This is for *numbers*. If we define *types* `𝟚 = 𝟙 + 𝟙` and `𝟜 = 𝟚 +
𝟚` with two and four elements respectively, where we are anticipating
the definition of [`_+_`](HoTT-UF-Agda.html#binarysum) for types, then we
will instead have that `𝟚 + 𝟚 ≡ 𝟜` is a type with `4!` elements, which
is [number of permutations](https://en.wikipedia.org/wiki/Factorial)
of a set with four elements, rather than a truth value `𝟘` or `𝟙`, as
a consequence of the univalence axiom. That is, we will have `(𝟚 + 𝟚 ≡
𝟜) ≃ (𝟜 + 𝟜 + 𝟜 + 𝟜 + 𝟜 + 𝟜)`, so that the type identity `𝟚 + 𝟚 ≡ 𝟜`
holds in [many more ways](https://arxiv.org/abs/math/9802029) than the
numerical equation `2 + 2 ≡ 4`.
The above is possible only because universes are genuine types and
hence their elements (that is, types) have identity types themselves,
so that writing `X ≡ Y` for types `X` and `Y` (inhabiting the same
universe) is allowed.
When we view `𝟘` as *false*, we can read the definition of
the *negation* `¬ X` as saying that "`X` implies *false*". With univalence
we will be able to show that "(*false* → *false*) `≡` *true*", which amounts
to `(𝟘 → 𝟘) ≡ 𝟙`, which in turn says that there is precisely one function
`𝟘 → 𝟘`, namely the (vacuous) identity function.
[<sub>Table of contents ⇑</sub>](HoTT-UF-Agda.html#contents)
### <a id="naturalnumbers"></a> The type `ℕ` of natural numbers
The definition is similar but not quite the same as the one via
[Peano Axioms](https://en.wikipedia.org/wiki/Peano_axioms).
We stipulate an element `zero : ℕ` and a successor function `succ : ℕ → ℕ`,
and then define induction. Once we have defined the identity type former `_≡_`, we
will [*prove*](HoTT-UF-Agda.html#naturalsset) the other peano axioms.
\begin{code}
data ℕ : 𝓤₀ ̇ where
zero : ℕ
succ : ℕ → ℕ
\end{code}
In general, declarations with `data` are inductive definitions. To write the number `5`, we have to write
> `succ (succ (succ (succ (succ zero))))`
We can use the following Agda
[*built-in*](https://agda.readthedocs.io/en/latest/language/built-ins.html)
to be able to just write `5` as a shorthand:
\begin{code}
{-# BUILTIN NATURAL ℕ #-}
\end{code}
Apart from this notational effect, the above declaration doesn't play any
role in the Agda development of these lectures notes.
In the following, the type family `A` can be seen as playing the role
of a property of elements of `ℕ`, except that it doesn't need to be
necessarily
[subsingleton](HoTT-UF-Agda.html#subsingletonsandsets) valued. When it
is, the *type* of the function gives the familiar [principle of
mathematical
induction](https://en.wikipedia.org/wiki/Mathematical_induction) for
natural numbers, whereas, in general, its definition says how to
compute with induction.
\begin{code}
ℕ-induction : (A : ℕ → 𝓤 ̇ )
→ A 0
→ ((n : ℕ) → A n → A (succ n))
→ (n : ℕ) → A n
ℕ-induction A a₀ f = h
where
h : (n : ℕ) → A n
h 0 = a₀
h (succ n) = f n (h n)
\end{code}
The definition of `ℕ-induction` is itself by induction. It says that given a point `a₀ : A 0` and a function `f : (n : ℕ) → A n → A (succ n)`, in order to calculate an element of `A n` for a given `n : ℕ`, we just calculate `h n`, that is,
> `f n (f (n-1) (f (n-2) (... (f 0 a₀)...)))`.
So the principle of induction is a construction that given a *base
case* `a₀ : A 0`, an *induction step* `f : (n : ℕ) → A n → A (succ n)` and a number `n`, says how to get
an element of the type `A n` by [primitive
recursion](https://www.encyclopediaofmath.org/index.php/Primitive_recursion).
Notice also that `ℕ-induction` is the dependently typed version of
primitive recursion, where the non-dependently typed version is
\begin{code}
ℕ-recursion : (X : 𝓤 ̇ )
→ X
→ (ℕ → X → X)
→ ℕ → X
ℕ-recursion X = ℕ-induction (λ _ → X)
\end{code}
The following special case occurs often (and is related to the fact that `ℕ` is the [initial algebra](https://en.wikipedia.org/wiki/Initial_algebra) of the functor `𝟙 + (-)`):
\begin{code}
ℕ-iteration : (X : 𝓤 ̇ )
→ X
→ (X → X)
→ ℕ → X
ℕ-iteration X x f = ℕ-recursion X x (λ _ x → f x)
\end{code}
Agda checks that any recursive definition as above is well founded,
with recursive invocations with structurally smaller arguments
only. If it isn't, the definition is not accepted.
In official Martin-Löf type theories, we have to use the `ℕ-induction`
functional to define everything else with the natural numbers. But Agda
allows us to define functions by structural recursion, like we defined
`ℕ-induction`.
We now define addition and multiplication for the sake of illustration.
We first do it in Peano style. We will create a local [`module`](https://agda.readthedocs.io/en/latest/language/module-system.html#) so that the
definitions are not globally visible, as we want to have the symbols
`+` and `×` free for type operations of MLTT to be defined soon. The
things in the module are indented and are visible outside the module
only if we [`open`](https://agda.readthedocs.io/en/latest/language/module-system.html#) the module or if we write them as
e.g. `Arithmetic._+_` in the following example.
\begin{code}
module Arithmetic where
_+_ _×_ : ℕ → ℕ → ℕ
x + 0 = x
x + succ y = succ (x + y)
x × 0 = 0
x × succ y = x + x × y
infixl 10 _+_
infixl 11 _×_
\end{code}
The above "fixity" declarations allow us to indicate the precedences
(multiplication has higher precedence than addition) and their
associativity (here we take left-associativity as the convention, so that
e.g. `x+y+z` parses as `(x+y)+z`).
Equivalent definitions use `ℕ-induction` on the second argument `y`, via
`ℕ-iteration`:
\begin{code}
module Arithmetic' where
_+_ _×_ : ℕ → ℕ → ℕ
x + y = h y
where
h : ℕ → ℕ
h = ℕ-iteration ℕ x succ
x × y = h y
where
h : ℕ → ℕ
h = ℕ-iteration ℕ 0 (x +_)
infixl 0 _+_
infixl 1 _×_
\end{code}
Here the expression "`x +_`" stands for the function `ℕ → ℕ` that adds
`x` to its argument. So to multiply `x` by `y`, we apply `y` times the
function "`x +_`" to `0`.
As another example, we define the less-than-or-equal relation by
nested induction, on the first argument and then the second, but we
use pattern
matching for the sake of readability.
*Exercise.* [Write it]((HoTT-UF-Agda.html#someexercisessol) using
`ℕ-induction`, recursion or iteration, as appropriate.
\begin{code}
module ℕ-order where
_≤_ _≥_ : ℕ → ℕ → 𝓤₀ ̇
0 ≤ y = 𝟙
succ x ≤ 0 = 𝟘
succ x ≤ succ y = x ≤ y
x ≥ y = y ≤ x
\end{code}
*Exercise.* After learning [`Σ`](HoTT-UF-Agda.html#sigmatypes)
and [`_≡_`](HoTT-UF-Agda.html#identitytype) explained below, prove [that](HoTT-UF-Agda.html#BasicArithmetic))
> `x ≤ y` if and only if `Σ \(z : ℕ) → x + z ≡ y`.
Later, after learning
[univalence](HoTT-UF-Agda.html#univalence) prove that in this case
[this implies](HoTT-UF-Agda.html#additionalexercisessol)
> `(x ≤ y) ≡ Σ \(z : ℕ) → x + z ≡ y`.
That [bi-implication can be turned into
equality](HoTT-UF-Agda.html#univalence-gives-propext) only holds for
types that are subsingletons (and this is called [propositional extensionality](HoTT-UF-Agda.html#propext)).
If we are doing applied mathematics and want to actually compute, we
can define a type for binary notation for the sake of efficiency, and
of course people have done [that](https://www.cs.bham.ac.uk/~mhe/agda-new/BinaryNaturals.html).
Here we are not concerned with
efficiency but only with understanding how to codify mathematics in
(univalent) type theory and in Agda.
[<sub>Table of contents ⇑</sub>](HoTT-UF-Agda.html#contents)
### <a id="binarysum"></a> The binary sum type constructor `_+_`
We now define the [disjoint](HoTT-UF-Agda.html#inl-inr-disjoint-images) sum of two types `X` and `Y`. The elements of
the type
> `X + Y`
are stipulated to be of the forms
> `inl x` and `inr y`
with `x : X` and `y : Y`. If `X : 𝓤` and `Y : 𝓥`, we stipulate that
`X + Y : 𝓤 ⊔ 𝓥 `, where
> `𝓤 ⊔ 𝓥 `
is the [least upper bound](HoTT-UF-Agda.html#universes) of the two universes `𝓤` and
`𝓥`. In Agda we can define this as follows.
\begin{code}
data _+_ {𝓤 𝓥} (X : 𝓤 ̇ ) (Y : 𝓥 ̇ ) : 𝓤 ⊔ 𝓥 ̇ where
inl : X → X + Y
inr : Y → X + Y
\end{code}
To prove that a property `A` of the sum holds for all `z : X + Y`, it is enough to
prove that `A(inl x)` holds for all `x : X` and that `A(inr y)` holds for
all `y : Y`. This amounts to definition by cases:
\begin{code}
+-induction : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (A : X + Y → 𝓦 ̇ )
→ ((x : X) → A(inl x))
→ ((y : Y) → A(inr y))
→ (z : X + Y) → A z
+-induction A f g (inl x) = f x
+-induction A f g (inr y) = g y
\end{code}