diff --git a/hott/algebra/algebra.md b/hott/algebra/algebra.md index 3c1316e36..03d2a88b9 100644 --- a/hott/algebra/algebra.md +++ b/hott/algebra/algebra.md @@ -3,18 +3,18 @@ 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)). -* [priority](priority.lean) : priority for algebraic operations -* [relation](relation.lean) -* [binary](binary.lean) : binary operations -* [order](order.lean) -* [lattice](lattice.lean) -* [group](group.lean) -* [ring](ring.lean) -* [ordered_group](ordered_group.lean) -* [ordered_ring](ordered_ring.lean) -* [field](field.lean) -* [ordered_field](ordered_field.lean) -* [bundled](bundled.lean) : bundled versions of the algebraic structures +* [priority](priority.hlean) : priority for algebraic operations +* [relation](relation.hlean) +* [binary](binary.hlean) : binary operations +* [order](order.hlean) +* [lattice](lattice.hlean) +* [group](group.hlean) +* [ring](ring.hlean) +* [ordered_group](ordered_group.hlean) +* [ordered_ring](ordered_ring.hlean) +* [field](field.hlean) +* [ordered_field](ordered_field.hlean) +* [bundled](bundled.hlean) : bundled versions of the algebraic structures Files which are HoTT specific: diff --git a/hott/algebra/category/limits/limits.md b/hott/algebra/category/limits/limits.md index 7938b8a73..5c4007651 100644 --- a/hott/algebra/category/limits/limits.md +++ b/hott/algebra/category/limits/limits.md @@ -3,6 +3,5 @@ algebra.category.limits * [limits](limits.hlean) : Limits in a category, defined as terminal object in the cone category * [colimits](colimits.hlean) : Colimits in a category, defined as the limit of the opposite functor -* [complete](complete.hlean) : Categories which are (co)complete or constructions which preserve (co)completeness * [functor_preserve](functor_preserve.hlean) : Functors which preserve limits and colimits * [adjoint](adjoint.hlean) : the (co)limit functor is adjoint to the diagonal map diff --git a/hott/book.md b/hott/book.md index 91f859018..e8131f411 100644 --- a/hott/book.md +++ b/hott/book.md @@ -115,13 +115,13 @@ Chapter 6: Higher inductive types - 6.2 (Induction principles and dependent paths): dependent paths in [init.pathover](init/pathover.hlean), circle in [homotopy.circle](homotopy/circle.hlean) - 6.3 (The interval): [homotopy.interval](homotopy/interval.hlean) - 6.4 (Circles and spheres): [homotopy.sphere](homotopy/sphere.hlean) and [homotopy.circle](homotopy/circle.hlean) -- 6.5 (Suspensions): [homotopy.suspension](homotopy/suspension.hlean) (we define the circle to be the suspension of bool, but Lemma 6.5.1 is similar to proving the ordinary induction principle for the circle in [homotopy.circle](homotopy/circle.hlean)) and a bit in [homotopy.sphere](homotopy/sphere.hlean) and [types.pointed](types/pointed.hlean) +- 6.5 (Suspensions): [homotopy.suspension](homotopy/susp.hlean) (we define the circle to be the suspension of bool, but Lemma 6.5.1 is similar to proving the ordinary induction principle for the circle in [homotopy.circle](homotopy/circle.hlean)) and a bit in [homotopy.sphere](homotopy/sphere.hlean) and [types.pointed](types/pointed.hlean) - 6.6 (Cell complexes): we define the torus using the quotient, see [hit.two_quotient](hit/two_quotient.hlean) and [homotopy.torus](homotopy/torus.hlean) (no dependent eliminator defined yet) - 6.7 (Hubs and spokes): [hit.two_quotient](hit/two_quotient.hlean) and [homotopy.torus](homotopy/torus.hlean) (no dependent eliminator defined yet) - 6.8 (Pushouts): [hit.pushout](hit/pushout.hlean). Some of the "standard homotopy-theoretic constructions" have separate files, although not all of them have been defined explicitly yet - 6.9 (Truncations): [hit.trunc](hit/trunc.hlean) (except Lemma 6.9.3) - 6.10 (Quotients): [hit.set_quotient](hit/set_quotient.hlean) (up to 6.10.3). We define integers differently, to make them compute, in the folder [types.int](types/int/int.md). 6.10.13 is in [types.int.hott](types/int/hott.hlean) -- 6.11 (Algebra): [algebra.group](algebra/group.hlean), [algebra.fundamental_group](algebra/fundamental_group.hlean) (no homotopy groups yet) +- 6.11 (Algebra): [algebra.group](algebra/group.hlean), [algebra.homotopy_group](algebra/homotopy_group.hlean) - 6.12 (The flattening lemma): [hit.quotient](hit/quotient.hlean) (for quotients instead of homotopy coequalizers, but these are practically the same) - 6.13 (The general syntax of higher inductive definitions): no formalizable content diff --git a/hott/init/init.md b/hott/init/init.md index bd2839981..81deec2af 100644 --- a/hott/init/init.md +++ b/hott/init/init.md @@ -9,7 +9,6 @@ Syntax declarations: * [reserved_notation](reserved_notation.hlean) * [tactic](tactic.hlean) -* [priority](priority.hlean) Datatypes and logic: diff --git a/hott/tools/tools.md b/hott/tools/tools.md index bc88f47d1..6a06271ae 100644 --- a/hott/tools/tools.md +++ b/hott/tools/tools.md @@ -3,4 +3,4 @@ tools Various additional tools. -* [helper_tactics](helper_tactics.lean) : useful tactics \ No newline at end of file +* [helper_tactics](helper_tactics.hlean) : useful tactics diff --git a/hott/types/int/int.md b/hott/types/int/int.md index 843cd56e4..5fe34add5 100644 --- a/hott/types/int/int.md +++ b/hott/types/int/int.md @@ -1,7 +1,7 @@ types.int ========= -The integers. Note: most of these files are ported 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 integers. Note: most of these files are ported 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)). * [basic](basic.hlean) : the integers, with basic operations -* [hott](hott.hlean) : facts about the integers specific to the HoTT library \ No newline at end of file +* [hott](hott.hlean) : facts about the integers specific to the HoTT library diff --git a/hott/types/nat/nat.md b/hott/types/nat/nat.md index b7a1f14a8..68d0319ef 100644 --- a/hott/types/nat/nat.md +++ b/hott/types/nat/nat.md @@ -1,8 +1,8 @@ types.nat ========= -The natural numbers. Note: all these files are ported 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 natural numbers. Note: all these files are ported 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)). * [basic](basic.hlean) : the natural numbers, with succ, pred, addition, and multiplication * [order](order.hlean) : less-than, less-then-or-equal, etc. -* [sub](sub.hlean) : subtraction, and distance \ No newline at end of file +* [sub](sub.hlean) : subtraction, and distance diff --git a/library/data/data.md b/library/data/data.md index 215517b45..d847f54ee 100644 --- a/library/data/data.md +++ b/library/data/data.md @@ -25,13 +25,11 @@ Constructors: * [sigma](sigma.lean) : the dependent product * [uprod](uprod.lean) : unordered pairs * [option](option.lean) -* [subtype](subtype.lean) * [squash](squash.lean) : propositional truncation * [list](list/list.md) * [finset](finset/finset.md) : finite sets * [stream](stream.lean) * [set](set/set.md) -* [vector](vector.lean) Types with extra information: diff --git a/library/data/int/int.md b/library/data/int/int.md index 83b470039..701972b58 100644 --- a/library/data/int/int.md +++ b/library/data/int/int.md @@ -8,4 +8,3 @@ The integers. * [div](div.lean) : div and mod * [power](power.lean) * [gcd](gcd.lean) : gcd, lcm, and coprime -* [bigops](bigops.lean) \ No newline at end of file diff --git a/library/data/rat/rat.md b/library/data/rat/rat.md index d3f80867d..18157f983 100644 --- a/library/data/rat/rat.md +++ b/library/data/rat/rat.md @@ -5,4 +5,3 @@ The rational numbers. * [basic](basic.lean) : the rationals as a field * [order](order.lean) : the order relations and the sign function -* [bigops](bigops.lean) \ No newline at end of file diff --git a/library/data/real/real.md b/library/data/real/real.md index 3a19476a7..39f128218 100644 --- a/library/data/real/real.md +++ b/library/data/real/real.md @@ -7,4 +7,3 @@ The real numbers: classically, as a quotient type; constructively, as a setoid. * [order](order.lean) : the reals as an ordered ring (constructive) * [division](division.lean) : the reals as a discrete linear ordered field (classical) * [complete](complete.lean) : the reals are Cauchy complete (classical) -* [bigops](bigops.lean) \ No newline at end of file diff --git a/library/init/init.md b/library/init/init.md index 7fb27f16e..d6be62f0b 100644 --- a/library/init/init.md +++ b/library/init/init.md @@ -9,12 +9,12 @@ Syntax declarations: * [reserved_notation](reserved_notation.lean) * [tactic](tactic.lean) -* [priority](priority.lean) Datatypes and logic: * [datatypes](datatypes.lean) * [logic](logic.lean) +* [classical](classical.lean) * [bool](bool.lean) * [num](num.lean) * [nat](nat.lean) @@ -42,3 +42,8 @@ logic.axioms.hilbert) the two are equivalent. Type class inferences are set up to use "inhabited" however, so users should use that to declare that types have an element. Use "nonempty" in the hypothesis of a theorem when the theorem does not depend on the witness chosen. + +Module init.classical declares a choice axiom, and uses it to +prove the excluded middle, propositional completeness, axiom of +choice, and prove that the decidable class is trivial when the +choice axiom is assumed. diff --git a/library/library.md b/library/library.md index 266675995..47a9d917a 100644 --- a/library/library.md +++ b/library/library.md @@ -7,7 +7,7 @@ The Lean standard library is contained in the following files and directories: * [logic](logic/logic.md) : logical constructs and axioms * [data](data/data.md) : concrete datatypes and type constructors * [algebra](algebra/algebra.md) : algebraic structures -* [theories](theories.md) : more domain-specific theories +* [theories](theories/theories.md) : more domain-specific theories * [tools](tools/tools.md) : additional tools The files in `init` are loaded by default, and hence do not need to be diff --git a/library/logic/examples/examples.md b/library/logic/examples/examples.md index 22d5c532b..8cf5cdde4 100644 --- a/library/logic/examples/examples.md +++ b/library/logic/examples/examples.md @@ -2,4 +2,3 @@ logic.examples ============== * [nuprl_examples](nuprl_examples.lean) : examples from "Logical investigations with the Nuprl Proof Assistant" -* [instances_test](instances_test.lean) diff --git a/library/logic/logic.md b/library/logic/logic.md index 864a4dd6f..f055689be 100644 --- a/library/logic/logic.md +++ b/library/logic/logic.md @@ -11,17 +11,8 @@ The command `import logic` does not import any axioms by default. * [cast](cast.lean) : casts and heterogeneous equality * [quantifiers](quantifiers.lean) : existential and universal quantifiers * [identities](identities.lean) : some useful identities -* [instances](instances.lean) : class instances for eq and iff -* [subsingleton](subsingleton.lean) * [default](default.lean) -The file `choice.lean` declares a choice axiom, and uses it to -prove the excluded middle, propositional completeness, axiom of -choice, and prove that the decidable class is trivial when the -choice axiom is assumed. - -* [choice](choice.lean) - Subfolders: -* [examples](examples/examples.md) \ No newline at end of file +* [examples](examples/examples.md)