An Agda library containing a simple foundation for works in intensional type theory