An Agda library containing a simple foundation for works in intensional type theory
there don't seem to be any issues for this project.