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

scheme :: YELLOW18:sch 1
AltCatStrLambda{ F1() -> non empty set , F2( set , set ) -> set , F3( set , set , set , set , set ) -> set } :
ex C being non empty transitive strict AltCatStr st
( the carrier of C = F1() & ( for a, b being object of C holds <^a,b^> = F2(a,b) ) & ( for a, b, c being object of C st <^a,b^> <> {} & <^b,c^> <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c holds g * f = F3(a,b,c,f,g) ) )
provided
A1: for a, b, c being Element of F1()
for f, g being set st f in F2(a,b) & g in F2(b,c) holds
F3(a,b,c,f,g) in F2(a,c)
proof end;

scheme :: YELLOW18:sch 2
CatAssocSch{ F1() -> non empty transitive AltCatStr , F2( set , set , set , set , set ) -> set } :
F1() is associative
provided
A1: for a, b, c being object of F1() st <^a,b^> <> {} & <^b,c^> <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c holds g * f = F2(a,b,c,f,g) and
A2: for a, b, c, d being object of F1()
for f, g, h being set st f in <^a,b^> & g in <^b,c^> & h in <^c,d^> holds
F2(a,c,d,F2(a,b,c,f,g),h) = F2(a,b,d,f,F2(b,c,d,g,h))
proof end;

scheme :: YELLOW18:sch 3
CatUnitsSch{ F1() -> non empty transitive AltCatStr , F2( set , set , set , set , set ) -> set } :
F1() is with_units
provided
A1: for a, b, c being object of F1() st <^a,b^> <> {} & <^b,c^> <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c holds g * f = F2(a,b,c,f,g) and
A2: for a being object of F1() ex f being set st
( f in <^a,a^> & ( for b being object of F1()
for g being set st g in <^a,b^> holds
F2(a,a,b,f,g) = g ) ) and
A3: for a being object of F1() ex f being set st
( f in <^a,a^> & ( for b being object of F1()
for g being set st g in <^b,a^> holds
F2(b,a,a,g,f) = g ) )
proof end;

scheme :: YELLOW18:sch 4
CategoryLambda{ F1() -> non empty set , F2( set , set ) -> set , F3( set , set , set , set , set ) -> set } :
ex C being strict category st
( the carrier of C = F1() & ( for a, b being object of C holds <^a,b^> = F2(a,b) ) & ( for a, b, c being object of C st <^a,b^> <> {} & <^b,c^> <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c holds g * f = F3(a,b,c,f,g) ) )
provided
A1: for a, b, c being Element of F1()
for f, g being set st f in F2(a,b) & g in F2(b,c) holds
F3(a,b,c,f,g) in F2(a,c) and
A2: for a, b, c, d being Element of F1()
for f, g, h being set st f in F2(a,b) & g in F2(b,c) & h in F2(c,d) holds
F3(a,c,d,F3(a,b,c,f,g),h) = F3(a,b,d,f,F3(b,c,d,g,h)) and
A3: for a being Element of F1() ex f being set st
( f in F2(a,a) & ( for b being Element of F1()
for g being set st g in F2(a,b) holds
F3(a,a,b,f,g) = g ) ) and
A4: for a being Element of F1() ex f being set st
( f in F2(a,a) & ( for b being Element of F1()
for g being set st g in F2(b,a) holds
F3(b,a,a,g,f) = g ) )
proof end;

scheme :: YELLOW18:sch 5
CategoryLambdaUniq{ F1() -> non empty set , F2( set , set ) -> set , F3( set , set , set , set , set ) -> set } :
for C1, C2 being non empty transitive AltCatStr st the carrier of C1 = F1() & ( for a, b being object of C1 holds <^a,b^> = F2(a,b) ) & ( for a, b, c being object of C1 st <^a,b^> <> {} & <^b,c^> <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c holds g * f = F3(a,b,c,f,g) ) & the carrier of C2 = F1() & ( for a, b being object of C2 holds <^a,b^> = F2(a,b) ) & ( for a, b, c being object of C2 st <^a,b^> <> {} & <^b,c^> <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c holds g * f = F3(a,b,c,f,g) ) holds
AltCatStr(# the carrier of C1,the Arrows of C1,the Comp of C1 #) = AltCatStr(# the carrier of C2,the Arrows of C2,the Comp of C2 #)
proof end;

scheme :: YELLOW18:sch 6
CategoryQuasiLambda{ F1() -> non empty set , P1[ set , set , set ], F2( set , set ) -> set , F3( set , set , set , set , set ) -> set } :
ex C being strict category st
( the carrier of C = F1() & ( for a, b being object of C
for f being set holds
( f in <^a,b^> iff ( f in F2(a,b) & P1[a,b,f] ) ) ) & ( for a, b, c being object of C st <^a,b^> <> {} & <^b,c^> <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c holds g * f = F3(a,b,c,f,g) ) )
provided
A1: for a, b, c being Element of F1()
for f, g being set st f in F2(a,b) & P1[a,b,f] & g in F2(b,c) & P1[b,c,g] holds
( F3(a,b,c,f,g) in F2(a,c) & P1[a,c,F3(a,b,c,f,g)] ) and
A2: for a, b, c, d being Element of F1()
for f, g, h being set st f in F2(a,b) & P1[a,b,f] & g in F2(b,c) & P1[b,c,g] & h in F2(c,d) & P1[c,d,h] holds
F3(a,c,d,F3(a,b,c,f,g),h) = F3(a,b,d,f,F3(b,c,d,g,h)) and
A3: for a being Element of F1() ex f being set st
( f in F2(a,a) & P1[a,a,f] & ( for b being Element of F1()
for g being set st g in F2(a,b) & P1[a,b,g] holds
F3(a,a,b,f,g) = g ) ) and
A4: for a being Element of F1() ex f being set st
( f in F2(a,a) & P1[a,a,f] & ( for b being Element of F1()
for g being set st g in F2(b,a) & P1[b,a,g] holds
F3(b,a,a,g,f) = g ) )
proof end;

registration
let f be Function-yielding Function;
let a, b, c be set ;
cluster f . a,b,c -> Relation-like Function-like ;
coherence
( f . a,b,c is Relation-like & f . a,b,c is Function-like )
proof end;
end;

scheme :: YELLOW18:sch 7
SubcategoryEx{ F1() -> category, P1[ set ], P2[ set , set , set ] } :
ex B being non empty strict subcategory of F1() st
( ( for a being object of F1() holds
( a is object of B iff P1[a] ) ) & ( for a, b being object of F1()
for a', b' being object of B st a' = a & b' = b & <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a',b'^> iff P2[a,b,f] ) ) )
provided
A1: ex a being object of F1() st P1[a] and
A2: for a, b, c being object of F1() st P1[a] & P1[b] & P1[c] & <^a,b^> <> {} & <^b,c^> <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c st P2[a,b,f] & P2[b,c,g] holds
P2[a,c,g * f] and
A3: for a being object of F1() st P1[a] holds
P2[a,a, idm a]
proof end;

