chore(*.md): fix/remove broken links

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
+* [priority](priority.hlean) : priority for algebraic operations
-* [relation](relation.lean)
+* [relation](relation.hlean)
-* [binary](binary.lean) : binary operations
+* [binary](binary.hlean) : binary operations
-* [order](order.lean)
+* [order](order.hlean)
-* [lattice](lattice.lean)
+* [lattice](lattice.hlean)
-* [group](group.lean)
+* [group](group.hlean)
-* [ring](ring.lean)
+* [ring](ring.hlean)
-* [ordered_group](ordered_group.lean)
+* [ordered_group](ordered_group.hlean)
-* [ordered_ring](ordered_ring.lean)
+* [ordered_ring](ordered_ring.hlean)
-* [field](field.lean)
+* [field](field.hlean)
-* [ordered_field](ordered_field.lean)
+* [ordered_field](ordered_field.hlean)
-* [bundled](bundled.lean) : bundled versions of the algebraic structures
+* [bundled](bundled.hlean) : bundled versions of the algebraic structures
 
 Files which are HoTT specific:
 

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

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
 

hott/init/init.md

@@ -9,7 +9,6 @@ Syntax declarations:
 
 * [reserved_notation](reserved_notation.hlean)
 * [tactic](tactic.hlean)
-* [priority](priority.hlean)
 
 Datatypes and logic:
 

hott/tools/tools.md

@@ -3,4 +3,4 @@ tools
 
 Various additional tools.
 
-* [helper_tactics](helper_tactics.lean) : useful tactics
+* [helper_tactics](helper_tactics.hlean) : useful tactics

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
+* [hott](hott.hlean) : facts about the integers specific to the HoTT library

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
+* [sub](sub.hlean) : subtraction, and distance

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:
 

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)

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)

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)

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.

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

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)

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)
+* [examples](examples/examples.md)