Agda-2.5.1.2: A dependently typed functional programming language and proof assistant

Note that Inf a b, where Inf is the INFINITY builtin, is translated to of b (assuming that all coinductive builtins are defined).
Note that if haskellType supported universe polymorphism then the special treatment of INFINITY might not be needed.