A

agda-real

A formalisation of the real numbers in dependent type theory using the Agda programming language.