Guides

In this part of the wiki, you will find everything you need to get going with writing code in UniMath.

Tutorials

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.

1. Type Formers in UniMath
2. Reasoning with paths
3. Equivalences between types
4. Propositions and Sets: homotopy types
5. Category Theory
6. Working with transports

Other guides

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.

FAQ

• Help, my proof is slow!

Relevant reading

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.