:: Concrete Categories
:: by Grzegorz Bancerek
::
:: Received January 12, 2001
:: Copyright (c) 2001-2021 Association of Mizar Users


:: <section1>Definability of categories and functors</section1>
scheme :: YELLOW18:sch 1
AltCatStrLambda{ F1() -> non empty set , F2( object , object ) -> set , F3( object , object , object , object , object ) -> object } :
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( object , object , object , object , object ) -> object } :
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( object , object , object , object , object ) -> object } :
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( object , object ) -> set , F3( object , object , object , object , object ) -> object } :
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( object , object ) -> object , F3( object , object , object , object , object ) -> object } :
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[ object , object , object ], F2( object , object ) -> set , F3( object , object , object , object , object ) -> object } :
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[ object ], P2[ object , object , object ] } :
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 a9, b9 being Object of B st a9 = a & b9 = b & <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a9,b9^> 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( object ) -> object , F4( object , object , object ) -> object } :
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 a9, b9, c9 being Object of F2() st a9 = F3(a) & b9 = F3(b) & c9 = F3(c) holds
for f9 being Morphism of a9,b9
for g9 being Morphism of b9,c9 st f9 = F4(a,b,f) & g9 = F4(b,c,g) holds
F4(a,c,(g * f)) = g9 * f9 and
A4: for a being Object of F1()
for a9 being Object of F2() st a9 = F3(a) holds
F4(a,a,(idm a)) = idm a9
proof end;

theorem Th1: :: YELLOW18:1
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( object ) -> object , F4( object , object , object ) -> object } :
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 a9, b9, c9 being Object of F2() st a9 = F3(a) & b9 = F3(b) & c9 = F3(c) holds
for f9 being Morphism of b9,a9
for g9 being Morphism of c9,b9 st f9 = F4(a,b,f) & g9 = F4(b,c,g) holds
F4(a,c,(g * f)) = f9 * g9 and
A4: for a being Object of F1()
for a9 being Object of F2() st a9 = F3(a) holds
F4(a,a,(idm a)) = idm a9
proof end;

theorem Th2: :: YELLOW18:2
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;

:: <section2>Isomorphism and equivalence of categories</section2>
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( object ) -> object , F5( object , object , object ) -> object } :
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( object ) -> object , F4( object , object , object ) -> object } :
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( object ) -> object , F5( object , object , object ) -> object } :
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( object ) -> object , F4( object , object , object ) -> object } :
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
for A, B, C being non empty reflexive AltGraph
for F1, F2 being feasible FunctorStr over A,B
for G1, G2 being FunctorStr over 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
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
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( object ) -> object } :
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( object ) -> object } :
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;

:: <section3>Dual categories</section3>
definition
let C1, C2 be non empty AltCatStr ;
pred C1,C2 are_opposite means :: 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 a9, b9, c9 being Object of C2 st a9 = a & b9 = b & c9 = c holds
the Comp of C2 . (a9,b9,c9) = ~ ( 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 a9, b9, c9 being Object of C2 st a9 = a & b9 = b & c9 = c holds
the Comp of C2 . (a9,b9,c9) = ~ ( 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 a9, b9, c9 being Object of C1 st a9 = a & b9 = b & c9 = c holds
the Comp of C1 . (a9,b9,c9) = ~ ( the Comp of C2 . (c,b,a)) ) )
proof end;
end;

:: deftheorem 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 a9, b9, c9 being Object of C2 st a9 = a & b9 = b & c9 = c holds
the Comp of C2 . (a9,b9,c9) = ~ ( the Comp of C1 . (c,b,a)) ) ) );

theorem :: YELLOW18:6
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 ;

theorem Th7: :: YELLOW18:7
for A, B being non empty AltCatStr st A,B are_opposite holds
for a, b being Object of A
for a9, b9 being Object of B st a9 = a & b9 = b holds
<^a,b^> = <^b9,a9^> by ALTCAT_2:6;

theorem :: YELLOW18:8
for A, B being non empty AltCatStr st A,B are_opposite holds
for a, b being Object of A
for a9, b9 being Object of B st a9 = a & b9 = b holds
for f being Morphism of a,b holds f is Morphism of b9,a9 by Th7;

theorem Th9: :: YELLOW18:9
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 a9, b9, c9 being Object of C2 st a9 = a & b9 = b & c9 = c holds
( <^a,b^> = <^b9,a9^> & ( <^a,b^> <> {} & <^b,c^> <> {} implies for f being Morphism of a,b
for g being Morphism of b,c
for f9 being Morphism of b9,a9
for g9 being Morphism of c9,b9 st f9 = f & g9 = g holds
f9 * g9 = g * f ) ) ) ) )
proof end;

theorem Th10: :: YELLOW18:10
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
for A, B being non empty transitive AltCatStr st A,B are_opposite & A is associative holds
B is associative
proof end;

