functor (R : Ring.Euclidean-> T