[Agda] Formalization of Linear Algebra in agda

[Guillermo Calderon]

Dear all,

I am looking for a formalization  in Agda
of vectorial spaces (over a field).
My concern is to work in the formalization of some concepts involved 
with Grassman and Clifford algebras which are defined as extensions of
vectorial spaces.

I would be very grateful if anyone can give me some references on this 
topic.

Thanks,

Guillermo