theorem Th12: :: YELLOW18:12
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 Th13: :: YELLOW18:13
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 Th13;
existence
ex b1 being non empty transitive strict AltCatStr st C,b1 are_opposite
proof end;
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 by Def4, Th11;
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 by Def4, Th12;
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;
A3: now :: thesis: for a, b being Object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds H2(a,b,f) in the Arrows of B . (H1(b),H1(a))
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 a9 = a, b9 = b as Object of B by A2;
<^a,b^> = <^b9,a9^> 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 a9, b9, c9 being Object of B st a9 = H1(a) & b9 = H1(b) & c9 = H1(c) holds
for f9 being Morphism of b9,a9
for g9 being Morphism of c9,b9 st f9 = H2(a,b,f) & g9 = H2(b,c,g) holds
H2(a,c,g * f) = f9 * g9 by A1, Th9;
A6: for a being Object of A
for a9 being Object of B st a9 = H1(a) holds
H2(a,a, idm a) = idm a9 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 Th14: :: YELLOW18:14
for A, B being category st A,B are_opposite holds
(dualizing-func (A,B)) * (dualizing-func (B,A)) = id B
proof end;

theorem Th15: :: YELLOW18:15
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 by Def4, Th15;
cluster dualizing-func ((A opp),A) -> strict contravariant bijective ;
coherence
dualizing-func ((A opp),A) is bijective
proof end;
end;

theorem :: YELLOW18:16
for A, B being category st A,B are_opposite holds
A,B are_anti-isomorphic
proof end;

theorem Th17: :: YELLOW18:17
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:18
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:19
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 :: thesis: 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 a9, b9 being Object of B st a9 = a & b9 = b holds
for f being Morphism of a,b
for f9 being Morphism of b9,a9 st f9 = f holds
( ( f is retraction implies f9 is coretraction ) & ( f is coretraction implies f9 is retraction ) )
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 a9, b9 being Object of B st a9 = a & b9 = b holds
for f being Morphism of a,b
for f9 being Morphism of b9,a9 st f9 = f holds
( ( f is retraction implies f9 is coretraction ) & ( f is coretraction implies f9 is retraction ) ) )
assume A1: A,B are_opposite ; :: thesis: for a, b being Object of A st <^a,b^> <> {} & <^b,a^> <> {} holds
for a9, b9 being Object of B st a9 = a & b9 = b holds
for f being Morphism of a,b
for f9 being Morphism of b9,a9 st f9 = f holds
( ( f is retraction implies f9 is coretraction ) & ( f is coretraction implies f9 is retraction ) )
let a, b be Object of A; :: thesis: ( <^a,b^> <> {} & <^b,a^> <> {} implies for a9, b9 being Object of B st a9 = a & b9 = b holds
for f being Morphism of a,b
for f9 being Morphism of b9,a9 st f9 = f holds
( ( f is retraction implies f9 is coretraction ) & ( f is coretraction implies f9 is retraction ) ) )
assume that
A2: <^a,b^> <> {} and
A3: <^b,a^> <> {} ; :: thesis: for a9, b9 being Object of B st a9 = a & b9 = b holds
for f being Morphism of a,b
for f9 being Morphism of b9,a9 st f9 = f holds
( ( f is retraction implies f9 is coretraction ) & ( f is coretraction implies f9 is retraction ) )
let a9, b9 be Object of B; :: thesis: ( a9 = a & b9 = b implies for f being Morphism of a,b
for f9 being Morphism of b9,a9 st f9 = f holds
( ( f is retraction implies f9 is coretraction ) & ( f is coretraction implies f9 is retraction ) ) )
assume that
A4: a9 = a and
A5: b9 = b ; :: thesis: for f being Morphism of a,b
for f9 being Morphism of b9,a9 st f9 = f holds
( ( f is retraction implies f9 is coretraction ) & ( f is coretraction implies f9 is retraction ) )
let f be Morphism of a,b; :: thesis: for f9 being Morphism of b9,a9 st f9 = f holds
( ( f is retraction implies f9 is coretraction ) & ( f is coretraction implies f9 is retraction ) )
let f9 be Morphism of b9,a9; :: thesis: ( f9 = f implies ( ( f is retraction implies f9 is coretraction ) & ( f is coretraction implies f9 is retraction ) ) )
assume A6: f9 = f ; :: thesis: ( ( f is retraction implies f9 is coretraction ) & ( f is coretraction implies f9 is retraction ) )
thus ( f is retraction implies f9 is coretraction ) :: thesis: ( f is coretraction implies f9 is retraction )
proof
given g being Morphism of b,a such that A7: g is_right_inverse_of f ; :: according to ALTCAT_3:def 2 :: thesis: f9 is coretraction
reconsider g9 = g as Morphism of a9,b9 by A1, A4, A5, Th7;
take g9 ; :: according to ALTCAT_3:def 3 :: thesis: g9 is_left_inverse_of f9
f * g = idm b by A7
.= idm b9 by A1, A5, Th10 ;
hence g9 * f9 = idm b9 by A1, A2, A3, A4, A5, A6, Th9; :: according to ALTCAT_3:def 1 :: thesis: verum
end;
thus ( f is coretraction implies f9 is retraction ) :: thesis: verum
proof
given g being Morphism of b,a such that A8: g is_left_inverse_of f ; :: according to ALTCAT_3:def 3 :: thesis: f9 is retraction
reconsider g9 = g as Morphism of a9,b9 by A1, A4, A5, Th7;
take g9 ; :: according to ALTCAT_3:def 2 :: thesis: f9 is_left_inverse_of g9
g * f = idm a by A8
.= idm a9 by A1, A4, Th10 ;
hence f9 * g9 = idm a9 by A1, A2, A3, A4, A5, A6, Th9; :: according to ALTCAT_3:def 1 :: thesis: verum
end;
end;

theorem :: YELLOW18:20
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 a9, b9 being Object of B st a9 = a & b9 = b holds
for f being Morphism of a,b
for f9 being Morphism of b9,a9 st f9 = f holds
( f is retraction iff f9 is coretraction )
proof end;

theorem :: YELLOW18:21
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 a9, b9 being Object of B st a9 = a & b9 = b holds
for f being Morphism of a,b
for f9 being Morphism of b9,a9 st f9 = f holds
( f is coretraction iff f9 is retraction )
proof end;

theorem Th22: :: YELLOW18:22
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 a9, b9 being Object of B st a9 = a & b9 = b holds
for f being Morphism of a,b
for f9 being Morphism of b9,a9 st f9 = f & f is retraction & f is coretraction holds
f9 " = f "
proof end;

theorem Th23: :: YELLOW18:23
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 a9, b9 being Object of B st a9 = a & b9 = b holds
for f being Morphism of a,b
for f9 being Morphism of b9,a9 st f9 = f holds
( f is iso iff f9 is iso )
proof end;

theorem Th24: :: YELLOW18:24
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 Th25: :: YELLOW18:25
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:26
for A, B being category st A,B are_anti-isomorphic holds
A,B are_dual
proof end;

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

theorem :: YELLOW18:29
for A, B, C being category st A,B are_dual & B,C are_dual holds
A,C are_equivalent
proof end;

:: <section4>Concrete categories</section4>
theorem Th30: :: YELLOW18:30
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 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 non empty transitive quasi-functional associative with_units -> para-functional for 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, 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 Th31: :: YELLOW18:31
for A being non empty set
for a being Object of (EnsCat A) holds idm a = id a
proof end;

theorem Th32: :: YELLOW18:32
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 -> set-id-inheriting ;
coherence
EnsCat A is set-id-inheriting
proof end;
end;

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

:: deftheorem 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 non empty transitive associative with_units concrete -> semi-functional para-functional set-id-inheriting for AltCatStr ;
coherence
for b1 being category st b1 is concrete holds
( b1 is para-functional & b1 is semi-functional & b1 is set-id-inheriting ) ;
cluster non empty transitive semi-functional associative with_units para-functional set-id-inheriting -> concrete for AltCatStr ;
coherence
for b1 being category st b1 is para-functional & b1 is semi-functional & b1 is set-id-inheriting holds
b1 is concrete ;
end;

registration
cluster non empty transitive strict quasi-functional associative with_units reflexive concrete for AltCatStr ;
existence
ex b1 being category st
( b1 is concrete & b1 is quasi-functional & b1 is strict )
proof end;
end;

theorem Th33: :: YELLOW18:33
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 Th34: :: YELLOW18:34
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 for 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 Th35: :: YELLOW18:35
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 Th36: :: YELLOW18:36
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 Th37: :: YELLOW18:37
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( object , object ) -> set , F3( object ) -> 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[ object , object , object ], F2( object ) -> 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( object ) -> set , P1[ object , object ], P2[ object , object , object ] } :
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( object , object ) -> object } :
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[ object , object , object ], F2( object ) -> 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( object ) -> set , P1[ object , object ], P2[ object , object , object ] } :
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;

:: <section5>Equivalence between concrete categories</section5>
theorem Th38: :: YELLOW18:38
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 Th39: :: YELLOW18:39
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 Th40: :: YELLOW18:40
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 ) by ALTCAT_3:5, Th38, Th39;

theorem Th41: :: YELLOW18:41
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:42
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( object ) -> object , F4( object ) -> object , F5( object , object , object ) -> Function, F6( object , object , object ) -> Function, F7( object ) -> Function, F8( object ) -> 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;

:: <section6>Concretization of categories</section6>
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;
A13: 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 Th43: :: YELLOW18:43
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 Th44: :: YELLOW18:44
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 Th45: :: YELLOW18:45
for A being category
for a, b being Object of A
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[ object , object , object ] } :
ex F being ManySortedFunction of F2(),F3() st
for i, x being object 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 object st i in F1() & x in F2() . i holds
ex y being object 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;

:: WP: Representation theorem for categories as concrete categories
theorem :: YELLOW18:46
for A being category holds A, Concretized A are_isomorphic
proof end;