:: Categories without Uniqueness of { \bf cod } and { \bf dom }
:: by Andrzej Trybulec
::
:: Received February 28, 1995
:: Copyright (c) 1995-2012 Association of Mizar Users


begin

theorem Th1: :: ALTCAT_1:1
for A being set holds id A in Funcs (A,A)
proofend;

theorem Th2: :: ALTCAT_1:2
Funcs ({},{}) = {(id {})}
proofend;

theorem Th3: :: ALTCAT_1:3
for A, B, C being set
for f, g being Function st f in Funcs (A,B) & g in Funcs (B,C) holds
g * f in Funcs (A,C)
proofend;

theorem Th4: :: ALTCAT_1:4
for A, B, C being set st Funcs (A,B) <> {} &amp; Funcs (B,C) <> {} holds
Funcs (A,C) <> {}
proofend;

theorem :: ALTCAT_1:5
for A, B being set
for F being ManySortedSet of [:B,A:]
for C being Subset of A
for D being Subset of B
for x, y being set st x in C &amp; y in D holds
F . (y,x) = (F | [:D,C:]) . (y,x)
proofend;

scheme :: ALTCAT_1:sch 1
MSSLambda2{ F1() ->  set , F2() ->  set , F3( set , set ) ->  set } :
 ex M being ManySortedSet of [:F1(),F2():] st
for i, j being set st i in F1() &amp; j in F2() holds
M . (i,j) = F3(i,j)
proofend;

scheme :: ALTCAT_1:sch 2
MSSLambda2D{ F1() ->  non empty set , F2() ->  non empty set , F3( set , set ) ->  set } :
 ex M being ManySortedSet of [:F1(),F2():] st
for i being Element of F1()
for j being Element of F2() holds M . (i,j) = F3(i,j)
proofend;

scheme :: ALTCAT_1:sch 3
MSSLambda3{ F1() ->  set , F2() ->  set , F3() ->  set , F4( set , set , set ) ->  set } :
 ex M being ManySortedSet of [:F1(),F2(),F3():] st
for i, j, k being set st i in F1() &amp; j in F2() &amp; k in F3() holds
M . (i,j,k) = F4(i,j,k)
proofend;

scheme :: ALTCAT_1:sch 4
MSSLambda3D{ F1() ->  non empty set , F2() ->  non empty set , F3() ->  non empty set , F4( set , set , set ) ->  set } :
 ex M being ManySortedSet of [:F1(),F2(),F3():] st
for i being Element of F1()
for j being Element of F2()
for k being Element of F3() holds M . (i,j,k) = F4(i,j,k)
proofend;

theorem Th6: :: ALTCAT_1:6
for A, B being set
for N, M being ManySortedSet of [:A,B:] st ( for i, j being set st i in A &amp; j in B holds
N . (i,j) = M . (i,j) ) holds
M = N
proofend;

theorem Th7: :: ALTCAT_1:7
for A, B being non empty set
for N, M being ManySortedSet of [:A,B:] st ( for i being Element of A
for j being Element of B holds N . (i,j) = M . (i,j) ) holds
M = N
proofend;

theorem Th8: :: ALTCAT_1:8
for A being set
for N, M being ManySortedSet of [:A,A,A:] st ( for i, j, k being set st i in A &amp; j in A &amp; k in A holds
N . (i,j,k) = M . (i,j,k) ) holds
M = N
proofend;

theorem :: ALTCAT_1:9
for i, j, k being set holds (i,j) :-> k = [i,j] .--> k ;

theorem Th10: :: ALTCAT_1:10
for i, j, k being set holds ((i,j) :-> k) . (i,j) = k
proofend;

begin

definition
attrc1 is strict ;
struct AltGraph  ->  1-sorted ;
aggrAltGraph(# carrier, Arrows #) ->  AltGraph ;
sel Arrows c1 ->  ManySortedSet of [: the carrier of c1, the carrier of c1:];
end;

definition
let G be AltGraph ;
mode object of G is Element of G;
end;

definition
let G be AltGraph ;
let o1, o2 be object of G;
func<^o1,o2^> ->  set  equals :: ALTCAT_1:def 1
 the Arrows of G . (o1,o2);
correctness
coherence
the Arrows of G . (o1,o2) is set ;
;
end;

:: deftheorem  defines <^ ALTCAT_1:def_1_:_
 for G being AltGraph
for o1, o2 being object of G holds <^o1,o2^> = the Arrows of G . (o1,o2);

definition
let G be AltGraph ;
let o1, o2 be object of G;
mode Morphism of o1,o2 is Element of <^o1,o2^>;
end;

definition
let G be AltGraph ;
attrG is transitive  means :Def2: :: ALTCAT_1:def 2
 for o1, o2, o3 being object of G st <^o1,o2^> <> {} &amp; <^o2,o3^> <> {} holds
<^o1,o3^> <> {} ;
end;

:: deftheorem Def2 defines transitive ALTCAT_1:def_2_:_
 for G being AltGraph holds
( G is transitive iff for o1, o2, o3 being object of G st <^o1,o2^> <> {} &amp; <^o2,o3^> <> {} holds
<^o1,o3^> <> {} );

begin

definition
let I be set ;
let G be ManySortedSet of [:I,I:];
func{|G|} ->  ManySortedSet of [:I,I,I:] means :Def3: :: ALTCAT_1:def 3
 for i, j, k being set st i in I &amp; j in I &amp; k in I holds
it . (i,j,k) = G . (i,k);
existence
 ex b1 being ManySortedSet of [:I,I,I:] st
for i, j, k being set st i in I &amp; j in I &amp; k in I holds
b1 . (i,j,k) = G . (i,k)
proofend;
uniqueness
 for b1, b2 being ManySortedSet of [:I,I,I:] st ( for i, j, k being set st i in I &amp; j in I &amp; k in I holds
b1 . (i,j,k) = G . (i,k) ) &amp; ( for i, j, k being set st i in I &amp; j in I &amp; k in I holds
b2 . (i,j,k) = G . (i,k) ) holds
b1 = b2
proofend;
let H be ManySortedSet of [:I,I:];
func{|G,H|} ->  ManySortedSet of [:I,I,I:] means :Def4: :: ALTCAT_1:def 4
 for i, j, k being set st i in I &amp; j in I &amp; k in I holds
it . (i,j,k) = [:(H . (j,k)),(G . (i,j)):];
existence
 ex b1 being ManySortedSet of [:I,I,I:] st
for i, j, k being set st i in I &amp; j in I &amp; k in I holds
b1 . (i,j,k) = [:(H . (j,k)),(G . (i,j)):]
proofend;
uniqueness
 for b1, b2 being ManySortedSet of [:I,I,I:] st ( for i, j, k being set st i in I &amp; j in I &amp; k in I holds
b1 . (i,j,k) = [:(H . (j,k)),(G . (i,j)):] ) &amp; ( for i, j, k being set st i in I &amp; j in I &amp; k in I holds
b2 . (i,j,k) = [:(H . (j,k)),(G . (i,j)):] ) holds
b1 = b2
proofend;
end;

:: deftheorem Def3 defines {| ALTCAT_1:def_3_:_
 for I being set
for G being ManySortedSet of [:I,I:]
for b3 being ManySortedSet of [:I,I,I:] holds
( b3 = {|G|} iff for i, j, k being set st i in I &amp; j in I &amp; k in I holds
b3 . (i,j,k) = G . (i,k) );

:: deftheorem Def4 defines {| ALTCAT_1:def_4_:_
 for I being set
for G, H being ManySortedSet of [:I,I:]
for b4 being ManySortedSet of [:I,I,I:] holds
( b4 = {|G,H|} iff for i, j, k being set st i in I &amp; j in I &amp; k in I holds
b4 . (i,j,k) = [:(H . (j,k)),(G . (i,j)):] );

definition
let I be set ;
let G be ManySortedSet of [:I,I:];
mode BinComp of G is ManySortedFunction of {|G,G|},{|G|};
end;

definition
let I be non empty set ;
let G be ManySortedSet of [:I,I:];
let o be BinComp of G;
let i, j, k be Element of I;
:: original:.
redefine funco . (i,j,k) ->  Function of [:(G . (j,k)),(G . (i,j)):],(G . (i,k));
coherence
 o . (i,j,k) is Function of [:(G . (j,k)),(G . (i,j)):],(G . (i,k))
proofend;
end;

definition
let I be non empty set ;
let G be ManySortedSet of [:I,I:];
let IT be BinComp of G;
attrIT is associative  means :Def5: :: ALTCAT_1:def 5
 for i, j, k, l being Element of I
for f, g, h being set st f in G . (i,j) &amp; g in G . (j,k) &amp; h in G . (k,l) holds
(IT . (i,k,l)) . (h,((IT . (i,j,k)) . (g,f))) = (IT . (i,j,l)) . (((IT . (j,k,l)) . (h,g)),f);
attrIT is with_right_units  means :Def6: :: ALTCAT_1:def 6
 for i being Element of I ex e being set st
( e in G . (i,i) &amp; ( for j being Element of I
for f being set st f in G . (i,j) holds
(IT . (i,i,j)) . (f,e) = f ) );
attrIT is with_left_units  means :Def7: :: ALTCAT_1:def 7
 for j being Element of I ex e being set st
( e in G . (j,j) &amp; ( for i being Element of I
for f being set st f in G . (i,j) holds
(IT . (i,j,j)) . (e,f) = f ) );
end;

:: deftheorem Def5 defines associative ALTCAT_1:def_5_:_
 for I being non empty set
for G being ManySortedSet of [:I,I:]
for IT being BinComp of G holds
( IT is associative iff for i, j, k, l being Element of I
for f, g, h being set st f in G . (i,j) &amp; g in G . (j,k) &amp; h in G . (k,l) holds
(IT . (i,k,l)) . (h,((IT . (i,j,k)) . (g,f))) = (IT . (i,j,l)) . (((IT . (j,k,l)) . (h,g)),f) );

:: deftheorem Def6 defines with_right_units ALTCAT_1:def_6_:_
 for I being non empty set
for G being ManySortedSet of [:I,I:]
for IT being BinComp of G holds
( IT is with_right_units iff for i being Element of I ex e being set st
( e in G . (i,i) &amp; ( for j being Element of I
for f being set st f in G . (i,j) holds
(IT . (i,i,j)) . (f,e) = f ) ) );

:: deftheorem Def7 defines with_left_units ALTCAT_1:def_7_:_
 for I being non empty set
for G being ManySortedSet of [:I,I:]
for IT being BinComp of G holds
( IT is with_left_units iff for j being Element of I ex e being set st
( e in G . (j,j) &amp; ( for i being Element of I
for f being set st f in G . (i,j) holds
(IT . (i,j,j)) . (e,f) = f ) ) );

begin

definition
attrc1 is strict ;
struct AltCatStr  ->  AltGraph ;
aggrAltCatStr(# carrier, Arrows, Comp #) ->  AltCatStr ;
sel Comp c1 ->  BinComp of the Arrows of c1;
end;

registration
cluster non empty strict for AltCatStr ;
existence
 ex b1 being AltCatStr st
( b1 is strict &amp; not b1 is empty )
proofend;
end;

definition
let C be non empty AltCatStr ;
let o1, o2, o3 be object of C;
assume A1: ( <^o1,o2^> <> {} &amp; <^o2,o3^> <> {} ) ;
let f be Morphism of o1,o2;
let g be Morphism of o2,o3;
funcg * f ->  Morphism of o1,o3 equals :Def8: :: ALTCAT_1:def 8
( the Comp of C . (o1,o2,o3)) . (g,f);
coherence
 ( the Comp of C . (o1,o2,o3)) . (g,f) is Morphism of o1,o3
proofend;
correctness
;
end;

:: deftheorem Def8 defines * ALTCAT_1:def_8_:_
 for C being non empty AltCatStr
for o1, o2, o3 being object of C st <^o1,o2^> <> {} &amp; <^o2,o3^> <> {} holds
for f being Morphism of o1,o2
for g being Morphism of o2,o3 holds g * f = ( the Comp of C . (o1,o2,o3)) . (g,f);

definition
let IT be Function;
attrIT is compositional  means :Def9: :: ALTCAT_1:def 9
 for x being set st x in dom IT holds
ex f, g being Function st
( x = [g,f] &amp; IT . x = g * f );
end;

:: deftheorem Def9 defines compositional ALTCAT_1:def_9_:_
 for IT being Function holds
( IT is compositional iff for x being set st x in dom IT holds
ex f, g being Function st
( x = [g,f] &amp; IT . x = g * f ) );

registration
let A, B be functional set ;
cluster Relation-like [:A,B:] -defined Function-like V14([:A,B:]) Function-yielding V25() compositional for set ;
existence
 ex b1 being ManySortedFunction of [:A,B:] st b1 is compositional
proofend;
end;

theorem Th11: :: ALTCAT_1:11
for A, B being functional set
for F being compositional ManySortedSet of [:A,B:]
for g, f being Function st g in A &amp; f in B holds
F . (g,f) = g * f
proofend;

definition
let A, B be functional set ;
func FuncComp (A,B) ->  compositional ManySortedFunction of [:B,A:] means :Def10: :: ALTCAT_1:def 10
verum;
uniqueness
 for b1, b2 being compositional ManySortedFunction of [:B,A:] holds b1 = b2
proofend;
correctness
existence
ex b1 being compositional ManySortedFunction of [:B,A:] st verum;
;
end;

:: deftheorem Def10 defines FuncComp ALTCAT_1:def_10_:_
 for A, B being functional set
for b3 being compositional ManySortedFunction of [:B,A:] holds
( b3 = FuncComp (A,B) iff verum );

theorem Th12: :: ALTCAT_1:12
for A, B, C being set holds rng (FuncComp ((Funcs (A,B)),(Funcs (B,C)))) c= Funcs (A,C)
proofend;

theorem Th13: :: ALTCAT_1:13
for o being set holds FuncComp ({(id o)},{(id o)}) = ((id o),(id o)) :-> (id o)
proofend;

theorem Th14: :: ALTCAT_1:14
for A, B being functional set
for A1 being Subset of A
for B1 being Subset of B holds FuncComp (A1,B1) = (FuncComp (A,B)) | [:B1,A1:]
proofend;

:: Kategorie przeksztalcen, Semadeni Wiweger, 1.2.2, str.15
definition
let C be non empty AltCatStr ;
attrC is quasi-functional  means :Def11: :: ALTCAT_1:def 11
 for a1, a2 being object of C holds <^a1,a2^> c= Funcs (a1,a2);
attrC is semi-functional  means :Def12: :: ALTCAT_1:def 12
 for a1, a2, a3 being object of C st <^a1,a2^> <> {} &amp; <^a2,a3^> <> {} &amp; <^a1,a3^> <> {} holds
for f being Morphism of a1,a2
for g being Morphism of a2,a3
for f9, g9 being Function st f = f9 &amp; g = g9 holds
g * f = g9 * f9;
attrC is pseudo-functional  means :Def13: :: ALTCAT_1:def 13
 for o1, o2, o3 being object of C holds the Comp of C . (o1,o2,o3) = (FuncComp ((Funcs (o1,o2)),(Funcs (o2,o3)))) | [:<^o2,o3^>,<^o1,o2^>:];
end;

:: deftheorem Def11 defines quasi-functional ALTCAT_1:def_11_:_
 for C being non empty AltCatStr holds
( C is quasi-functional iff for a1, a2 being object of C holds <^a1,a2^> c= Funcs (a1,a2) );

:: deftheorem Def12 defines semi-functional ALTCAT_1:def_12_:_
 for C being non empty AltCatStr holds
( C is semi-functional iff for a1, a2, a3 being object of C st <^a1,a2^> <> {} &amp; <^a2,a3^> <> {} &amp; <^a1,a3^> <> {} holds
for f being Morphism of a1,a2
for g being Morphism of a2,a3
for f9, g9 being Function st f = f9 &amp; g = g9 holds
g * f = g9 * f9 );

:: deftheorem Def13 defines pseudo-functional ALTCAT_1:def_13_:_
 for C being non empty AltCatStr holds
( C is pseudo-functional iff for o1, o2, o3 being object of C holds the Comp of C . (o1,o2,o3) = (FuncComp ((Funcs (o1,o2)),(Funcs (o2,o3)))) | [:<^o2,o3^>,<^o1,o2^>:] );

registration
let X be non empty set ;
let A be ManySortedSet of [:X,X:];
let C be BinComp of A;
cluster AltCatStr(# X,A,C #) ->  non empty ;
coherence
 not AltCatStr(# X,A,C #) is empty ;
end;

registration
cluster non empty strict pseudo-functional for AltCatStr ;
existence
 ex b1 being non empty AltCatStr st
( b1 is strict &amp; b1 is pseudo-functional )
proofend;
end;

theorem :: ALTCAT_1:15
for C being non empty AltCatStr
for a1, a2, a3 being object of C holds the Comp of C . (a1,a2,a3) is Function of [:<^a2,a3^>,<^a1,a2^>:],<^a1,a3^> ;

theorem Th16: :: ALTCAT_1:16
for C being non empty pseudo-functional AltCatStr
for a1, a2, a3 being object of C st <^a1,a2^> <> {} &amp; <^a2,a3^> <> {} &amp; <^a1,a3^> <> {} holds
for f being Morphism of a1,a2
for g being Morphism of a2,a3
for f9, g9 being Function st f = f9 &amp; g = g9 holds
g * f = g9 * f9
proofend;

:: Kategorie EnsCat(A), Semadeni Wiweger 1.2.3, str. 15
:: ale bez parametryzacji
definition
let A be non empty set ;
func EnsCat A ->  non empty strict pseudo-functional AltCatStr  means :Def14: :: ALTCAT_1:def 14
( the carrier of it = A &amp; ( for a1, a2 being object of it holds <^a1,a2^> = Funcs (a1,a2) ) );
existence
 ex b1 being non empty strict pseudo-functional AltCatStr st
( the carrier of b1 = A &amp; ( for a1, a2 being object of b1 holds <^a1,a2^> = Funcs (a1,a2) ) )
proofend;
uniqueness
 for b1, b2 being non empty strict pseudo-functional AltCatStr st the carrier of b1 = A &amp; ( for a1, a2 being object of b1 holds <^a1,a2^> = Funcs (a1,a2) ) &amp; the carrier of b2 = A &amp; ( for a1, a2 being object of b2 holds <^a1,a2^> = Funcs (a1,a2) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def14 defines EnsCat ALTCAT_1:def_14_:_
 for A being non empty set
for b2 being non empty strict pseudo-functional AltCatStr holds
( b2 = EnsCat A iff ( the carrier of b2 = A &amp; ( for a1, a2 being object of b2 holds <^a1,a2^> = Funcs (a1,a2) ) ) );

definition
let C be non empty AltCatStr ;
attrC is associative  means :Def15: :: ALTCAT_1:def 15
 the Comp of C is associative ;
attrC is with_units  means :Def16: :: ALTCAT_1:def 16
( the Comp of C is with_left_units &amp; the Comp of C is with_right_units );
end;

:: deftheorem Def15 defines associative ALTCAT_1:def_15_:_
 for C being non empty AltCatStr holds
( C is associative iff the Comp of C is associative );

:: deftheorem Def16 defines with_units ALTCAT_1:def_16_:_
 for C being non empty AltCatStr holds
( C is with_units iff ( the Comp of C is with_left_units &amp; the Comp of C is with_right_units ) );

Lm1:  for A being non empty set holds
( EnsCat A is transitive &amp; EnsCat A is associative &amp; EnsCat A is with_units )
proofend;

registration
cluster non empty transitive strict associative with_units for AltCatStr ;
existence
 ex b1 being non empty AltCatStr st
( b1 is transitive &amp; b1 is associative &amp; b1 is with_units &amp; b1 is strict )
proofend;
end;

theorem :: ALTCAT_1:17
for C being non empty transitive AltCatStr
for a1, a2, a3 being object of C holds
( dom ( the Comp of C . (a1,a2,a3)) = [:<^a2,a3^>,<^a1,a2^>:] &amp; rng ( the Comp of C . (a1,a2,a3)) c= <^a1,a3^> )
proofend;

theorem Th18: :: ALTCAT_1:18
for C being non empty with_units AltCatStr
for o being object of C holds <^o,o^> <> {}
proofend;

registration
let A be non empty set ;
cluster EnsCat A ->  non empty transitive strict pseudo-functional associative with_units ;
coherence
 ( EnsCat A is transitive &amp; EnsCat A is associative &amp; EnsCat A is with_units ) by Lm1;
end;

registration
cluster non empty transitive quasi-functional semi-functional  ->  non empty pseudo-functional for AltCatStr ;
coherence
 for b1 being non empty AltCatStr st b1 is quasi-functional &amp; b1 is semi-functional &amp; b1 is transitive holds
b1 is pseudo-functional
proofend;
cluster non empty transitive pseudo-functional with_units  ->  non empty quasi-functional semi-functional for AltCatStr ;
coherence
 for b1 being non empty AltCatStr st b1 is with_units &amp; b1 is pseudo-functional &amp; b1 is transitive holds
( b1 is quasi-functional &amp; b1 is semi-functional )
proofend;
end;

:: Definicja kategorii, Semadeni Wiweger 1.3.1, str. 16-17
definition
mode category is non empty transitive associative with_units AltCatStr ;
end;

begin

definition
let C be non empty with_units AltCatStr ;
let o be object of C;
func idm o ->  Morphism of o,o means :Def17: :: ALTCAT_1:def 17
 for o9 being object of C st <^o,o9^> <> {} holds
for a being Morphism of o,o9 holds a * it = a;
existence
 ex b1 being Morphism of o,o st
for o9 being object of C st <^o,o9^> <> {} holds
for a being Morphism of o,o9 holds a * b1 = a
proofend;
uniqueness
 for b1, b2 being Morphism of o,o st ( for o9 being object of C st <^o,o9^> <> {} holds
for a being Morphism of o,o9 holds a * b1 = a ) &amp; ( for o9 being object of C st <^o,o9^> <> {} holds
for a being Morphism of o,o9 holds a * b2 = a ) holds
b1 = b2
proofend;
end;

:: deftheorem Def17 defines idm ALTCAT_1:def_17_:_
 for C being non empty with_units AltCatStr
for o being object of C
for b3 being Morphism of o,o holds
( b3 = idm o iff for o9 being object of C st <^o,o9^> <> {} holds
for a being Morphism of o,o9 holds a * b3 = a );

theorem Th19: :: ALTCAT_1:19
for C being non empty with_units AltCatStr
for o being object of C holds idm o in <^o,o^>
proofend;

theorem :: ALTCAT_1:20
for C being non empty with_units AltCatStr
for o1, o2 being object of C st <^o1,o2^> <> {} holds
for a being Morphism of o1,o2 holds (idm o2) * a = a
proofend;

theorem :: ALTCAT_1:21
for C being non empty transitive associative AltCatStr
for o1, o2, o3, o4 being object of C st <^o1,o2^> <> {} &amp; <^o2,o3^> <> {} &amp; <^o3,o4^> <> {} holds
for a being Morphism of o1,o2
for b being Morphism of o2,o3
for c being Morphism of o3,o4 holds c * (b * a) = (c * b) * a
proofend;

begin

:: kategoria dyskretna, Semadeni Wiweger, 1.3.1, str.18
definition
let C be AltCatStr ;
attrC is quasi-discrete  means :Def18: :: ALTCAT_1:def 18
 for i, j being object of C st <^i,j^> <> {} holds
i = j;
attrC is pseudo-discrete  means :Def19: :: ALTCAT_1:def 19
 for i being object of C holds <^i,i^> is trivial ;
end;

:: deftheorem Def18 defines quasi-discrete ALTCAT_1:def_18_:_
 for C being AltCatStr holds
( C is quasi-discrete iff for i, j being object of C st <^i,j^> <> {} holds
i = j );

:: deftheorem Def19 defines pseudo-discrete ALTCAT_1:def_19_:_
 for C being AltCatStr holds
( C is pseudo-discrete iff for i being object of C holds <^i,i^> is trivial );

theorem :: ALTCAT_1:22
for C being non empty with_units AltCatStr holds
( C is pseudo-discrete iff for o being object of C holds <^o,o^> = {(idm o)} )
proofend;

registration
cluster1 -element  ->  quasi-discrete for AltCatStr ;
coherence
 for b1 being AltCatStr st b1 is 1 -element holds
b1 is quasi-discrete
proofend;
end;

theorem Th23: :: ALTCAT_1:23
( EnsCat 1 is pseudo-discrete &amp; EnsCat 1 is 1 -element )
proofend;

registration
cluster non empty trivial transitive strict associative with_units pseudo-discrete for AltCatStr ;
existence
 ex b1 being category st
( b1 is pseudo-discrete &amp; b1 is trivial &amp; b1 is strict ) by Th23;
end;

registration
cluster non empty trivial transitive strict associative with_units quasi-discrete pseudo-discrete for AltCatStr ;
existence
 ex b1 being category st
( b1 is quasi-discrete &amp; b1 is pseudo-discrete &amp; b1 is trivial &amp; b1 is strict ) by Th23;
end;

definition
mode discrete_category is quasi-discrete pseudo-discrete category;
end;

definition
let A be non empty set ;
func DiscrCat A ->  non empty strict quasi-discrete AltCatStr  means :Def20: :: ALTCAT_1:def 20
( the carrier of it = A &amp; ( for i being object of it holds <^i,i^> = {(id i)} ) );
existence
 ex b1 being non empty strict quasi-discrete AltCatStr st
( the carrier of b1 = A &amp; ( for i being object of b1 holds <^i,i^> = {(id i)} ) )
proofend;
correctness
uniqueness
for b1, b2 being non empty strict quasi-discrete AltCatStr st the carrier of b1 = A &amp; ( for i being object of b1 holds <^i,i^> = {(id i)} ) &amp; the carrier of b2 = A &amp; ( for i being object of b2 holds <^i,i^> = {(id i)} ) holds
b1 = b2;
proofend;
end;

:: deftheorem Def20 defines DiscrCat ALTCAT_1:def_20_:_
 for A being non empty set
for b2 being non empty strict quasi-discrete AltCatStr holds
( b2 = DiscrCat A iff ( the carrier of b2 = A &amp; ( for i being object of b2 holds <^i,i^> = {(id i)} ) ) );

registration
cluster quasi-discrete  ->  transitive for AltCatStr ;
coherence
 for b1 being AltCatStr st b1 is quasi-discrete holds
b1 is transitive
proofend;
end;

theorem Th24: :: ALTCAT_1:24
for A being non empty set
for o1, o2, o3 being object of (DiscrCat A) st ( o1 <> o2 or o2 <> o3 ) holds
the Comp of (DiscrCat A) . (o1,o2,o3) = {}
proofend;

theorem Th25: :: ALTCAT_1:25
for A being non empty set
for o being object of (DiscrCat A) holds the Comp of (DiscrCat A) . (o,o,o) = ((id o),(id o)) :-> (id o)
proofend;

registration
let A be non empty set ;
cluster DiscrCat A ->  non empty strict pseudo-functional associative with_units quasi-discrete pseudo-discrete ;
coherence
 ( DiscrCat A is pseudo-functional &amp; DiscrCat A is pseudo-discrete &amp; DiscrCat A is with_units &amp; DiscrCat A is associative )
proofend;
end;