:: ALTCAT_1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

registration
let A be functional set ;
cluster -> functional Element of bool A;
coherence
for b1 being Subset of A holds b1 is functional
proof end;
end;

registration
let f be Function-yielding Function;
let C be set ;
cluster f | C -> Function-yielding ;
correctness
coherence
f | C is Function-yielding
;
by MSUHOM_1:3;
end;

registration
let f be Function;
cluster {f} -> functional ;
coherence
{f} is functional
proof end;
end;

theorem :: ALTCAT_1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th2: :: ALTCAT_1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being set holds id A in Funcs A,A
proof end;

theorem Th3: :: ALTCAT_1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
Funcs {} ,{} = {(id {} )}
proof end;

theorem Th4: :: ALTCAT_1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th5: :: ALTCAT_1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B, C being set st Funcs A,B <> {} & Funcs B,C <> {} holds
Funcs A,C <> {}
proof end;

theorem :: ALTCAT_1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: ALTCAT_1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 & y in D holds
F . y,x = (F | [:D,C:]) . y,x
proof end;

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() & j in F2() holds
M . i,j = F3(i,j)
proof end;

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)
proof end;

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() & j in F2() & k in F3() holds
M . i,j,k = F4(i,j,k)
proof end;

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)
proof end;

theorem Th8: :: ALTCAT_1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B being set
for N, M being ManySortedSet of [:A,B:] st ( for i, j being set st i in A & j in B holds
N . i,j = M . i,j ) holds
M = N
proof end;

theorem Th9: :: ALTCAT_1:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th10: :: ALTCAT_1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being set
for N, M being ManySortedSet of [:A,A,A:] st ( for i, j, k being set st i in A & j in A & k in A holds
N . i,j,k = M . i,j,k ) holds
M = N
proof end;

theorem Th11: :: ALTCAT_1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, j, k being set holds i,j :-> k = [i,j] .--> k
proof end;

theorem Th12: :: ALTCAT_1:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, j, k being set holds (i,j :-> k) . i,j = k
proof end;

definition
attr c1 is strict;
struct AltGraph -> 1-sorted ;
aggr AltGraph(# 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;
canceled;
func <^o1,o2^> -> set equals :: ALTCAT_1:def 2
the Arrows of G . o1,o2;
correctness
coherence
the Arrows of G . o1,o2 is set
;
;
end;

:: deftheorem ALTCAT_1:def 1 :
canceled;

:: deftheorem defines <^ ALTCAT_1:def 2 :
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 ;
canceled;
attr G is transitive means :Def4: :: ALTCAT_1:def 4
for o1, o2, o3 being object of G st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds
<^o1,o3^> <> {} ;
end;

:: deftheorem ALTCAT_1:def 3 :
canceled;

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

definition
let I be set ;
let G be ManySortedSet of [:I,I:];
func {|G|} -> ManySortedSet of [:I,I,I:] means :Def5: :: ALTCAT_1:def 5
for i, j, k being set st i in I & j in I & 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 & j in I & k in I holds
b1 . i,j,k = G . i,k
proof end;
uniqueness
for b1, b2 being ManySortedSet of [:I,I,I:] st ( for i, j, k being set st i in I & j in I & k in I holds
b1 . i,j,k = G . i,k ) & ( for i, j, k being set st i in I & j in I & k in I holds
b2 . i,j,k = G . i,k ) holds
b1 = b2
proof end;
let H be ManySortedSet of [:I,I:];
func {|G,H|} -> ManySortedSet of [:I,I,I:] means :Def6: :: ALTCAT_1:def 6
for i, j, k being set st i in I & j in I & 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 & j in I & k in I holds
b1 . i,j,k = [:(H . j,k),(G . i,j):]
proof end;
uniqueness
for b1, b2 being ManySortedSet of [:I,I,I:] st ( for i, j, k being set st i in I & j in I & k in I holds
b1 . i,j,k = [:(H . j,k),(G . i,j):] ) & ( for i, j, k being set st i in I & j in I & k in I holds
b2 . i,j,k = [:(H . j,k),(G . i,j):] ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines {| ALTCAT_1:def 5 :
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 & j in I & k in I holds
b3 . i,j,k = G . i,k );

:: deftheorem Def6 defines {| ALTCAT_1:def 6 :
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 & j in I & 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 func o . 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
proof end;
end;

definition
let I be non empty set ;
let G be ManySortedSet of [:I,I:];
let IT be BinComp of G;
attr IT is associative means :Def7: :: ALTCAT_1:def 7
for i, j, k, l being Element of I
for f, g, h being set st f in G . i,j & g in G . j,k & 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;
attr IT is with_right_units means :Def8: :: ALTCAT_1:def 8
for i being Element of I ex e being set st
( e in G . i,i & ( for j being Element of I
for f being set st f in G . i,j holds
(IT . i,i,j) . f,e = f ) );
attr IT is with_left_units means :Def9: :: ALTCAT_1:def 9
for j being Element of I ex e being set st
( e in G . j,j & ( 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 Def7 defines associative 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 associative iff for i, j, k, l being Element of I
for f, g, h being set st f in G . i,j & g in G . j,k & 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 Def8 defines with_right_units ALTCAT_1:def 8 :
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 & ( 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 Def9 defines with_left_units ALTCAT_1:def 9 :
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 & ( for i being Element of I
for f being set st f in G . i,j holds
(IT . i,j,j) . e,f = f ) ) );

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

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

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

:: deftheorem Def10 defines * ALTCAT_1:def 10 :
for C being non empty AltCatStr
for o1, o2, o3 being object of C st <^o1,o2^> <> {} & <^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;
attr IT is compositional means :Def11: :: ALTCAT_1:def 11
for x being set st x in dom IT holds
ex f, g being Function st
( x = [g,f] & IT . x = g * f );
end;

:: deftheorem Def11 defines compositional ALTCAT_1:def 11 :
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] & IT . x = g * f ) );

registration
let A, B be functional set ;
cluster compositional ManySortedSet of [:A,B:];
existence
ex b1 being ManySortedFunction of [:A,B:] st b1 is compositional
proof end;
end;

theorem Th13: :: ALTCAT_1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B being functional set
for F being compositional ManySortedSet of [:A,B:]
for g, f being Function st g in A & f in B holds
F . g,f = g * f
proof end;

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

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

theorem Th14: :: ALTCAT_1:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B, C being set holds rng (FuncComp (Funcs A,B),(Funcs B,C)) c= Funcs A,C
proof end;

theorem Th15: :: ALTCAT_1:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for o being set holds FuncComp {(id o)},{(id o)} = (id o),(id o) :-> (id o)
proof end;

theorem Th16: :: ALTCAT_1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:]
proof end;

definition
let C be non empty AltCatStr ;
attr C is quasi-functional means :Def13: :: ALTCAT_1:def 13
for a1, a2 being object of C holds <^a1,a2^> c= Funcs a1,a2;
attr C is semi-functional means :Def14: :: ALTCAT_1:def 14
for a1, a2, a3 being object of C st <^a1,a2^> <> {} & <^a2,a3^> <> {} & <^a1,a3^> <> {} holds
for f being Morphism of a1,a2
for g being Morphism of a2,a3
for f', g' being Function st f = f' & g = g' holds
g * f = g' * f';
attr C is pseudo-functional means :Def15: :: ALTCAT_1:def 15
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 Def13 defines quasi-functional ALTCAT_1:def 13 :
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 Def14 defines semi-functional ALTCAT_1:def 14 :
for C being non empty AltCatStr holds
( C is semi-functional iff for a1, a2, a3 being object of C st <^a1,a2^> <> {} & <^a2,a3^> <> {} & <^a1,a3^> <> {} holds
for f being Morphism of a1,a2
for g being Morphism of a2,a3
for f', g' being Function st f = f' & g = g' holds
g * f = g' * f' );

:: deftheorem Def15 defines pseudo-functional ALTCAT_1:def 15 :
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
by STRUCT_0:def 1;
end;

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

theorem :: ALTCAT_1:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th18: :: ALTCAT_1:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty pseudo-functional AltCatStr
for a1, a2, a3 being object of C st <^a1,a2^> <> {} & <^a2,a3^> <> {} & <^a1,a3^> <> {} holds
for f being Morphism of a1,a2
for g being Morphism of a2,a3
for f', g' being Function st f = f' & g = g' holds
g * f = g' * f'
proof end;

