This project is an attempt of verifying some parts of interpretability logics in Agda. This is part of my Master’s Thesis and it is a work in progress.
To check all Agda files run
agda src/All.agda
You can read more about this library in my master thesis report.