From 3409deecdbf36c6d3c69648f2bcd11638c3f1928 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Thu, 21 Jan 2016 15:31:41 -0500 Subject: [PATCH] chore(hott): update md files, move port.md --- hott/algebra/algebra.md | 4 ++-- hott/book.md | 4 ++-- hott/hott.md | 3 ++- hott/{algebra => }/port.md | 2 +- 4 files changed, 7 insertions(+), 6 deletions(-) rename hott/{algebra => }/port.md (91%) diff --git a/hott/algebra/algebra.md b/hott/algebra/algebra.md index 28741baf9c..3c1316e36e 100644 --- a/hott/algebra/algebra.md +++ b/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 diff --git a/hott/book.md b/hott/book.md index 6c8397d9c0..c46d715dab 100644 --- a/hott/book.md +++ b/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) diff --git a/hott/hott.md b/hott/hott.md index 2045f00c3f..11c9a42298 100644 --- a/hott/hott.md +++ b/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. diff --git a/hott/algebra/port.md b/hott/port.md similarity index 91% rename from hott/algebra/port.md rename to hott/port.md index d4c1a157db..660941f367 100644 --- a/hott/algebra/port.md +++ b/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`