Programming computer algebra with basing on constructive mathematics. Domains with factorization

The paper continues prevoius author publications on a constructive mathematics approach in computational algebra using a language with dependent types.
A constructive expression for the notion of a domain with factorization to primes for a monoid and for a ring possessing certain additionnal properties is obtained. A way to achieve constructed machine-checked proofs for theorems that relate the factorization notion for domains of different kinds is discussed.
All the described methods and proofs are completely implemented as a working program written in the Agda functional language. (In Russian).