Primitive recursion on higher types

A revision of the basic concepts of type, function (called here operation), and relation is proposed. A simple generic method is presented for constructing operations and types as concrete finite structures parameterized by natural numbers. The method gives rise to build inductively so called Universe intended to contain all what can be effectively constructed. For any (higher order) type A the operation of type Rec_A : (N;(N → (A → A))) → (A → A) is constructed that corresponds to primitive recursion of Grzegorzyk [1] and Girard [2].