In this part of the wiki, you will find everything you need to get going with writing code in UniMath.
If you are new to UniMath, we recommend to take a look at the tutorials. You can also use them as a cheat sheet to quickly find (the names of) the most important lemmas and definitions for working with a concept.
- Type Formers in UniMath
- Reasoning with paths
- Equivalences between types
- Propositions and Sets: homotopy types
- Category Theory
- Working with transports
In this folder, you will also find guides on a couple of separate topics:
- A cheat sheet for tactics and some tricks for writing proofs;
- Opaqueness of definitions and lemmas;
- Scripts and snippets that may assist when working with UniMath;
- The standard API for a type.
UniMath has a somewhat complicated theoretical foundation. Here are some links to related reading that may help you understand better how any of this works.
- For a short introduction to what univalent foundations is about, see "An introduction to univalent foundations for mathematicians" by Daniel Grayson.
- For a more comprehensive text about homotopy type theory and univalent foundations, see the HoTT book
- You can find a lot of material about category theory on Nlab.