Structure The two most important directories are: agda — the formalization of the type systems in Agda. tex — the (human-readable) paper. toy contains a toy proof-of-concept implementation of a language with refinement types that compiles to Idris.