For abelian groups and and a function , let us define the types
is an abelian group homomorphism if has a term. Since an abelian group is a set, the identity types are propositions and thus preserved in an abelian group homomorphism.
The type of abelian group homomorphisms between abelian groups and is defined as