Recovering the guidelines for direct clones (UniMath#694)

HOWTO-INSTALL.md

@@ -10,9 +10,17 @@ environment for making contributions to the library.
 
 ## Getting a copy of the library
 
+The way you install the library on your machine might depend on the way you plan
+to use it. If you plan to contribute to the library, then we suggest first
+creating a fork of the library, and then cloning your fork. If you don't intend
+to contribute the library, then you don't need to create your own fork, and you
+can proceed directly to clone the library.
+
 ### Creating a fork of the library
 
-Begin by creating a fork of the library on GitHub:
+If your plan is to submit a contribution, or to do a project that eventually
+could lead to a contribution to the library, then it is best to begin by
+creating a fork of the library on GitHub:
 
 1. Navigate to the library's GitHub page at
    [https://github.com/UniMath/agda-unimath](https://github.com/UniMath/agda-unimath).
@@ -36,6 +44,19 @@ size.
 If you prefer to clone the library with its history, simply omit `--depth 1` in
 the above command.
 
+### Cloning the library directly
+
+If you don't intend to contribute to the library, but still want to have a local
+copy of it on your machine, you can clone it directly with
+
+```bash
+git clone --depth 1 [email protected]:UniMath/agda-unimath.git
+```
+
+This is not our first recommendation, however, because if you later decide to
+use this clone for contributions, you will need some proficiency in using `git`
+to adjust the remote addresses of your clone.
+
 ### Creating a branch within your clone of the library
 
 Once you've cloned the library, we highly recommend you to preserve the `master`