GitLab Commit is coming up on August 3-4. Learn how to innovate together using GitLab, the DevOps platform. Register for free: gitlabcommitvirtual2021.com

Commit cbaccdb2 authored by Paolo Capriotti's avatar Paolo Capriotti
Browse files

Fix typo in README

parent 3d1a9dde
......@@ -21,7 +21,7 @@ agda -i . README.agda
Note that the [`agda-base`](http://github.com/pcapriotti/agda-base) library is required. See [this page](http://agda.readthedocs.io/en/latest/tools/package-system.html) for instructions on how to install Agda libraries.
A note that the postulates contained in `agda-base`: besides the *univalence* axiom, core to HoTT, the only postulates are those related to inductive and coinductive types, such as homotopy-terminality of M-types and induction principles for higher inductive types. Those do not affect the present development, since it does not make use of (co)inductive types at all.
A note about the postulates contained in `agda-base`: besides the *univalence* axiom, core to HoTT, the only postulates are those related to inductive and coinductive types, such as homotopy-terminality of M-types and induction principles for higher inductive types. Those do not affect the present development, since it does not make use of (co)inductive types at all.
### Structure of the formalisation
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment