Definition. Signature over given types
(called indices) is an element of type .
Where denotes coproduct type.

Definition. Vector of length over type
(denoted ) is a type:
Where denotes unit type that contains
only .

Definition. Assume we have types ,
function , and a natural number .
Then we define function :
≔

Definition.-ary algebraic operation over given
type is an element of type:

Definition.-ary algebraic relation over given
type is an element of type:
Where denotes type of all propositions, i.e.
≔

Definition. Algebraic structure over signature constists of:
(i) 0-Type called carrier,
(ii) -ary algebraic operation for each ,
(iii) -ary algebraic relation for each .
Or, more explicitly:
≔ We will write for carrier of algebraic structure ,
for its algebraic operations,
and for its relations.

Mappings

(Homomorphism). Given two algebraic structures over signature
and a function between them ,
we say that is homomorphism iff holds:
(i) ,
(ii) ,
for each or and .

Composition of two homomorphisms is also homomorphism.

(Isomorphism). We say that
is an ismorphism iff it is bijective and homomorphism.
Then we can say that and are isomorphic and write .

Isomorphism is an equivalence relation, i.e.
(i) ,
(ii) ,
(iii) .