Trying to decode a module functor

Question

This is section 5.1 from, ARITHMETIC DERIVATIVES THROUGH GEOMETRY OF NUMBERS by Hector Pasten.

Let $A$ be a commutative unitary ring, let $R$ be a commutative monoid, and let $\alpha : R \to A$ be a morphism of monoids with $A$ taken as a multiplicative monoid. Given an $A$-module $U$, a $U$-valued $\alpha$-derivation on $A$ is a function $D : A \to U$ satisfying

1. (Diff1) $R$-triviality: $D(\alpha(r)) = 0$ for all $r ∈ R$;
2. (Diff2) Leibniz rule: $D(ab) = a \, D(b) + b \, D(a)$ for all $a, b ∈ A$. A differential $(A, \alpha)$-module is a pair $(U , D)$, where $U$ is an $A$-module and $D$ is a $U$-valued $\alpha$-derivation on $A$.

A differential $(A, \alpha)$-module is a pair $(U , D)$, where $U$ is an $A$-module and $D$ is a $U$-valued $\alpha$-derivation on $A$.

Given differential $(A, \alpha)$-modules $(U, D)$ and $(V, E)$, a morphism of differential $(A, \alpha)$-modules is a morphism of $A$-modules $f : U \rightarrow V$ that satisfies $E = f \circ D$. We obtain a category of differential $(A, \alpha)$-modules which we denote by $Φ(A,\alpha)$.

For an $A$-module $U$, let $$Der(A,\alpha)(U) = \{D : A \to U : (U,D) \in Ob(Φ(A,\alpha))\}.$$ This is an $A$-module with the structure induced by $U$. Given $A$-modules $U$ and $V$ and a morphism $f \in Hom_A(U, V)$, we define $$Der(A,\alpha)(f) : Der(A,\alpha)(U) \to Der(A,\alpha)(V)$$ by $Der(A,\alpha)(f)(D) = f \circ D$.

Lemma 5.2. The rule $Der(A,\alpha)$ defines a functor $A{-}\mathbf{Mod} \rightarrow A{-}\mathbf{Mod}$.

The lemma 5.2 is provided without a proof.

I am left to wonder how is this map on objects defined given an $A$-module $U$, I cant see how to read the set builder style notation for objects in a way that makes sense to me. How should one read it?

To note some of the confusing bits about this section: $D, E$ are functions, $f$ is a morphism of $A$-modules their composition is a morphism of $A$-modules, I understand how this yields another function. Are morphism of $A$-modules post-composed with functions again sensible morphisms of $A$-modules in some way?