chore(hott): update md files, move port.md

hott/algebra/algebra.md

@@ -1,7 +1,7 @@
 algebra
 =======
 
-The following files are [ported](port.md) from the standard library. If anything needs to be changed, it is probably a good idea to change it in the standard library and then port the file again (see also [script/port.pl](../../script/port.pl)).
+The following files are [ported](../port.md) from the standard library. If anything needs to be changed, it is probably a good idea to change it in the standard library and then port the file again (see also [script/port.pl](../../script/port.pl)).
 
 * [priority](priority.lean) : priority for algebraic operations
 * [relation](relation.lean)
@@ -16,7 +16,7 @@ The following files are [ported](port.md) from the standard library. If anything
 * [ordered_field](ordered_field.lean)
 * [bundled](bundled.lean) : bundled versions of the algebraic structures
 
-Files which are not ported:
+Files which are HoTT specific:
 
 * [hott](hott.hlean) : Basic theorems about the algebraic hierarchy specific to HoTT
 * [trunc_group](trunc_group.hlean) : truncate an infinity-group to a group

hott/book.md

@@ -17,7 +17,7 @@ The rows indicate the chapters, the columns the sections.
 |-------|---|---|---|---|---|---|---|---|---|----|----|----|----|----|----|
 | Ch 1  | . | . | . | . | + | + | + | + | + | .  | +  | +  |    |    |    |
 | Ch 2  | + | + | + | + | . | + | + | + | + | +  | +  | +  | +  | +  | +  |
-| Ch 3  | + | + | + | + | ½ | + | + | - | + | .  | +  |    |    |    |    |
+| Ch 3  | + | + | + | + | ½ | + | + | + | + | .  | +  |    |    |    |    |
 | Ch 4  | - | + | + | + | . | + | ½ | + | + |    |    |    |    |    |    |
 | Ch 5  | - | . | ½ | - | - | . | . | ½ |   |    |    |    |    |    |    |
 | Ch 6  | . | + | + | + | + | ½ | ½ | + | ¾ | ¼  | ¾  | +  | .  |    |    |
@@ -78,7 +78,7 @@ Chapter 3: Sets and logic
 - 3.5 (Subsets and propositional resizing): Lemma 3.5.1 is subtype_eq in [types.sigma](types/sigma.hlean), we don't have propositional resizing as axiom yet.
 - 3.6 (The logic of mere propositions): in the corresponding file in the [types](types/types.md) folder. (is_trunc_prod is defined in [types.sigma](types/sigma.hlean))
 - 3.7 (Propositional truncation): [init.hit](init/hit.hlean) and [hit.trunc](hit/trunc.hlean)
-- 3.8 (The axiom of choice): not formalized
+- 3.8 (The axiom of choice): [choice](choice.hlean)
 - 3.9 (The principle of unique choice): Lemma 9.3.1 in [hit.trunc](hit/trunc.hlean), Lemma 9.3.2 in [types.trunc](types/trunc.hlean)
 - 3.10 (When are propositions truncated?): no formalizable content
 - 3.11 (Contractibility): [init.trunc](init/trunc.hlean) (mostly), [types.pi](types/pi.hlean) (Lemma 3.11.6), [types.trunc](types/trunc.hlean) (Lemma 3.11.7), [types.sigma](types/sigma.hlean) (Lemma 3.11.9)

hott/hott.md

@@ -14,6 +14,7 @@ The following files don't fit in any of the subfolders:
 * [eq2](eq2.hlean): coherence rules for the higher dimensional structure of equality
 * [function](function.hlean): embeddings, (split) surjections, retractions
 * [arity](arity.hlean) : equality theorems about functions with arity 2 or higher
+* [choice](choice.hlean) : theorems about the axiom of choice.
 
 See [book.md](book.md) for an overview of the sections of the [HoTT book](http://homotopytypetheory.org/book/) which have been covered.
 
@@ -28,4 +29,4 @@ Note that there is no proof-irrelevant or impredicative universe.
 
 By default, the univalence axiom is declared on initialization.
 
-See also the [standard library](../library/library.md).
+See also the [standard library](../library/library.md). We [port](port.md) some files from the standard library to the HoTT library.

hott/port.md

@@ -1,4 +1,4 @@
-We port a lot of algebra files from the standard library to the HoTT library.
+We port a lot of algebra and number systems (nat, int, ...) files from the standard library to the HoTT library.
 
 Port instructions:
 - use the script port.pl in scripts/ to port the file. e.g. execute the following in the `scripts` folder: `./port.pl ../library/algebra/lattice.lean ../hott/algebra/lattice.hlean`