### Properties

#### Properties - Predicates

reflexivity
```definition
let X, Y be set;
pred X = Y means psi_1[X,Y];
reflexivity
proof
thus for A being set holds psi_1[A,A];
end;
end;
```
```definition
let X, Y be set;
pred X = Y means
phi_1[X,Y] if C1[X,Y],
phi_2[X,Y] if C2[X,Y],
phi_3[X,Y] if C3[X,Y]
otherwise phi_4[X,Y];
consistency;
reflexivity
proof
let A be set;
thus C1[A,A] implies phi_1[A,A];
thus C2[A,A] implies phi_2[A,A];
thus C3[A,A] implies phi_3[A,A];
thus not C1[A,A] & not C2[A,A] & not C3[A,A] implies phi_4[A,A];
end;
end;
```
irreflexivity
```definition
let X, Y be set;
pred X = Y means psi_1[X,Y];
irreflexivity
proof
thus for A being set holds not psi_1[A,A];
end;
end;
```
```definition
let X, Y be set;
pred X = Y means
phi_1[X,Y] if C1[X,Y],
phi_2[X,Y] if C2[X,Y],
phi_3[X,Y] if C3[X,Y]
otherwise phi_4[X,Y];
consistency;
irreflexivity
proof
let A be set;
thus not
(
(C1[A,A] implies phi_1[A,A]) &
(C2[A,A] implies phi_2[A,A]) &
(C3[A,A] implies phi_3[A,A]) &
(not C1[A,A] & not C2[A,A] & not C3[A,A] implies phi_4[A,A])
);
end;
end;
```
symmetry
```definition
let X, Y be set;
pred X = Y means psi_1[X,Y];
symmetry
proof
thus for A, B being set holds psi_1[A,B] implies psi_1[B,A];
end;
end;
```
```definition
let X, Y be set;
pred X = Y means
phi_1[X,Y] if C1[X,Y],
phi_2[X,Y] if C2[X,Y],
phi_3[X,Y] if C3[X,Y]
otherwise phi_4[X,Y];
consistency;
symmetry
proof
let A, B be set;
thus
(C1[A,B] implies phi_1[A,B]) &
(C2[A,B] implies phi_2[A,B]) &
(C3[A,B] implies phi_3[A,B]) &
(not C1[A,B] & not C2[A,B]& not C3[A,B] implies phi_4[A,B])
implies
(C1[B,A] implies phi_1[B,A]) &
(C2[B,A] implies phi_2[B,A]) &
(C3[B,A] implies phi_3[B,A]) &
(not C1[B,A] & not C2[B,A] & not C3[B,A] implies phi_4[B,A]);
end;
end;
```
asymmetry
```definition
let X, Y be set;
pred X = Y means psi_1[X,Y];
asymmetry
proof
thus for A, B being set holds psi_1[A,B] implies not psi_1[B,A];
end;
end;
```
```definition
let X, Y be set;
pred X = Y means
phi_1[X,Y] if C1[X,Y],
phi_2[X,Y] if C2[X,Y],
phi_3[X,Y] if C3[X,Y]
otherwise phi_4[X,Y];
consistency;
asymmetry
proof
let A, B be set;
thus
(C1[A,B] implies phi_1[A,B]) &
(C2[A,B] implies phi_2[A,B]) &
(C3[A,B] implies phi_3[A,B]) &
(not C1[A,B] & not C2[A,B]& not C3[A,B] implies phi_4[A,B])
implies
not (
(C1[B,A] implies phi_1[B,A]) &
(C2[B,A] implies phi_2[B,A]) &
(C3[B,A] implies phi_3[B,A]) &
(not C1[B,A] & not C2[B,A] & not C3[B,A] implies phi_4[B,A])
);
end;
end;
```
connectedness
```definition
let X, Y be set;
pred X = Y means psi_1[X,Y];
connectedness
proof
thus for A, B being set holds psi_1[A,B] or psi_1[B,A];
end;
end;
```
```definition
let X, Y be set;
pred X c= Y means
phi_1[X,Y] if C1[X,Y],
phi_2[X,Y] if C2[X,Y],
phi_3[X,Y] if C3[X,Y]
otherwise phi_4[X,Y];
consistency;
connectedness
proof
let A, B be set;
thus
not (
(C1[A,B] implies phi_1[A,B]) &
(C2[A,B] implies phi_2[A,B]) &
(C3[A,B] implies phi_3[A,B]) &
(not C1[A,B] & not C2[A,B]& not C3[A,B] implies phi_4[A,B])
)
implies
(C1[B,A] implies phi_1[B,A]) &
(C2[B,A] implies phi_2[B,A]) &
(C3[B,A] implies phi_3[B,A]) &
(not C1[B,A] & not C2[B,A] & not C3[B,A] implies phi_4[B,A]);
end;
end;
```

