6.4 Functor Definition

We will explain the fuctor definition next. For example, let us think about
a 2 variable fuctor. Let us assume that we want to make a new set Z from
the set (set)X,Y. We will explain what to do at this point.

X /\ Y → Z

set set set

definition

let X , Y be set;

func X /\ Y -> set

means

:N: x in it iff

x in X & x in Y;

existence ......;

uniqueness

proof

end;

end;

This case also allows for it to be written in the operation
form instead of the definition of a function like . Let us assume that we want to define such a symbol as . To make a new set Z from sets X and Y is truly this functor. With let
X,Y be set;, we have sets X, Y ready. In addition, func X /\ Y -> set indicates X /\ Y as a set. The next line after means is the meaning of that functor. We will then write the meaning of the functor by placing a label like before. In this meaning, X /\ Y is indicated as it.

In addition, in the demonstration section (contents of the
meaning) , we have to demonstrate the existence and uniqueness. In other
words, we have to express its existence and uniqueness (the existence is
only one).

For the demonstration for uniqueness, we only have to state
the following.

If we take A1 and A2 as it:

(x in A1 ⇔ x in X & x in
Y)

and (x in A2 ⇔ x in X & x in Y)

⇒ A1 = A2

If we write this, it will be as below:

uniqueness

proof

let A1,A2 be set such that

A1: x in A1 iff x in X & x in Y

and

A2: x in A2 iff x in X & x in
Y;

now let y;

y in A1 iff y in X & y in Y by A1;

hence y in A1 iff y in A2 by A2;

end:

hence A1=A2 by TARSKI:2;

In short, when we bring in the two sets A1 and A2 that satisfy this condition, by demonstrating the equality of these two sets, the uniqueness is in fact demonstrated.

In this demonstration of uniqueness, because it is such that
in the third line, one can see that after it the two sentences label A1
and label A2 are connected with and. It is stated as now let y. Let us
assume that this y is reserved as set. In addition, by label A1 we can
state as y in A1 iff y in X & y in Y, and therefore, by label A2, y
in A1 iff y in A2 can be stated. In addition, it means that enough necessary
conditions for A1=A2 are demonstrated by TARSKI:2 stating that y in A1
and y in A2 are equally corresponding with the optional y; therefore, A1=A2
are demonstrated.

We also have to demonstrate the existence in the same way;
however, we have to state that such an it exists. That is, let us demonstrate
for the following.

ex A being set st for x

holds x in A1 iff x in X & x in Y