definition
let A be non empty set ;
func EnsCat A -> non empty strict pseudo-functional AltCatStr means :Def16: :: ALTCAT_1:def 16
( the carrier of it = A & ( 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 & ( for a1, a2 being object of b1 holds <^a1,a2^> = Funcs a1,a2 ) )
proof end;
uniqueness
for b1, b2 being non empty strict pseudo-functional AltCatStr st the carrier of b1 = A & ( for a1, a2 being object of b1 holds <^a1,a2^> = Funcs a1,a2 ) & the carrier of b2 = A & ( for a1, a2 being object of b2 holds <^a1,a2^> = Funcs a1,a2 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def16 defines EnsCat ALTCAT_1:def 16 :
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 & ( for a1, a2 being object of b2 holds <^a1,a2^> = Funcs a1,a2 ) ) );

definition
let C be non empty AltCatStr ;
attr C is associative means :Def17: :: ALTCAT_1:def 17
the Comp of C is associative;
attr C is with_units means :Def18: :: ALTCAT_1:def 18
( the Comp of C is with_left_units & the Comp of C is with_right_units );
end;

:: deftheorem Def17 defines associative ALTCAT_1:def 17 :
for C being non empty AltCatStr holds
( C is associative iff the Comp of C is associative );

:: deftheorem Def18 defines with_units ALTCAT_1:def 18 :
for C being non empty AltCatStr holds
( C is with_units iff ( the Comp of C is with_left_units & the Comp of C is with_right_units ) );

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

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

theorem :: ALTCAT_1:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: ALTCAT_1:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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^>:] & rng (the Comp of C . a1,a2,a3) c= <^a1,a3^> )
proof end;

theorem Th21: :: ALTCAT_1:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty with_units AltCatStr
for o being object of C holds <^o,o^> <> {}
proof end;

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

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

definition
mode category is non empty transitive associative with_units AltCatStr ;
end;

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

:: deftheorem Def19 defines idm ALTCAT_1:def 19 :
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 o' being object of C st <^o,o'^> <> {} holds
for a being Morphism of o,o' holds a * b3 = a );

theorem :: ALTCAT_1:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th23: :: ALTCAT_1:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty with_units AltCatStr
for o being object of C holds idm o in <^o,o^>
proof end;

theorem :: ALTCAT_1:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: ALTCAT_1:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty transitive associative AltCatStr
for o1, o2, o3, o4 being object of C st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^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
proof end;

definition
let C be AltCatStr ;
attr C is quasi-discrete means :Def20: :: ALTCAT_1:def 20
for i, j being object of C st <^i,j^> <> {} holds
i = j;
attr C is pseudo-discrete means :Def21: :: ALTCAT_1:def 21
for i being object of C holds <^i,i^> is trivial;
end;

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

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

theorem :: ALTCAT_1:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)} )
proof end;

registration
cluster non empty trivial -> quasi-discrete AltCatStr ;
coherence
for b1 being AltCatStr st b1 is trivial & not b1 is empty holds
b1 is quasi-discrete
proof end;
end;

theorem Th27: :: ALTCAT_1:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
( EnsCat 1 is pseudo-discrete & EnsCat 1 is trivial )
proof end;

registration
cluster trivial strict quasi-discrete pseudo-discrete AltCatStr ;
existence
ex b1 being category st
( b1 is pseudo-discrete & b1 is trivial & b1 is strict )
by Th27;
end;

registration
cluster trivial strict quasi-discrete pseudo-discrete AltCatStr ;
existence
ex b1 being category st
( b1 is quasi-discrete & b1 is pseudo-discrete & b1 is trivial & b1 is strict )
proof end;
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 :Def22: :: ALTCAT_1:def 22
( the carrier of it = A & ( 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 & ( for i being object of b1 holds <^i,i^> = {(id i)} ) )
proof end;
correctness
uniqueness
for b1, b2 being non empty strict quasi-discrete AltCatStr st the carrier of b1 = A & ( for i being object of b1 holds <^i,i^> = {(id i)} ) & the carrier of b2 = A & ( for i being object of b2 holds <^i,i^> = {(id i)} ) holds
b1 = b2
;
proof end;
end;

:: deftheorem Def22 defines DiscrCat ALTCAT_1:def 22 :
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 & ( for i being object of b2 holds <^i,i^> = {(id i)} ) ) );

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

theorem Th28: :: ALTCAT_1:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 = {}
proof end;

theorem Th29: :: ALTCAT_1:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

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