This repository contains my (rather brief) introduction to the programming language/proof assistant Coq. I completed the tutorial Coq in a Hurry by Yves Bartot in preparation for my attendance at the School of Univalent Mathematics in July 2024.
Much as Coq itself, this repository is licensed under the GNU LGPL.