1 files changed, 37 insertions, 0 deletions
diff --git a/README.md b/README.md
new file mode 100644
index 0000000..82df265
--- /dev/null
+++ b/README.md
@@ -0,0 +1,37 @@
+B: A New Way of Looking at the Agda Standard Library
+====================================================
+
+B (as in ‘Plan B’) is an compatible extension of the [Agda standard library][]
+intended to support general programming with dependent types.  Its goal is to
+eliminate the large numbers of imports common in Agda programs through universal
+use of type classes and pre-imported names.
+
+B fulfils a different role than the [Agda Prelude][].  The Agda Prelude is a
+fully-featured standard library alternative, but it comes at the expense of
+compatibility.  The Prelude is also heavily programming-oriented, disabling the
+termination checker when appropriate.  B, on the other hand, takes a more
+general route: it is much smaller, makes only compatible extensions to the
+standard library, and it avoids turning off the termination checker.
+
+Getting started
+---------------
+
+B is probably not yet ready for general use.  However, if you’d like to try it,
+you should probably use [Agda][] v2.4.2.2 and version 0.9 of the standard
+library.
+
+Copyright and licence
+---------------------
+
+B is copyright © 2015 [Benjamin Barenblat][] and licensed under the
+[Apache License, version 2.0] [Apache License].  Unless required by applicable
+law or agreed to in writing, B is distributed on an _‘as is’ basis, without
+warranties or conditions of any kind_, either express or implied.  See the
+License for the specific language governing permissions and limitations under
+the License.
+
+[Agda]: http://wiki.portal.chalmers.se/agda/
+[Agda Prelude]: https://github.com/UlfNorell/agda-prelude
+[Agda standard library]: http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.StandardLibrary
+[Apache License]: http://www.apache.org/licenses/LICENSE-2.0
+[Benjamin Barenblat]: https://benjamin.barenblat.name/