#### Properties - Functors

involutiveness
involutiveness - means
```definition
let X be set;
func +X -> set means psi_1[it,X];
existence;
uniqueness;
involutiveness
proof
thus for r, A being set st psi_1[r,A] holds psi_1[A,r];
end;
end;
```
```definition
let X be set;
func +X -> set means
phi_1[it,X] if G1[X],
phi_2[it,X] if G2[X],
phi_3[it,X] if G3[X]
otherwise phi_4[it,X];
existence;
uniqueness;
consistency;
involutiveness
proof
let IT, x be set;
thus
(G1[x] implies phi_1[IT,x]) &
(G2[x] implies phi_2[IT,x]) &
(G3[x] implies phi_3[IT,x]) &
(not G1[x] & not G2[x] & not G3[x] implies phi_4[IT,x])
implies
(G1[IT] implies phi_1[x,IT]) &
(G2[IT] implies phi_2[x,IT]) &
(G3[IT] implies phi_3[x,IT]) &
(not G1[IT] & not G2[IT] & not G3[IT] implies phi_4[x,IT]);
end;
end;
```
involutiveness - equals
```definition
let X be set;
func +X -> set equals tau_1(X);
coherence;
involutiveness
proof
thus for r, A being set st r = tau_1(A) holds A = tau_1(r);
end;
end;
```
```definition
let X be set;
func +X -> set equals
tau_1(X) if G1[X],
tau_2(X) if G2[X],
tau_3(X) if G3[X]
otherwise tau_4(X);
coherence;
consistency;
involutiveness
proof
let IT, x be set;
thus
(G1[x] implies IT = tau_1(x)) &
(G2[x] implies IT = tau_2(x)) &
(G3[x] implies IT = tau_3(x)) &
(not G1[x] & not G2[x] & not G3[x] implies IT = tau_4(x))
implies
(G1[IT] implies x = tau_1(IT)) &
(G2[IT] implies x = tau_2(IT)) &
(G3[IT] implies x = tau_3(IT)) &
(not G1[IT] & not G2[IT] & not G3[IT] implies x = tau_4(IT));
end;
end;
```
projectivity
projectivity - means
```definition
let X be set;
func +X -> set means psi_1[it,X];
existence;
uniqueness;
projectivity
proof
thus for r, A being set st psi_1[r,A] holds psi_1[r,r];
end;
end;
```
```definition
let X be set;
func +X -> set means
phi_1[it,X] if G1[X],
phi_2[it,X] if G2[X],
phi_3[it,X] if G3[X]
otherwise phi_4[it,X];
existence;
uniqueness;
consistency;
projectivity
proof
let IT, x be set;
thus
(G1[x] implies phi_1[IT,x]) &
(G2[x] implies phi_2[IT,x]) &
(G3[x] implies phi_3[IT,x]) &
(not G1[x] & not G2[x] & not G3[x] implies phi_4[IT,x])
implies
(G1[IT] implies phi_1[IT,IT]) &
(G2[IT] implies phi_2[IT,IT]) &
(G3[IT] implies phi_3[IT,IT]) &
(not G1[IT] & not G2[IT] & not G3[IT] implies phi_4[IT,IT]);
end;
end;
```
projectivity - equals
```definition
let X be set;
func +X -> set equals tau_1(X);
coherence;
projectivity
proof
thus for r, A being set st r = tau_1(A) holds r = tau_1(r);
end;
end;
```
```definition
let X be set;
func +X -> set equals
tau_1(X) if G1[X],
tau_2(X) if G2[X],
tau_3(X) if G3[X]
otherwise tau_4(X);
coherence;
consistency;
projectivity
proof
let IT, x be set;
thus
(G1[x] implies IT = tau_1(x)) &
(G2[x] implies IT = tau_2(x)) &
(G3[x] implies IT = tau_3(x)) &
(not G1[x] & not G2[x] & not G3[x] implies IT = tau_4(x))
implies
(G1[IT] implies IT = tau_1(IT)) &
(G2[IT] implies IT = tau_2(IT)) &
(G3[IT] implies IT = tau_3(IT)) &
(not G1[IT] & not G2[IT] & not G3[IT] implies IT = tau_4(IT));
end;
end;
```
commutativity
commutativity - means
```definition
let X, Y be set;
func X + Y -> set means psi_1[it,X,Y];
existence;
uniqueness;
commutativity
proof
thus for r, A, B being set holds psi_1[r,A,B] implies psi_1[r,B,A];
end;
end;
```
```definition
let X, Y be set;
func X + Y -> set means
psi_1[it,X,Y] if C1[X,Y],
psi_2[it,X,Y] if C2[X,Y],
psi_3[it,X,Y] if C3[X,Y]
otherwise psi_4[it,X,Y];
existence;
uniqueness;
consistency;
commutativity
proof
let IT, x, y be set;
thus
(C1[x,y] implies psi_1[IT,x,y]) &
(C2[x,y] implies psi_2[IT,x,y]) &
(C3[x,y] implies psi_3[IT,x,y]) &
(not C1[x,y] & not C2[x,y] & not C3[x,y] implies psi_4[IT,x,y])
implies
(C1[y,x] implies psi_1[IT,y,x]) &
(C2[y,x] implies psi_2[IT,y,x]) &
(C3[y,x] implies psi_3[IT,y,x]) &
(not C1[y,x] & not C2[y,x] & not C3[y,x] implies psi_4[IT,y,x]);
end;
end;
```
commutativity - equals
```definition
let X, Y be set;
func X + Y -> set equals tau_1(X,Y);
coherence;
commutativity
proof
thus for r, A, B being set st r = tau_1(A,B) holds r = tau_1(B,A);
end;
end;
```
```definition
let X, Y be set;
func X + Y -> set equals
tau_1(X,Y) if C1[X,Y],
tau_2(X,Y) if C2[X,Y],
tau_3(X,Y) if C3[X,Y]
otherwise tau_4(X,Y);
coherence;
consistency;
commutativity
proof
let IT, x, y be set;
thus
(C1[x,y] implies IT = tau_1(x,y)) &
(C2[x,y] implies IT = tau_2(x,y)) &
(C3[x,y] implies IT = tau_3(x,y)) &
(not C1[x,y] & not C2[x,y] & not C3[x,y] implies IT = tau_4(x,y))
implies
(C1[y,x] implies IT = tau_1(y,x)) &
(C2[y,x] implies IT = tau_2(y,x)) &
(C3[y,x] implies IT = tau_3(y,x)) &
(not C1[y,x] & not C2[y,x] & not C3[y,x] implies IT = tau_4(y,x));
end;
end;
```
idempotence
idempotence - means
```definition
let X, Y be set;
func X + Y -> set means psi_1[it,X,Y];
existence;
uniqueness;
idempotence
proof
thus for A being set holds psi_1[A,A,A];
end;
end;
```
```definition
let X, Y be set;
func X + Y -> set means
psi_1[it,X,Y] if C1[X,Y],
psi_2[it,X,Y] if C2[X,Y],
psi_3[it,X,Y] if C3[X,Y]
otherwise psi_4[it,X,Y];
existence;
uniqueness;
consistency;
idempotence
proof
let IT be set;
thus C1[IT,IT] implies psi_1[IT,IT,IT];
thus C2[IT,IT] implies psi_2[IT,IT,IT];
thus C3[IT,IT] implies psi_3[IT,IT,IT];
thus not C1[IT,IT] & not C2[IT,IT] & not C3[IT,IT]
implies psi_4[IT,IT,IT];
end;
end;
```
idempotence - equals
```definition
let X, Y be set;
func X + Y -> set equals F(X,Y);
coherence;
idempotence
proof
thus for A being set holds A = F(A,A);
end;
end;
```
```definition
let X, Y be set;
func X + Y -> set equals
tau_1(X,Y) if C1[X,Y],
tau_2(X,Y) if C2[X,Y],
tau_3(X,Y) if C3[X,Y]
otherwise tau_4(X,Y);
coherence;
consistency;
idempotence
proof
let IT be set;
thus C1[IT,IT] implies IT = tau_1(IT,IT);
thus C2[IT,IT] implies IT = tau_2(IT,IT);
thus C3[IT,IT] implies IT = tau_3(IT,IT);
thus not C1[IT,IT] & not C2[IT,IT] & not C3[IT,IT]
implies IT = tau_4(IT,IT);
end;
end;
```