Merge pull request UniMath#1979 from arnoudvanderleer/documentation-b…

…roken-links

Fix most broken internal links

README.md

@@ -17,7 +17,7 @@ For instance, you can run the files from the [School on Univalent Mathematics](h
 
 ## Further documentation
 
-* For **general** information about UniMath, citing UniMath and the coordinating committee, see the documentation page [about UniMath](./documentation/misc/About-UniMath.md).
+* For **general** information about UniMath, citing UniMath and the coordinating committee, see the documentation page [about UniMath](./documentation/unimath/About-UniMath.md).
 * For **installing** UniMath and other software-related information, see [setup](./documentation/setup/Setup.md).
 * For **contributing** to UniMath, see the documentation about [contributing](documentation/contributing/Contributing.md).
 

documentation/contributing/Contributing.md

@@ -6,15 +6,15 @@ Potential work on the library is tracked in two ways. Firstly, there are the [Gi
 Feel free to take up a project from either the issues or opportunities file, or to add new issues or opportunities you think of.
 
 ## Pull Requests
-The git and GitHub part of the contribution process, including forking, branching, and remote tracking, is documented on the page about [git and GitHub](Git-and-GitHub).
+The git and GitHub part of the contribution process, including forking, branching, and remote tracking, is documented on the page about [git and GitHub](./Git-and-GitHub.md).
 
 Before making a pull request:
 - Check all your modified code compiles.
 - Run the sanity checks with `make sanity-checks`.
-- Make sure that your code adheres to the [Style guide](./Style-guide.md). In particular, to make sure that your code is usable down the road, make sure that your proofs and definitions have the correct [opaqueness](./../misc/On-opaqueness.md).
+- Make sure that your code adheres to the [Style guide](./Style-guide.md). In particular, to make sure that your code is usable down the road, make sure that your proofs and definitions have the correct [opaqueness](./../guides/Opaqueness.md).
 - If you have changed the file structure of the repository, for example by adding a new file, make sure you have followed the instructions below.
 
-In the end, you will need someone from the [coordinating committee](../misc/About-UniMath.md#coordinating-committee) to merge your pull request into the main repository. Note that from then on, your code will be subject to the [copyright and license agreement](../../LICENSE.md).
+In the end, you will need someone from the [coordinating committee](../unimath/About-UniMath.md#coordinating-committee) to merge your pull request into the main repository. Note that from then on, your code will be subject to the [copyright and license agreement](../../LICENSE.md).
 
 ## Foundations
 

documentation/contributing/Git-and-GitHub.md

@@ -88,7 +88,7 @@ git push -u origin YonedaLemma
 Before making a pull request:
 - Check all your modified code compiles
 - Run the sanity checks with `make sanity-checks`
-- Check you have followed the [style guide](Style-Guide.md) and other instructions in [Contributing](Contributing.md) for creating new files/packages.
+- Check you have followed the [style guide](./Style-guide.md) and other instructions in [Contributing](./Contributing.md) for creating new files/packages.
 
 It is fine if there are still issues when you make the pull request. The pull request will be reviewed and you can make changes before the pull request is merged.
 
@@ -105,7 +105,7 @@ Once your pull request has been reviewed and approved, it can be merged. This wi
 
 ### Merging pull requests on the commandline
 
-This subsection is only relevant if you have write access to the repository (i.e. if you are on the [coordinating committee](../misc/About-UniMath.md#coordinating-committee)).
+This subsection is only relevant if you have write access to the repository (i.e. if you are on the [coordinating committee](../unimath/About-UniMath.md#coordinating-committee)).
 
 To merge a pull request on the command line, first make sure that git also fetches pull requests to your computer. Go to [`.git/config`](../../.git/config) and locate the section that corresponds to the main UniMath repository, for example:
 ```

documentation/contributing/Opportunities.md

@@ -37,7 +37,7 @@ Relevant notions in UniMath:
 
 ## Markov Categories
 
-Markov categories [1] give a synthetic way to study probability theory, and in particular, they can be used to give semantics for probabilistic programming languages [2]. For example, the notion of a deterministic morphism can be define internal to arbitrary Markov categories. 
+Markov categories [1] give a synthetic way to study probability theory, and in particular, they can be used to give semantics for probabilistic programming languages [2]. For example, the notion of a deterministic morphism can be define internal to arbitrary Markov categories.
 
 The goal of this project would be:
 ⁃ Define the notion of Markov category (Definition 2.1 in [1], Definition 6.3 in [2]).
@@ -82,4 +82,4 @@ Literature:
 [3]: https://ncatlab.org/nlab/show/dagger+category
 
 Relevant notions in UniMath:
-- `monoidal_cat` (https://github.com/UniMath/UniMath/blob/master/UniMath/CategoryTheory/Monoidal/MonoidalCategories.v)
+- `monoidal_cat` (https://github.com/UniMath/UniMath/blob/master/UniMath/CategoryTheory/Monoidal/MonoidalCategories.v)

documentation/contributing/Style-guide.md

@@ -1,7 +1,7 @@
 * Avoid inductive types
 * Use notation wherever possible (and feasible)
 * Make sure that all variables (from induction and intros) are introduced by name
-* [Make everything opaque that should be opaque](./On-opaqueness)
+* [Make everything opaque that should be opaque](../guides/Opaqueness)
 * Split long definitions into smaller parts. This makes unification faster, allows you to more easily make the right parts opaque and is more readable.
 * Structure your proof with [bullets](https://coq.inria.fr/refman/proofs/writing-proofs/proof-mode.html#bullets). An occasional proof part with curly braces is okay, but preferably use bullets. The first three levels are `-`, `+` and `*`. If you need more levels, start with `--` (or maybe `**`), but at that point you should probably start splitting up your proof.
 * Minimize your imports: When you create a commit or PR in which you have added `Require Import` statements to a file, or (re)moved code, check that all involved import statements are indeed used or useful. For larger changes, [JasonGross has created a tool](https://github.com/JasonGross/coq-tools) which can come in handy. However, always verify the outcome, because some redundant imports are still good to have (see [this discussion](https://github.com/UniMath/UniMath/issues/1664) for more details).

documentation/guides/Tactics-and-tricks.md

@@ -47,7 +47,7 @@ These tactics act on a (sequence of) tactics `t`.
 
 The tactic `now t` will execute `t` and then close the goal if it has become trivial (and else it will fail).
 
-If `t` closes the goal, the tactic `abstract t` will execute `t` and make the proof term produced by `t` opaque (see [On Opaqueness](./On-opaqueness)). This is useful if you are, for example, defining a (not too complicated) functor, which needs two pieces of data, but also two proofs, and you don't want to split it yet into two (or one) proofs with `Defined` and two (or one) proofs with `Qed`.
+If `t` closes the goal, the tactic `abstract t` will execute `t` and make the proof term produced by `t` opaque (see [On Opaqueness](./Opaqueness.md)). This is useful if you are, for example, defining a (not too complicated) functor, which needs two pieces of data, but also two proofs, and you don't want to split it yet into two (or one) proofs with `Defined` and two (or one) proofs with `Qed`.
 
 The tactic `do n t` will try to execute `t` exactly `n` times (and fail if `t` fails before `n` executions are reached).
 
@@ -93,4 +93,4 @@ The commands `Set` and `Unset` influence the behaviour of coq in the rest of the
 Unset Printing Notations.
 Set Printing Coercions.
 Set Printing Implicit.
-```
+```

documentation/guides/faq/Slow-proof.md

@@ -1,5 +1,5 @@
 ## Make things opaque
-One of the first things to check if proofs are becoming slow, or proof terms become large, is whether [the things that should be opaque](./On-opaqueness), are opaque.
+One of the first things to check if proofs are becoming slow, or proof terms become large, is whether [the things that should be opaque](../Opaqueness.md), are opaque.
 However, note that properly managing opaqueness/transparency saves at most one or two minutes per definition. If a definition is very slow, then it is most likely related to unification. Also, make sure to properly split your definitions. By having everything split up in multiple identifiers, unification becomes a bit nicer, because computation gets blocked more.
 
 ## Try to pinpoint the origin of slowness
@@ -29,4 +29,4 @@ If the second step does not work, try having a look at the unfolded goal.
  * Try to find out what the types of the different parts are (and what coercions would be applied then).
  * Try to construct an `exact (maponpaths (λ z, ... z ...) (rewrite_term)).` from this.
 
-As a rule of thumb (not as a law), functions with transport might fail because they don't have enough type information. In that case, you need to provide them some hints, and you can do so, by (partially) filling in the implicit arguments that relate to the type and the type family.
+As a rule of thumb (not as a law), functions with transport might fail because they don't have enough type information. In that case, you need to provide them some hints, and you can do so, by (partially) filling in the implicit arguments that relate to the type and the type family.

documentation/setup/Build-Dune.md

@@ -22,7 +22,7 @@ If you have previously compiled UniMath using `make` you need to clean up your
 repository or else dune will complain about files that it does not know how to
 compile. Running `make clean` should be enough.
 
-Assuming coq is installed (otherwise see for example [INSTALL.md](INSTALL.md))
+Assuming coq is installed (otherwise see for example [Install.md](./Install.md))
 and in your `PATH` you should now be able to build UniMath with the command
 `dune build`. **Note** that dune by default does not have caching enabled. To
 enable this once give the flag `--cache=enabled` to dune:

documentation/setup/Emacs-and-Proof-General.md

@@ -4,7 +4,7 @@ Browsing and editing a file in the UniMath source tree
 
 The UniMath library consists of Coq source files (file ending *.v) in the subdirectory `UniMath/UniMath`.
 
-Once you have [installed](./INSTALL.md) UniMath, you can start browsing and editing the source files.
+Once you have [installed](./Install.md) UniMath, you can start browsing and editing the source files.
 There are several programs to interactively edit and step through the files, among which
 are
 1. [CoqIDE](https://coq.inria.fr/refman/practical-tools/coqide.html) and
@@ -22,14 +22,14 @@ When opening a source file in the directory `UniMath/UniMath` in Emacs, the foll
 1. *The Proof General add-on to Emacs is loaded.*
    Proof General is an add-on to the text editor Emacs, adding buttons, menus, and keyboard shortcuts
    to interact with Coq, the proof assistant that UniMath relies on.
-   During the [installation procedure](./INSTALL.md) you have set up Proof General on your computer.
+   During the [installation procedure](./Install.md) you have set up Proof General on your computer.
 2. *A Unicode input method is loaded.*
    It allows you to insert Unicode symbols using a LaTeX-like syntax.
-   See [Section on Unicode input below](USAGE.md/#unicode-input)
+   See [the page on Unicode input below](../unimath/Symbols-list.md).
 3. Proof General is informed about the location of the Coq proof assistant installed during the installation of UniMath,
    and of the options that need to be passed to Coq.
 
-Items 2 and 3 are achieved through the Emacs configuration file [`.dir-locals.el`](./UniMath/.dir-locals.el) located in
+Items 2 and 3 are achieved through the Emacs configuration file [`.dir-locals.el`](../../UniMath/.dir-locals.el) located in
 the subdirectory `UniMath/UniMath`.
 For this reason, we recommend you save your UniMath files in this subdirectory as well.
 

documentation/setup/Install-CoqIDE.md

@@ -23,4 +23,4 @@ order to run the program `coqide`, you may use the following command.
 ```bash
 $ sub/coq/bin/coqide <flags>
 ```
-where `<flags>` are the options passed to Coq as per the [Emacs configuration file](./UniMath/.dir-locals.el), which is made from the file [`UniMath/.dir-locals.el.in`](./UniMath/.dir-locals.el) as a result of running `make`..
+where `<flags>` are the options passed to Coq as per the [Emacs configuration file](../../UniMath/.dir-locals.el), which is made from the file [`UniMath/.dir-locals.el.in`](../../UniMath/.dir-locals.el.in) as a result of running `make`..

documentation/setup/Install-opam.md

@@ -2,7 +2,7 @@
 
 This method for installing OCaml (in order to also build Coq) allows more
 flexibility, but is more involved than the method in
-[INSTALL.md](./INSTALL.md), because it depends on "opam".
+[Install.md](./Install.md), because it depends on "opam".
 
 First install opam and needed prerequisites:
 

documentation/setup/Install.md

@@ -27,13 +27,13 @@ brew install coq
 
 Alternatively, you can install Coq in any other standard way; or you can ask UniMath to build its own copy of Coq, which may be useful if your globally installed Coq is a version incompatible with UniMath.  If you plan to do this, then you must first install its dependencies, e.g. with the Homebrew command:
 ```bash
-brew install bash objective-caml ocaml-num ocaml-findlib camlp5 
+brew install bash objective-caml ocaml-num ocaml-findlib camlp5
 ```
-or, for more customisability, using the "opam" OCaml package manager, according to the detailed instructions in [`INSTALL_OPAM.md`](./INSTALL_OPAM.md).
+or, for more customisability, using the "opam" OCaml package manager, according to the detailed instructions in [`Install-opam.md`](./Install-opam.md).
 
 Emacs may be installed using https://emacsformacosx.com/, http://aquamacs.org, or any other flavour of Emacs you prefer.
 
-Now you may proceed to the instructions for [Installation of Proof General](#installation-of-proofgeneral-all-operating-systems) and [Installing UniMath](#installing-unimath) below.
+Now you may proceed to the instructions for [Installation of Proof General](#installation-of-proof-general-all-operating-systems) and [Installing UniMath](#installing-unimath) below.
 
 The automated sanity checks (for contributions to UniMath) may require a more recent version of bash than the one preinstalled on Mac OS; this can be installed with `brew install bash`.
 
@@ -51,7 +51,7 @@ following shell command.
 ```bash
  sudo apt-get install build-essential git ocaml ocaml-nox ocaml-native-compilers camlp5 libgtk2.0 libgtksourceview2.0 liblablgtk-extras-ocaml-dev ocaml-findlib libnum-ocaml-dev emacs
 ```
-Now proceed with [Installation of Proof General](#installation-of-proofgeneral-all-operating-systems) and [Installing UniMath](#installing-unimath) below.
+Now proceed with [Installation of Proof General](#installation-of-proof-general-all-operating-systems) and [Installing UniMath](#installing-unimath) below.
 
 ### Preparing for the installation under Arch Linux or Manjaro Linux
 
@@ -64,7 +64,7 @@ shell commands.
  sudo pacman --sync --needed ocaml camlp5 ocaml-findlib ocaml-num
  sudo pacman -S emacs
 ```
-Now proceed with [Installation of Proof General](#installation-of-proofgeneral-all-operating-systems) and [Installing UniMath](#installing-unimath) below.
+Now proceed with [Installation of Proof General](#installation-of-proof-general-all-operating-systems) and [Installing UniMath](#installing-unimath) below.
 
 ## Installation of Proof General (all operating systems)
 
@@ -106,7 +106,7 @@ shell command (in this directory).
 make
 ```
 
-Once this is done, you can start [browsing and editing UniMath](./USAGE.md).
+Once this is done, you can start [browsing and editing UniMath](../guides/Guides.md).
 Below, we explain how to compile individual packages of UniMath, and how to
 create HTML documentation.
 
@@ -147,7 +147,7 @@ create HTML documentation.
    ```
    The path to that directory from here, by default, is ./sub/coq/user-contrib/.
 
-- To install [CoqIDE](https://coq.inria.fr/refman/practical-tools/coqide.html), see [INSTALL\_COQIDE](./INSTALL_COQIDE.md).
+- To install [CoqIDE](https://coq.inria.fr/refman/practical-tools/coqide.html), see [Install-CoqIDE](./Install-CoqIDE.md).
 
 ## TAGS files
 
@@ -273,7 +273,7 @@ between the version of OCaml used and the version of Coq being compiled.
 File "lib/pp_control.ml", line 61, characters 22-33:
 Error: This expression has type bytes -> int -> int -> unit
        but an expression was expected of type string -> int -> int -> unit
-       Type bytes is not compatible with type string 
+       Type bytes is not compatible with type string
 ```
 
 For example, Coq 8.6.1 cannot be compiled by OCaml 4.06.0, and must instead be
@@ -282,7 +282,7 @@ compiled by an older version.  In the instructions above, we arrange for OCaml
 
 ### Problems caused by ill-formed input to make
 
-When calling `make`, various files are read, some of them not under version control by git. 
+When calling `make`, various files are read, some of them not under version control by git.
 If those files are ill-formed, `make` stops working; in particular, `make` cannot be used to delete and recreate those files.
 When such a situation arises, one solution is to try cleaning everything with this command:
 ```bash
@@ -330,7 +330,7 @@ This package is not among the build dependencies for older versions of Coq.
 
 - Before submitting a pull request, developers should run the sanity checks that are specified
   in the Makefile by adding `sanity-checks` to the "make" command line.
-  
+
 - One of the sanity checks checks that all proof files in the directory tree
   are listed in the corresponding package, but it will complain even about
   files you haven't checked in; to disable the test, add `-o
@@ -346,4 +346,4 @@ This package is not among the build dependencies for older versions of Coq.
   `LIMIT_MEMORY=yes` to the `make` command line.  Unfortunately, under Mac OS
   X, such memory limits are ineffective, so you may prefer to run the test
   under Linux.
-  
+