Mini-HoTT   Build Status GitHub issues MIT license GitHub tag

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


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

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

Table of Contents


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: