Free Many Sorted Universal Algebra
Beata Perkowska · 1996
The following proposition is true (1) Let I be a set, and let J be a non empty set, and let f be a function from I into J∗, and let X be a many sorted set of J , and let p be an element of J∗, and let x be arbitrary. If x ∈ I and p = f(x), then (X · f)(x) = ∏ (X · p). Let I be a set, let A, B be many sorted sets of I, let C be a many sorted subset of A, and let F be a many sorted function from A into B. The functor F C yielding a many sorted function from C into B is defined as follows: (Def.1) For arbitrary i such that i ∈ I and for every function f from A(i) into B(i) such that f = F (i) holds (F C)(i) = f C(i). Let I be a set, let X be a many sorted set of I, and let i be arbitrary. Let us assume that i ∈ I. The functor coprod(i,X) yields a set and is defined as follows: (Def.2) For arbitrary x holds x ∈ coprod(i,X) iff there exists arbitrary a such that a ∈ X(i) and x = 〈a, i〉. Let I be a set and let X be a many sorted set of I. Then disjointX is a many sorted set of I and it can be characterized by the condition: (Def.3) For arbitrary i such that i ∈ I holds (disjointX)(i) = coprod(i,X).