add formalization of Arrows and Freyd Categories