# Mini-HoTT   ¶

Mini-HoTT is a basic Agda library which contains basic definitions and results in Univalent type theory. There is no guarantee whatsoever of any kind. At the moment, this library suffers of many changes without any warning.

## Quick start¶

### Installation¶

The only prerequisite is to have installed the latest version of Agda and a text editor with Agda support, e.g., Emacs or Atom. Then, you can install the library as usual after cloning the sources by running the following command.

$git clone http://github.com/jonaprieto/mini-hott  For newcomers, the easiest way to install a library is using agda-pkg You can run the following commands to install it: $ pip3 install agda-pkg
$apkg init$ apkg install --github jonaprieto/mini-hott


After installing the sources, just include in your code at the top the following line:

open import MiniHoTT


## Contributors¶

Collaborations are always welcomed. At the moment, me, Jonathan Prieto-Cubides, I’m using the library to type-check my proofs for my research project at the University of Bergen.

People involved in making this library better, although not directly involved are: