Artem Gureev

This page contains brief guides to two interactive theorem provers supporting HoTT: Coq and Agda for people with a background in Type Theory.

For those that are only starting their journey in Type Theory and its applications, it is recommended to consult Coq and Agda's wonderful Foundation texts. However, it is a bit tedious to go through them for people who already have a grasp on Type Theory and simply want a demonstration and an adequate cheatsheet of the language's syntactical needs to start working with the theorem provers right away. These two small documents are meant for people in similar situations.

Note that this is supposed to serve as an extremely short introduction into the main functionality of Agda and Coq, what that means is that some (if not all) of the material and actions that will be presented may be extremely inefficient or generally have better ways of execution. Hence one is encouraged to use the documents for a smooth start and then move on to the Foundation texts in order to encounter some proper treatment of selected topics and actions.

I am thankful to Ilia Vlasov for helping me in starting out using both systems and whose advice in mastering them I am trying to translate in written format through these tutorials. Hopefully other people lacking a practical guide can begin their journey without barriers that I have faced before help arrived.