scheme :: YELLOW18:sch 8
CovariantFunctorLambda{ F1() -> category, F2() -> category, F3( set ) -> set , F4( set , set , set ) -> set } :
ex F being strict covariant Functor of F1(),F2() st
( ( for a being object of F1() holds F . a = F3(a) ) & ( for a, b being object of F1() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . f = F4(a,b,f) ) )
provided
A1: for a being object of F1() holds F3(a) is object of F2() and
A2: for a, b being object of F1() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F4(a,b,f) in the Arrows of F2() . F3(a),F3(b) and
A3: for a, b, c being object of F1() st <^a,b^> <> {} & <^b,c^> <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c
for a', b', c' being object of F2() st a' = F3(a) & b' = F3(b) & c' = F3(c) holds
for f' being Morphism of a',b'
for g' being Morphism of b',c' st f' = F4(a,b,f) & g' = F4(b,c,g) holds
F4(a,c,(g * f)) = g' * f' and
A4: for a being object of F1()
for a' being object of F2() st a' = F3(a) holds
F4(a,a,(idm a)) = idm a'
proof end;

theorem Th1: :: YELLOW18:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B being category
for F, G being covariant Functor of A,B st ( for a being object of A holds F . a = G . a ) & ( for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . f = G . f ) holds
FunctorStr(# the ObjectMap of F,the MorphMap of F #) = FunctorStr(# the ObjectMap of G,the MorphMap of G #)
proof end;

scheme :: YELLOW18:sch 9
ContravariantFunctorLambda{ F1() -> category, F2() -> category, F3( set ) -> set , F4( set , set , set ) -> set } :
ex F being strict contravariant Functor of F1(),F2() st
( ( for a being object of F1() holds F . a = F3(a) ) & ( for a, b being object of F1() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . f = F4(a,b,f) ) )
provided
A1: for a being object of F1() holds F3(a) is object of F2() and
A2: for a, b being object of F1() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F4(a,b,f) in the Arrows of F2() . F3(b),F3(a) and
A3: for a, b, c being object of F1() st <^a,b^> <> {} & <^b,c^> <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c
for a', b', c' being object of F2() st a' = F3(a) & b' = F3(b) & c' = F3(c) holds
for f' being Morphism of b',a'
for g' being Morphism of c',b' st f' = F4(a,b,f) & g' = F4(b,c,g) holds
F4(a,c,(g * f)) = f' * g' and
A4: for a being object of F1()
for a' being object of F2() st a' = F3(a) holds
F4(a,a,(idm a)) = idm a'
proof end;

theorem Th2: :: YELLOW18:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B being category
for F, G being contravariant Functor of A,B st ( for a being object of A holds F . a = G . a ) & ( for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . f = G . f ) holds
FunctorStr(# the ObjectMap of F,the MorphMap of F #) = FunctorStr(# the ObjectMap of G,the MorphMap of G #)
proof end;

definition
let A, B, C be non empty set ;
let f be Function of [:A,B:],C;
:: original: one-to-one
redefine attr f is one-to-one means :: YELLOW18:def 1
for a1, a2 being Element of A
for b1, b2 being Element of B st f . a1,b1 = f . a2,b2 holds
( a1 = a2 & b1 = b2 );
compatibility
( f is one-to-one iff for a1, a2 being Element of A
for b1, b2 being Element of B st f . a1,b1 = f . a2,b2 holds
( a1 = a2 & b1 = b2 ) )
proof end;
end;

:: deftheorem defines one-to-one YELLOW18:def 1 :
for A, B, C being non empty set
for f being Function of [:A,B:],C holds
( f is one-to-one iff for a1, a2 being Element of A
for b1, b2 being Element of B st f . a1,b1 = f . a2,b2 holds
( a1 = a2 & b1 = b2 ) );

scheme :: YELLOW18:sch 10
CoBijectiveSch{ F1() -> category, F2() -> category, F3() -> covariant Functor of F1(),F2(), F4( set ) -> set , F5( set , set , set ) -> set } :
F3() is bijective
provided
A1: for a being object of F1() holds F3() . a = F4(a) and
A2: for a, b being object of F1() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F3() . f = F5(a,b,f) and
A3: for a, b being object of F1() st F4(a) = F4(b) holds
a = b and
A4: for a, b being object of F1() st <^a,b^> <> {} holds
for f, g being Morphism of a,b st F5(a,b,f) = F5(a,b,g) holds
f = g and
A5: for a, b being object of F2() st <^a,b^> <> {} holds
for f being Morphism of a,b ex c, d being object of F1() ex g being Morphism of c,d st
( a = F4(c) & b = F4(d) & <^c,d^> <> {} & f = F5(c,d,g) )
proof end;

scheme :: YELLOW18:sch 11
CatIsomorphism{ F1() -> category, F2() -> category, F3( set ) -> set , F4( set , set , set ) -> set } :
F1(),F2() are_isomorphic
provided
A1: ex F being covariant Functor of F1(),F2() st
( ( for a being object of F1() holds F . a = F3(a) ) & ( for a, b being object of F1() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . f = F4(a,b,f) ) ) and
A2: for a, b being object of F1() st F3(a) = F3(b) holds
a = b and
A3: for a, b being object of F1() st <^a,b^> <> {} holds
for f, g being Morphism of a,b st F4(a,b,f) = F4(a,b,g) holds
f = g and
A4: for a, b being object of F2() st <^a,b^> <> {} holds
for f being Morphism of a,b ex c, d being object of F1() ex g being Morphism of c,d st
( a = F3(c) & b = F3(d) & <^c,d^> <> {} & f = F4(c,d,g) )
proof end;

scheme :: YELLOW18:sch 12
ContraBijectiveSch{ F1() -> category, F2() -> category, F3() -> contravariant Functor of F1(),F2(), F4( set ) -> set , F5( set , set , set ) -> set } :
F3() is bijective
provided
A1: for a being object of F1() holds F3() . a = F4(a) and
A2: for a, b being object of F1() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F3() . f = F5(a,b,f) and
A3: for a, b being object of F1() st F4(a) = F4(b) holds
a = b and
A4: for a, b being object of F1() st <^a,b^> <> {} holds
for f, g being Morphism of a,b st F5(a,b,f) = F5(a,b,g) holds
f = g and
A5: for a, b being object of F2() st <^a,b^> <> {} holds
for f being Morphism of a,b ex c, d being object of F1() ex g being Morphism of c,d st
( b = F4(c) & a = F4(d) & <^c,d^> <> {} & f = F5(c,d,g) )
proof end;

scheme :: YELLOW18:sch 13
CatAntiIsomorphism{ F1() -> category, F2() -> category, F3( set ) -> set , F4( set , set , set ) -> set } :
F1(),F2() are_anti-isomorphic
provided
A1: ex F being contravariant Functor of F1(),F2() st
( ( for a being object of F1() holds F . a = F3(a) ) & ( for a, b being object of F1() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . f = F4(a,b,f) ) ) and
A2: for a, b being object of F1() st F3(a) = F3(b) holds
a = b and
A3: for a, b being object of F1() st <^a,b^> <> {} holds
for f, g being Morphism of a,b st F4(a,b,f) = F4(a,b,g) holds
f = g and
A4: for a, b being object of F2() st <^a,b^> <> {} holds
for f being Morphism of a,b ex c, d being object of F1() ex g being Morphism of c,d st
( b = F3(c) & a = F3(d) & <^c,d^> <> {} & f = F4(c,d,g) )
proof end;

definition
let A, B be category;
pred A,B are_equivalent means :: YELLOW18:def 2
 ex F being covariant Functor of A,B ex G being covariant Functor of B,A st
( G * F, id A are_naturally_equivalent & F * G, id B are_naturally_equivalent );
reflexivity
for A being category ex F, G being covariant Functor of A,A st
( G * F, id A are_naturally_equivalent & F * G, id A are_naturally_equivalent )
proof end;
symmetry
for A, B being category st ex F being covariant Functor of A,B ex G being covariant Functor of B,A st
( G * F, id A are_naturally_equivalent & F * G, id B are_naturally_equivalent ) holds
ex F being covariant Functor of B,A ex G being covariant Functor of A,B st
( G * F, id B are_naturally_equivalent & F * G, id A are_naturally_equivalent ) ;
end;

:: deftheorem defines are_equivalent YELLOW18:def 2 :
for A, B being category holds
( A,B are_equivalent iff ex F being covariant Functor of A,B ex G being covariant Functor of B,A st
( G * F, id A are_naturally_equivalent & F * G, id B are_naturally_equivalent ) );

theorem Th3: :: YELLOW18:3  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 non empty reflexive AltGraph
for F1, F2 being feasible FunctorStr of A,B
for G1, G2 being FunctorStr of B,C st FunctorStr(# the ObjectMap of F1,the MorphMap of F1 #) = FunctorStr(# the ObjectMap of F2,the MorphMap of F2 #) & FunctorStr(# the ObjectMap of G1,the MorphMap of G1 #) = FunctorStr(# the ObjectMap of G2,the MorphMap of G2 #) holds
G1 * F1 = G2 * F2
proof end;

theorem Th4: :: YELLOW18: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 category st A,B are_equivalent & B,C are_equivalent holds
A,C are_equivalent
proof end;

theorem Th5: :: YELLOW18:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B being category st A,B are_isomorphic holds
A,B are_equivalent
proof end;

scheme :: YELLOW18:sch 14
NatTransLambda{ F1() -> category, F2() -> category, F3() -> covariant Functor of F1(),F2(), F4() -> covariant Functor of F1(),F2(), F5( set ) -> set } :
ex t being natural_transformation of F3(),F4() st
( F3() is_naturally_transformable_to F4() & ( for a being object of F1() holds t ! a = F5(a) ) )
provided
A1: for a being object of F1() holds F5(a) in <^(F3() . a),(F4() . a)^> and
A2: for a, b being object of F1() st <^a,b^> <> {} holds
for f being Morphism of a,b
for g1 being Morphism of (F3() . a),(F4() . a) st g1 = F5(a) holds
for g2 being Morphism of (F3() . b),(F4() . b) st g2 = F5(b) holds
g2 * (F3() . f) = (F4() . f) * g1
proof end;

scheme :: YELLOW18:sch 15
NatEquivalenceLambda{ F1() -> category, F2() -> category, F3() -> covariant Functor of F1(),F2(), F4() -> covariant Functor of F1(),F2(), F5( set ) -> set } :
ex t being natural_equivalence of F3(),F4() st
( F3(),F4() are_naturally_equivalent & ( for a being object of F1() holds t ! a = F5(a) ) )
provided
A1: for a being object of F1() holds
( F5(a) in <^(F3() . a),(F4() . a)^> & <^(F4() . a),(F3() . a)^> <> {} & ( for f being Morphism of (F3() . a),(F4() . a) st f = F5(a) holds
f is iso ) ) and
A2: for a, b being object of F1() st <^a,b^> <> {} holds
for f being Morphism of a,b
for g1 being Morphism of (F3() . a),(F4() . a) st g1 = F5(a) holds
for g2 being Morphism of (F3() . b),(F4() . b) st g2 = F5(b) holds
g2 * (F3() . f) = (F4() . f) * g1
proof end;

definition
let C1, C2 be non empty AltCatStr ;
pred C1,C2 are_opposite means :Def3: :: YELLOW18:def 3
( the carrier of C2 = the carrier of C1 & the Arrows of C2 = ~ the Arrows of C1 & ( for a, b, c being object of C1
for a', b', c' being object of C2 st a' = a & b' = b & c' = c holds
the Comp of C2 . a',b',c' = ~ (the Comp of C1 . c,b,a) ) );
symmetry
for C1, C2 being non empty AltCatStr st the carrier of C2 = the carrier of C1 & the Arrows of C2 = ~ the Arrows of C1 & ( for a, b, c being object of C1
for a', b', c' being object of C2 st a' = a & b' = b & c' = c holds
the Comp of C2 . a',b',c' = ~ (the Comp of C1 . c,b,a) ) holds
( the carrier of C1 = the carrier of C2 & the Arrows of C1 = ~ the Arrows of C2 & ( for a, b, c being object of C2
for a', b', c' being object of C1 st a' = a & b' = b & c' = c holds
the Comp of C1 . a',b',c' = ~ (the Comp of C2 . c,b,a) ) )
proof end;
end;

:: deftheorem Def3 defines are_opposite YELLOW18:def 3 :
for C1, C2 being non empty AltCatStr holds
( C1,C2 are_opposite iff ( the carrier of C2 = the carrier of C1 & the Arrows of C2 = ~ the Arrows of C1 & ( for a, b, c being object of C1
for a', b', c' being object of C2 st a' = a & b' = b & c' = c holds
the Comp of C2 . a',b',c' = ~ (the Comp of C1 . c,b,a) ) ) );

theorem Th6: :: YELLOW18:6  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 AltCatStr st A,B are_opposite holds
for a being object of A holds a is object of B
proof end;

theorem Th7: :: YELLOW18: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 non empty AltCatStr st A,B are_opposite holds
for a, b being object of A
for a', b' being object of B st a' = a & b' = b holds
<^a,b^> = <^b',a'^>
proof end;

theorem :: YELLOW18: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 non empty AltCatStr st A,B are_opposite holds
for a, b being object of A
for a', b' being object of B st a' = a & b' = b holds
for f being Morphism of a,b holds f is Morphism of b',a' by Th7;

theorem Th9: :: YELLOW18:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C1, C2 being non empty transitive AltCatStr holds
( C1,C2 are_opposite iff ( the carrier of C2 = the carrier of C1 & ( for a, b, c being object of C1
for a', b', c' being object of C2 st a' = a & b' = b & c' = c holds
( <^a,b^> = <^b',a'^> & ( <^a,b^> <> {} & <^b,c^> <> {} implies for f being Morphism of a,b
for g being Morphism of b,c
for f' being Morphism of b',a'
for g' being Morphism of c',b' st f' = f & g' = g holds
f' * g' = g * f ) ) ) ) )
proof end;

theorem Th10: :: YELLOW18:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B being category st A,B are_opposite holds
for a being object of A
for b being object of B st a = b holds
idm a = idm b
proof end;

theorem Th11: :: YELLOW18:11  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 ex C' being non empty transitive strict AltCatStr st C,C' are_opposite
proof end;

theorem Th12: :: YELLOW18:12  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 transitive AltCatStr st A,B are_opposite & A is associative holds
B is associative
proof end;

theorem Th13: :: YELLOW18: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 non empty transitive AltCatStr st A,B are_opposite & A is with_units holds
B is with_units
proof end;

theorem Th14: :: YELLOW18:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, C1, C2 being non empty AltCatStr st C,C1 are_opposite holds
( C,C2 are_opposite iff AltCatStr(# the carrier of C1,the Arrows of C1,the Comp of C1 #) = AltCatStr(# the carrier of C2,the Arrows of C2,the Comp of C2 #) )
proof end;

definition
let C be non empty transitive AltCatStr ;
func C opp -> non empty transitive strict AltCatStr means :Def4: :: YELLOW18:def 4
C,it are_opposite ;
uniqueness
for b1, b2 being non empty transitive strict AltCatStr st C,b1 are_opposite & C,b2 are_opposite holds
b1 = b2 by Th14;
existence
ex b1 being non empty transitive strict AltCatStr st C,b1 are_opposite by Th11;
end;

:: deftheorem Def4 defines opp YELLOW18:def 4 :
for C being non empty transitive AltCatStr
for b2 being non empty transitive strict AltCatStr holds
( b2 = C opp iff C,b2 are_opposite );

registration
let C be non empty transitive associative AltCatStr ;
cluster C opp -> non empty transitive strict associative ;
coherence
C opp is associative
proof end;
end;

registration
let C be non empty transitive with_units AltCatStr ;
cluster C opp -> non empty transitive strict with_units ;
coherence
C opp is with_units
proof end;
end;

definition
let A, B be category;
assume A1: A,B are_opposite ;
deffunc H1( set ) -> set = $1;
deffunc H2( set , set , set ) -> set = $3;
A2: for a being object of A holds H1(a) is object of B by A1, Def3;
A3: now
let a, b be object of A; :: thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b holds H2(a,b,f) in the Arrows of B . H1(b),H1(a) )
assume A4: <^a,b^> <> {} ; :: thesis: for f being Morphism of a,b holds H2(a,b,f) in the Arrows of B . H1(b),H1(a)
let f be Morphism of a,b; :: thesis: H2(a,b,f) in the Arrows of B . H1(b),H1(a)
reconsider a' = a, b' = b as object of B by A1, Def3;
<^a,b^> = <^b',a'^> by A1, Th9
.= the Arrows of B . b,a ;
hence H2(a,b,f) in the Arrows of B . H1(b),H1(a) by A4; :: thesis: verum
end;
A5: for a, b, c being object of A st <^a,b^> <> {} & <^b,c^> <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c
for a', b', c' being object of B st a' = H1(a) & b' = H1(b) & c' = H1(c) holds
for f' being Morphism of b',a'
for g' being Morphism of c',b' st f' = H2(a,b,f) & g' = H2(b,c,g) holds
H2(a,c,g * f) = f' * g' by A1, Th9;
A6: for a being object of A
for a' being object of B st a' = H1(a) holds
H2(a,a, idm a) = idm a' by A1, Th10;
func dualizing-func A,B -> strict contravariant Functor of A,B means :Def5: :: YELLOW18:def 5
( ( for a being object of A holds it . a = a ) & ( for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds it . f = f ) );
existence
ex b1 being strict contravariant Functor of A,B st
( ( for a being object of A holds b1 . a = a ) & ( for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds b1 . f = f ) )
proof end;
uniqueness
for b1, b2 being strict contravariant Functor of A,B st ( for a being object of A holds b1 . a = a ) & ( for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds b1 . f = f ) & ( for a being object of A holds b2 . a = a ) & ( for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds b2 . f = f ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines dualizing-func YELLOW18:def 5 :
for A, B being category st A,B are_opposite holds
for b3 being strict contravariant Functor of A,B holds
( b3 = dualizing-func A,B iff ( ( for a being object of A holds b3 . a = a ) & ( for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds b3 . f = f ) ) );

theorem Th15: :: YELLOW18:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B being category st A,B are_opposite holds
(dualizing-func A,B) * (dualizing-func B,A) = id B
proof end;

theorem Th16: :: YELLOW18: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 category st A,B are_opposite holds
dualizing-func A,B is bijective
proof end;

registration
let A be category;
cluster dualizing-func A,(A opp ) -> strict contravariant bijective ;
coherence
dualizing-func A,(A opp ) is bijective
proof end;
cluster dualizing-func (A opp ),A -> strict contravariant bijective ;
coherence
dualizing-func (A opp ),A is bijective
proof end;
end;

theorem :: YELLOW18:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B being category st A,B are_opposite holds
A,B are_anti-isomorphic
proof end;

theorem Th18: :: YELLOW18:18  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 category st A,B are_opposite holds
( A,C are_isomorphic iff B,C are_anti-isomorphic )
proof end;

theorem :: YELLOW18:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B, C, D being category st A,B are_opposite & C,D are_opposite & A,C are_isomorphic holds
B,D are_isomorphic
proof end;

theorem :: YELLOW18:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B, C, D being category st A,B are_opposite & C,D are_opposite & A,C are_anti-isomorphic holds
B,D are_anti-isomorphic
proof end;

Lm1: now
let A, B be category; :: thesis: ( A,B are_opposite implies for a, b being object of A st <^a,b^> <> {} & <^b,a^> <> {} holds
for a', b' being object of B st a' = a & b' = b holds
for f being Morphism of a,b
for f' being Morphism of b',a' st f' = f holds
( ( f is retraction implies f' is coretraction ) & ( f is coretraction implies f' is retraction ) ) )
assume A1: A,B are_opposite ; :: thesis: for a, b being object of A st <^a,b^> <> {} & <^b,a^> <> {} holds
for a', b' being object of B st a' = a & b' = b holds
for f being Morphism of a,b
for f' being Morphism of b',a' st f' = f holds
( ( f is retraction implies f' is coretraction ) & ( f is coretraction implies f' is retraction ) )
let a, b be object of A; :: thesis: ( <^a,b^> <> {} & <^b,a^> <> {} implies for a', b' being object of B st a' = a & b' = b holds
for f being Morphism of a,b
for f' being Morphism of b',a' st f' = f holds
( ( f is retraction implies f' is coretraction ) & ( f is coretraction implies f' is retraction ) ) )
assume A2: ( <^a,b^> <> {} & <^b,a^> <> {} ) ; :: thesis: for a', b' being object of B st a' = a & b' = b holds
for f being Morphism of a,b
for f' being Morphism of b',a' st f' = f holds
( ( f is retraction implies f' is coretraction ) & ( f is coretraction implies f' is retraction ) )
let a', b' be object of B; :: thesis: ( a' = a & b' = b implies for f being Morphism of a,b
for f' being Morphism of b',a' st f' = f holds
( ( f is retraction implies f' is coretraction ) & ( f is coretraction implies f' is retraction ) ) )
assume A3: ( a' = a & b' = b ) ; :: thesis: for f being Morphism of a,b
for f' being Morphism of b',a' st f' = f holds
( ( f is retraction implies f' is coretraction ) & ( f is coretraction implies f' is retraction ) )
let f be Morphism of a,b; :: thesis: for f' being Morphism of b',a' st f' = f holds
( ( f is retraction implies f' is coretraction ) & ( f is coretraction implies f' is retraction ) )
let f' be Morphism of b',a'; :: thesis: ( f' = f implies ( ( f is retraction implies f' is coretraction ) & ( f is coretraction implies f' is retraction ) ) )
assume A4: f' = f ; :: thesis: ( ( f is retraction implies f' is coretraction ) & ( f is coretraction implies f' is retraction ) )
thus ( f is retraction implies f' is coretraction ) :: thesis: ( f is coretraction implies f' is retraction )
proof
given g being Morphism of b,a such that A5: g is_right_inverse_of f ; :: according to ALTCAT_3:def 2 :: thesis: f' is coretraction
reconsider g' = g as Morphism of a',b' by A1, A3, Th7;
take g' ; :: according to ALTCAT_3:def 3 :: thesis: g' is_left_inverse_of f'
f * g = idm b by A5, ALTCAT_3:def 1
.= idm b' by A1, A3, Th10 ;
hence g' * f' = idm b' by A1, A2, A3, A4, Th9; :: according to ALTCAT_3:def 1 :: thesis: verum
end;
thus ( f is coretraction implies f' is retraction ) :: thesis: verum
proof
given g being Morphism of b,a such that A6: g is_left_inverse_of f ; :: according to ALTCAT_3:def 3 :: thesis: f' is retraction
reconsider g' = g as Morphism of a',b' by A1, A3, Th7;
take g' ; :: according to ALTCAT_3:def 2 :: thesis: f' is_left_inverse_of g'
g * f = idm a by A6, ALTCAT_3:def 1
.= idm a' by A1, A3, Th10 ;
hence f' * g' = idm a' by A1, A2, A3, A4, Th9; :: according to ALTCAT_3:def 1 :: thesis: verum
end;
end;

theorem :: YELLOW18:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B being category st A,B are_opposite holds
for a, b being object of A st <^a,b^> <> {} & <^b,a^> <> {} holds
for a', b' being object of B st a' = a & b' = b holds
for f being Morphism of a,b
for f' being Morphism of b',a' st f' = f holds
( f is retraction iff f' is coretraction )
proof end;

theorem :: YELLOW18:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B being category st A,B are_opposite holds
for a, b being object of A st <^a,b^> <> {} & <^b,a^> <> {} holds
for a', b' being object of B st a' = a & b' = b holds
for f being Morphism of a,b
for f' being Morphism of b',a' st f' = f holds
( f is coretraction iff f' is retraction )
proof end;

theorem Th23: :: YELLOW18:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B being category st A,B are_opposite holds
for a, b being object of A st <^a,b^> <> {} & <^b,a^> <> {} holds
for a', b' being object of B st a' = a & b' = b holds
for f being Morphism of a,b
for f' being Morphism of b',a' st f' = f & f is retraction & f is coretraction holds
f' " = f "
proof end;

theorem Th24: :: YELLOW18:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B being category st A,B are_opposite holds
for a, b being object of A st <^a,b^> <> {} & <^b,a^> <> {} holds
for a', b' being object of B st a' = a & b' = b holds
for f being Morphism of a,b
for f' being Morphism of b',a' st f' = f holds
( f is iso iff f' is iso )
proof end;

theorem Th25: :: YELLOW18:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B, C, D being category st A,B are_opposite & C,D are_opposite holds
for F, G being covariant Functor of B,C st F,G are_naturally_equivalent holds
((dualizing-func C,D) * G) * (dualizing-func A,B),((dualizing-func C,D) * F) * (dualizing-func A,B) are_naturally_equivalent
proof end;

theorem Th26: :: YELLOW18:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B, C, D being category st A,B are_opposite & C,D are_opposite & A,C are_equivalent holds
B,D are_equivalent
proof end;

definition
let A, B be category;
pred A,B are_dual means :Def6: :: YELLOW18:def 6
A,B opp are_equivalent ;
symmetry
for A, B being category st A,B opp are_equivalent holds
B,A opp are_equivalent
proof end;
end;

:: deftheorem Def6 defines are_dual YELLOW18:def 6 :
for A, B being category holds
( A,B are_dual iff A,B opp are_equivalent );

theorem :: YELLOW18:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B being category st A,B are_anti-isomorphic holds
A,B are_dual
proof end;

theorem :: YELLOW18:28  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 category st A,B are_opposite holds
( A,C are_equivalent iff B,C are_dual )
proof end;

theorem :: YELLOW18:29  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 category st A,B are_dual & B,C are_equivalent holds
A,C are_dual
proof end;

theorem :: YELLOW18:30  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 category st A,B are_dual & B,C are_dual holds
A,C are_equivalent
proof end;

theorem Th31: :: YELLOW18:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y, x being set holds
( x in Funcs X,Y iff ( x is Function & proj1 x = X & proj2 x c= Y ) )
proof end;

definition
let C be 1-sorted ;
mode ManySortedSet of C is ManySortedSet of the carrier of C;
end;

definition
let C be category;
attr C is para-functional means :: YELLOW18:def 7
 ex F being ManySortedSet of C st
for a1, a2 being object of C holds <^a1,a2^> c= Funcs (F . a1),(F . a2);
end;

:: deftheorem defines para-functional YELLOW18:def 7 :
for C being category holds
( C is para-functional iff ex F being ManySortedSet of C st
for a1, a2 being object of C holds <^a1,a2^> c= Funcs (F . a1),(F . a2) );

registration
cluster quasi-functional -> para-functional AltCatStr ;
coherence
for b1 being category st b1 is quasi-functional holds
b1 is para-functional
proof end;
end;

definition
let C be category;
let a be set ;
func C -carrier_of a -> set means :Def8: :: YELLOW18:def 8
 ex b being object of C st
( b = a & it = proj1 (idm b) ) if a is object of C
otherwise it = {} ;
consistency
for b1 being set holds verum ;
existence
( ( a is object of C implies ex b1 being set ex b being object of C st
( b = a & b1 = proj1 (idm b) ) ) & ( a is not object of C implies ex b1 being set st b1 = {} ) )
proof end;
uniqueness
for b1, b2 being set holds
( ( a is object of C & ex b being object of C st
( b = a & b1 = proj1 (idm b) ) & ex b being object of C st
( b = a & b2 = proj1 (idm b) ) implies b1 = b2 ) & ( a is not object of C & b1 = {} & b2 = {} implies b1 = b2 ) ) ;
end;

:: deftheorem Def8 defines -carrier_of YELLOW18:def 8 :
for C being category
for a being set
for b3 being set holds
( ( a is object of C implies ( b3 = C -carrier_of a iff ex b being object of C st
( b = a & b3 = proj1 (idm b) ) ) ) & ( a is not object of C implies ( b3 = C -carrier_of a iff b3 = {} ) ) );

notation
let C be category;
let a be object of C;
synonym the_carrier_of a for C -carrier_of a;
end;

definition
let C be category;
let a be object of C;
redefine func C -carrier_of a equals :: YELLOW18:def 9
 proj1 (idm a);
compatibility
for b1 being set holds
( b1 = C -carrier_of a iff b1 = proj1 (idm a) ) by Def8;
end;

:: deftheorem defines -carrier_of YELLOW18:def 9 :
for C being category
for a being object of C holds C -carrier_of a = proj1 (idm a);

theorem Th32: :: YELLOW18:32  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 a being object of (EnsCat A) holds idm a = id a
proof end;

theorem Th33: :: YELLOW18:33  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 a being object of (EnsCat A) holds the_carrier_of a = a
proof end;

definition
let C be category;
attr C is set-id-inheriting means :Def10: :: YELLOW18:def 10
for a being object of C holds idm a = id (the_carrier_of a);
end;

:: deftheorem Def10 defines set-id-inheriting YELLOW18:def 10 :
for C being category holds
( C is set-id-inheriting iff for a being object of C holds idm a = id (the_carrier_of a) );

registration
let A be non empty set ;
cluster EnsCat A -> para-functional set-id-inheriting ;
coherence
EnsCat A is set-id-inheriting
proof end;
end;

definition
let C be category;
attr C is concrete means :Def11: :: YELLOW18:def 11
( C is para-functional & C is semi-functional & C is set-id-inheriting );
end;

:: deftheorem Def11 defines concrete YELLOW18:def 11 :
for C being category holds
( C is concrete iff ( C is para-functional & C is semi-functional & C is set-id-inheriting ) );

registration
cluster concrete -> semi-functional para-functional set-id-inheriting AltCatStr ;
coherence
for b1 being category st b1 is concrete holds
( b1 is para-functional & b1 is semi-functional & b1 is set-id-inheriting ) by Def11;
cluster semi-functional para-functional set-id-inheriting -> concrete AltCatStr ;
coherence
for b1 being category st b1 is para-functional & b1 is semi-functional & b1 is set-id-inheriting holds
b1 is concrete by Def11;
end;

registration
cluster strict quasi-functional semi-functional para-functional set-id-inheriting concrete AltCatStr ;
existence
ex b1 being category st
( b1 is concrete & b1 is quasi-functional & b1 is strict )
proof end;
end;

theorem Th34: :: YELLOW18:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being category holds
( C is para-functional iff for a1, a2 being object of C holds <^a1,a2^> c= Funcs (the_carrier_of a1),(the_carrier_of a2) )
proof end;

theorem Th35: :: YELLOW18:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being para-functional category
for a, b being object of C st <^a,b^> <> {} holds
for f being Morphism of a,b holds f is Function of the_carrier_of a, the_carrier_of b
proof end;

registration
let A be para-functional category;
let a, b be object of A;
cluster -> Relation-like Function-like Element of <^a,b^>;
coherence
for b1 being Morphism of a,b holds
( b1 is Function-like & b1 is Relation-like )
proof end;
end;

theorem Th36: :: YELLOW18:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being para-functional category
for a, b being object of C st <^a,b^> <> {} holds
for f being Morphism of a,b holds
( dom f = the_carrier_of a & rng f c= the_carrier_of b )
proof end;

theorem :: YELLOW18:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being semi-functional para-functional category
for a being object of C holds the_carrier_of a = dom (idm a) by FUNCT_5:21;

theorem Th38: :: YELLOW18:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being semi-functional para-functional category
for a, b, c being object of C st <^a,b^> <> {} & <^b,c^> <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c holds g * f = g * f
proof end;

theorem Th39: :: YELLOW18:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being semi-functional para-functional category
for a being object of C st id (the_carrier_of a) in <^a,a^> holds
idm a = id (the_carrier_of a)
proof end;

scheme :: YELLOW18:sch 16
ConcreteCategoryLambda{ F1() -> non empty set , F2( set , set ) -> set , F3( set ) -> set } :
ex C being strict concrete category st
( the carrier of C = F1() & ( for a being object of C holds the_carrier_of a = F3(a) ) & ( for a, b being object of C holds <^a,b^> = F2(a,b) ) )
provided
A1: for a, b, c being Element of F1()
for f, g being Function st f in F2(a,b) & g in F2(b,c) holds
g * f in F2(a,c) and
A2: for a, b being Element of F1() holds F2(a,b) c= Funcs F3(a),F3(b) and
A3: for a being Element of F1() holds id F3(a) in F2(a,a)
proof end;

scheme :: YELLOW18:sch 17
ConcreteCategoryQuasiLambda{ F1() -> non empty set , P1[ set , set , set ], F2( set ) -> set } :
ex C being strict concrete category st
( the carrier of C = F1() & ( for a being object of C holds the_carrier_of a = F2(a) ) & ( for a, b being Element of F1()
for f being Function holds
( f in the Arrows of C . a,b iff ( f in Funcs F2(a),F2(b) & P1[a,b,f] ) ) ) )
provided
A1: for a, b, c being Element of F1()
for f, g being Function st P1[a,b,f] & P1[b,c,g] holds
P1[a,c,g * f] and
A2: for a being Element of F1() holds P1[a,a, id F2(a)]
proof end;

scheme :: YELLOW18:sch 18
ConcreteCategoryEx{ F1() -> non empty set , F2( set ) -> set , P1[ set , set ], P2[ set , set , set ] } :
ex C being strict concrete category st
( the carrier of C = F1() & ( for a being object of C
for x being set holds
( x in the_carrier_of a iff ( x in F2(a) & P1[a,x] ) ) ) & ( for a, b being Element of F1()
for f being Function holds
( f in the Arrows of C . a,b iff ( f in Funcs (C -carrier_of a),(C -carrier_of b) & P2[a,b,f] ) ) ) )
provided
A1: for a, b, c being Element of F1()
for f, g being Function st P2[a,b,f] & P2[b,c,g] holds
P2[a,c,g * f] and
A2: for a being Element of F1()
for X being set st ( for x being set holds
( x in X iff ( x in F2(a) & P1[a,x] ) ) ) holds
P2[a,a, id X]
proof end;

scheme :: YELLOW18:sch 19
ConcreteCategoryUniq1{ F1() -> non empty set , F2( set , set ) -> set } :
for C1, C2 being semi-functional para-functional category st the carrier of C1 = F1() & ( for a, b being object of C1 holds <^a,b^> = F2(a,b) ) & the carrier of C2 = F1() & ( for a, b being object of C2 holds <^a,b^> = F2(a,b) ) holds
AltCatStr(# the carrier of C1,the Arrows of C1,the Comp of C1 #) = AltCatStr(# the carrier of C2,the Arrows of C2,the Comp of C2 #)
proof end;

scheme :: YELLOW18:sch 20
ConcreteCategoryUniq2{ F1() -> non empty set , P1[ set , set , set ], F2( set ) -> set } :
for C1, C2 being semi-functional para-functional category st the carrier of C1 = F1() & ( for a, b being Element of F1()
for f being Function holds
( f in the Arrows of C1 . a,b iff ( f in Funcs F2(a),F2(b) & P1[a,b,f] ) ) ) & the carrier of C2 = F1() & ( for a, b being Element of F1()
for f being Function holds
( f in the Arrows of C2 . a,b iff ( f in Funcs F2(a),F2(b) & P1[a,b,f] ) ) ) holds
AltCatStr(# the carrier of C1,the Arrows of C1,the Comp of C1 #) = AltCatStr(# the carrier of C2,the Arrows of C2,the Comp of C2 #)
proof end;

scheme :: YELLOW18:sch 21
ConcreteCategoryUniq3{ F1() -> non empty set , F2( set ) -> set , P1[ set , set ], P2[ set , set , set ] } :
for C1, C2 being semi-functional para-functional category st the carrier of C1 = F1() & ( for a being object of C1
for x being set holds
( x in the_carrier_of a iff ( x in F2(a) & P1[a,x] ) ) ) & ( for a, b being Element of F1()
for f being Function holds
( f in the Arrows of C1 . a,b iff ( f in Funcs (C1 -carrier_of a),(C1 -carrier_of b) & P2[a,b,f] ) ) ) & the carrier of C2 = F1() & ( for a being object of C2
for x being set holds
( x in the_carrier_of a iff ( x in F2(a) & P1[a,x] ) ) ) & ( for a, b being Element of F1()
for f being Function holds
( f in the Arrows of C2 . a,b iff ( f in Funcs (C2 -carrier_of a),(C2 -carrier_of b) & P2[a,b,f] ) ) ) holds
AltCatStr(# the carrier of C1,the Arrows of C1,the Comp of C1 #) = AltCatStr(# the carrier of C2,the Arrows of C2,the Comp of C2 #)
proof end;

theorem Th40: :: YELLOW18:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being concrete category
for a, b being object of C st <^a,b^> <> {} & <^b,a^> <> {} holds
for f being Morphism of a,b st f is retraction holds
rng f = the_carrier_of b
proof end;

theorem Th41: :: YELLOW18:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being concrete category
for a, b being object of C st <^a,b^> <> {} & <^b,a^> <> {} holds
for f being Morphism of a,b st f is coretraction holds
f is one-to-one
proof end;

theorem Th42: :: YELLOW18:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being concrete category
for a, b being object of C st <^a,b^> <> {} & <^b,a^> <> {} holds
for f being Morphism of a,b st f is iso holds
( f is one-to-one & rng f = the_carrier_of b )
proof end;

theorem Th43: :: YELLOW18:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being semi-functional para-functional category
for a, b being object of C st <^a,b^> <> {} holds
for f being Morphism of a,b st f is one-to-one & f " in <^b,a^> holds
f is iso
proof end;

theorem :: YELLOW18:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being concrete category
for a, b being object of C st <^a,b^> <> {} & <^b,a^> <> {} holds
for f being Morphism of a,b st f is iso holds
f " = f "
proof end;

scheme :: YELLOW18:sch 22
ConcreteCatEquivalence{ F1() -> semi-functional para-functional category, F2() -> semi-functional para-functional category, F3( set ) -> set , F4( set ) -> set , F5( set , set , set ) -> Function, F6( set , set , set ) -> Function, F7( set ) -> Function, F8( set ) -> Function } :
F1(),F2() are_equivalent
provided
A1: ex F being covariant Functor of F1(),F2() st
( ( for a being object of F1() holds F . a = F3(a) ) & ( for a, b being object of F1() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . f = F5(a,b,f) ) ) and
A2: ex G being covariant Functor of F2(),F1() st
( ( for a being object of F2() holds G . a = F4(a) ) & ( for a, b being object of F2() st <^a,b^> <> {} holds
for f being Morphism of a,b holds G . f = F6(a,b,f) ) ) and
A3: for a, b being object of F1() st a = F4(F3(b)) holds
( F7(b) in <^a,b^> & F7(b) " in <^b,a^> & F7(b) is one-to-one ) and
A4: for a, b being object of F2() st b = F3(F4(a)) holds
( F8(a) in <^a,b^> & F8(a) " in <^b,a^> & F8(a) is one-to-one ) and
A5: for a, b being object of F1() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F7(b) * F6(F3(a),F3(b),F5(a,b,f)) = f * F7(a) and
A6: for a, b being object of F2() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F5(F4(a),F4(b),F6(a,b,f)) * F8(a) = F8(b) * f
proof end;

definition
let C be category;
defpred S1[ set , set ] means $1 = $2 `22 ;
defpred S2[ set , set , Function] means ex fa, fb being object of C ex g being Morphism of fa,fb st
( fa = $1 & fb = $2 & <^fa,fb^> <> {} & ( for o being object of C st <^o,fa^> <> {} holds
for h being Morphism of o,fa holds $3 . [h,[o,fa]] = [(g * h),[o,fb]] ) );
deffunc H1( set ) -> set = Union (disjoin the Arrows of C);
A1: for a, b, c being Element of C
for f, g being Function st S2[a,b,f] & S2[b,c,g] holds
S2[a,c,g * f]
proof end;
A9: for a being Element of C
for X being set st ( for x being set holds
( x in X iff ( x in H1(a) & S1[a,x] ) ) ) holds
S2[a,a, id X]
proof end;
func Concretized C -> strict concrete category means :Def12: :: YELLOW18:def 12
( the carrier of it = the carrier of C & ( for a being object of it
for x being set holds
( x in the_carrier_of a iff ( x in Union (disjoin the Arrows of C) & a = x `22 ) ) ) & ( for a, b being Element of C
for f being Function holds
( f in the Arrows of it . a,b iff ( f in Funcs (it -carrier_of a),(it -carrier_of b) & ex fa, fb being object of C ex g being Morphism of fa,fb st
( fa = a & fb = b & <^fa,fb^> <> {} & ( for o being object of C st <^o,fa^> <> {} holds
for h being Morphism of o,fa holds f . [h,[o,fa]] = [(g * h),[o,fb]] ) ) ) ) ) );
uniqueness
for b1, b2 being strict concrete category st the carrier of b1 = the carrier of C & ( for a being object of b1
for x being set holds
( x in the_carrier_of a iff ( x in Union (disjoin the Arrows of C) & a = x `22 ) ) ) & ( for a, b being Element of C
for f being Function holds
( f in the Arrows of b1 . a,b iff ( f in Funcs (b1 -carrier_of a),(b1 -carrier_of b) & ex fa, fb being object of C ex g being Morphism of fa,fb st
( fa = a & fb = b & <^fa,fb^> <> {} & ( for o being object of C st <^o,fa^> <> {} holds
for h being Morphism of o,fa holds f . [h,[o,fa]] = [(g * h),[o,fb]] ) ) ) ) ) & the carrier of b2 = the carrier of C & ( for a being object of b2
for x being set holds
( x in the_carrier_of a iff ( x in Union (disjoin the Arrows of C) & a = x `22 ) ) ) & ( for a, b being Element of C
for f being Function holds
( f in the Arrows of b2 . a,b iff ( f in Funcs (b2 -carrier_of a),(b2 -carrier_of b) & ex fa, fb being object of C ex g being Morphism of fa,fb st
( fa = a & fb = b & <^fa,fb^> <> {} & ( for o being object of C st <^o,fa^> <> {} holds
for h being Morphism of o,fa holds f . [h,[o,fa]] = [(g * h),[o,fb]] ) ) ) ) ) holds
b1 = b2
proof end;
existence
ex b1 being strict concrete category st
( the carrier of b1 = the carrier of C & ( for a being object of b1
for x being set holds
( x in the_carrier_of a iff ( x in Union (disjoin the Arrows of C) & a = x `22 ) ) ) & ( for a, b being Element of C
for f being Function holds
( f in the Arrows of b1 . a,b iff ( f in Funcs (b1 -carrier_of a),(b1 -carrier_of b) & ex fa, fb being object of C ex g being Morphism of fa,fb st
( fa = a & fb = b & <^fa,fb^> <> {} & ( for o being object of C st <^o,fa^> <> {} holds
for h being Morphism of o,fa holds f . [h,[o,fa]] = [(g * h),[o,fb]] ) ) ) ) ) )
proof end;
end;

:: deftheorem Def12 defines Concretized YELLOW18:def 12 :
for C being category
for b2 being strict concrete category holds
( b2 = Concretized C iff ( the carrier of b2 = the carrier of C & ( for a being object of b2
for x being set holds
( x in the_carrier_of a iff ( x in Union (disjoin the Arrows of C) & a = x `22 ) ) ) & ( for a, b being Element of C
for f being Function holds
( f in the Arrows of b2 . a,b iff ( f in Funcs (b2 -carrier_of a),(b2 -carrier_of b) & ex fa, fb being object of C ex g being Morphism of fa,fb st
( fa = a & fb = b & <^fa,fb^> <> {} & ( for o being object of C st <^o,fa^> <> {} holds
for h being Morphism of o,fa holds f . [h,[o,fa]] = [(g * h),[o,fb]] ) ) ) ) ) ) );

theorem Th45: :: YELLOW18:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being category
for a being object of A
for x being set holds
( x in (Concretized A) -carrier_of a iff ex b being object of A ex f being Morphism of b,a st
( <^b,a^> <> {} & x = [f,[b,a]] ) )
proof end;

registration
let A be category;
let a be object of A;
cluster (Concretized A) -carrier_of a -> non empty ;
coherence
not (Concretized A) -carrier_of a is empty
proof end;
end;

theorem Th46: :: YELLOW18:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being category
for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b ex F being Function of (Concretized A) -carrier_of a,(Concretized A) -carrier_of b st
( F in the Arrows of (Concretized A) . a,b & ( for c being object of A
for g being Morphism of c,a st <^c,a^> <> {} holds
F . [g,[c,a]] = [(f * g),[c,b]] ) )
proof end;

theorem Th47: :: YELLOW18:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being category
for a, b being object of A st <^a,b^> <> {} holds
for F1, F2 being Function st F1 in the Arrows of (Concretized A) . a,b & F2 in the Arrows of (Concretized A) . a,b & F1 . [(idm a),[a,a]] = F2 . [(idm a),[a,a]] holds
F1 = F2
proof end;

scheme :: YELLOW18:sch 23
NonUniqMSFunctionEx{ F1() -> set , F2() -> ManySortedSet of F1(), F3() -> ManySortedSet of F1(), P1[ set , set , set ] } :
ex F being ManySortedFunction of F2(),F3() st
for i, x being set st i in F1() & x in F2() . i holds
( (F . i) . x in F3() . i & P1[i,x,(F . i) . x] )
provided
A1: for i, x being set st i in F1() & x in F2() . i holds
ex y being set st
( y in F3() . i & P1[i,x,y] )
proof end;

definition
let A be category;
set B = Concretized A;
func Concretization A -> strict covariant Functor of A, Concretized A means :Def13: :: YELLOW18:def 13
( ( for a being object of A holds it . a = a ) & ( for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds (it . f) . [(idm a),[a,a]] = [f,[a,b]] ) );
uniqueness
for b1, b2 being strict covariant Functor of A, Concretized A st ( for a being object of A holds b1 . a = a ) & ( for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds (b1 . f) . [(idm a),[a,a]] = [f,[a,b]] ) & ( for a being object of A holds b2 . a = a ) & ( for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds (b2 . f) . [(idm a),[a,a]] = [f,[a,b]] ) holds
b1 = b2
proof end;
existence
ex b1 being strict covariant Functor of A, Concretized A st
( ( for a being object of A holds b1 . a = a ) & ( for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds (b1 . f) . [(idm a),[a,a]] = [f,[a,b]] ) )
proof end;
end;

:: deftheorem Def13 defines Concretization YELLOW18:def 13 :
for A being category
for b2 being strict covariant Functor of A, Concretized A holds
( b2 = Concretization A iff ( ( for a being object of A holds b2 . a = a ) & ( for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds (b2 . f) . [(idm a),[a,a]] = [f,[a,b]] ) ) );

registration
let A be category;
cluster Concretization A -> strict covariant bijective ;
coherence
Concretization A is bijective
proof end;
end;

theorem :: YELLOW18:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being category holds A, Concretized A are_isomorphic
proof end;