[Agda] Numerical Programming in Agda

[david rush]

Hello all - 

I am working on a numerical programming project and it is increasingly looking 
like I am going to need something like Agda's fully dependent types in order 
to correctly express the structure of my code. The trouble is, it looks like 
almost no-one does any numerical programming in it, and I am loath to create 
my own prelude with the usual numeric type hierarchy (building up from Nat to 
Complex Floats). Well, I'd rather not if someone has already done it, anyway 
:) 

Google comes up with very few hits for "numerical programming in agda" and 
other similar searches. Can it really be that I am the first to try doing 
this? Does anyone have a pointer to pre-existing work which might help? 

TIA, 
david rush