Programming basic computer algebra in a language with dependent types

It is described the experience in provable programming of certain classical categories of computational algebra (“group”, “ring”, and so on) basing on the approach of intuitionism, a language with dependent types, forming of machine-checked proofs. There are detected the related problems, and are described certain additional possibilities given by the approach. The Agda functional language is used as an instrument. This paper is a continuation for the introductory paper published in this journal in 2014. (In Russian).