:: YELLOW18 semantic presentation

scheme :: YELLOW18:sch 1
s1{ F₁() -> non empty set , F₂( set , set ) -> set , F₃( set , set , set , set , set ) -> set } :

ex b₁ being non empty transitive strict AltCatStr st
( the carrier of b₁ = F₁() & ( for b₂, b₃ being object of b₁ holds <^b₂,b₃^> = F₂(b₂,b₃) ) & ( for b₂, b₃, b₄ being object of b₁ st <^b₂,b₃^> <> {} & <^b₃,b₄^> <> {} holds
for b₅ being Morphism of b₂,b₃
for b₆ being Morphism of b₃,b₄ holds b₆ * b₅ = F₃(b₂,b₃,b₄,b₅,b₆) ) )

provided

E1: for b₁, b₂, b₃ being Element of F₁()
for b₄, b₅ being set st b₄ in F₂(b₁,b₂) & b₅ in F₂(b₂,b₃) holds
F₃(b₁,b₂,b₃,b₄,b₅) in F₂(b₁,b₃)

proof end;

scheme :: YELLOW18:sch 2
s2{ F₁() -> non empty transitive AltCatStr , F₂( set , set , set , set , set ) -> set } :

F₁() is associative

provided

E1: for b₁, b₂, b₃ being object of F₁() st <^b₁,b₂^> <> {} & <^b₂,b₃^> <> {} holds
for b₄ being Morphism of b₁,b₂
for b₅ being Morphism of b₂,b₃ holds b₅ * b₄ = F₂(b₁,b₂,b₃,b₄,b₅) and
E2: for b₁, b₂, b₃, b₄ being object of F₁()
for b₅, b₆, b₇ being set st b₅ in <^b₁,b₂^> & b₆ in <^b₂,b₃^> & b₇ in <^b₃,b₄^> holds
F₂(b₁,b₃,b₄,F₂(b₁,b₂,b₃,b₅,b₆),b₇) = F₂(b₁,b₂,b₄,b₅,F₂(b₂,b₃,b₄,b₆,b₇))

proof end;

scheme :: YELLOW18:sch 3
s3{ F₁() -> non empty transitive AltCatStr , F₂( set , set , set , set , set ) -> set } :

F₁() is with_units

provided

E1: for b₁, b₂, b₃ being object of F₁() st <^b₁,b₂^> <> {} & <^b₂,b₃^> <> {} holds
for b₄ being Morphism of b₁,b₂
for b₅ being Morphism of b₂,b₃ holds b₅ * b₄ = F₂(b₁,b₂,b₃,b₄,b₅) and
E2: for b₁ being object of F₁() ex b₂ being set st
( b₂ in <^b₁,b₁^> & ( for b₃ being object of F₁()
for b₄ being set st b₄ in <^b₁,b₃^> holds
F₂(b₁,b₁,b₃,b₂,b₄) = b₄ ) ) and
E3: for b₁ being object of F₁() ex b₂ being set st
( b₂ in <^b₁,b₁^> & ( for b₃ being object of F₁()
for b₄ being set st b₄ in <^b₃,b₁^> holds
F₂(b₃,b₁,b₁,b₄,b₂) = b₄ ) )

proof end;

scheme :: YELLOW18:sch 4
s4{ F₁() -> non empty set , F₂( set , set ) -> set , F₃( set , set , set , set , set ) -> set } :

ex b₁ being strict category st
( the carrier of b₁ = F₁() & ( for b₂, b₃ being object of b₁ holds <^b₂,b₃^> = F₂(b₂,b₃) ) & ( for b₂, b₃, b₄ being object of b₁ st <^b₂,b₃^> <> {} & <^b₃,b₄^> <> {} holds
for b₅ being Morphism of b₂,b₃
for b₆ being Morphism of b₃,b₄ holds b₆ * b₅ = F₃(b₂,b₃,b₄,b₅,b₆) ) )

provided

E1: for b₁, b₂, b₃ being Element of F₁()
for b₄, b₅ being set st b₄ in F₂(b₁,b₂) & b₅ in F₂(b₂,b₃) holds
F₃(b₁,b₂,b₃,b₄,b₅) in F₂(b₁,b₃) and
E2: for b₁, b₂, b₃, b₄ being Element of F₁()
for b₅, b₆, b₇ being set st b₅ in F₂(b₁,b₂) & b₆ in F₂(b₂,b₃) & b₇ in F₂(b₃,b₄) holds
F₃(b₁,b₃,b₄,F₃(b₁,b₂,b₃,b₅,b₆),b₇) = F₃(b₁,b₂,b₄,b₅,F₃(b₂,b₃,b₄,b₆,b₇)) and
E3: for b₁ being Element of F₁() ex b₂ being set st
( b₂ in F₂(b₁,b₁) & ( for b₃ being Element of F₁()
for b₄ being set st b₄ in F₂(b₁,b₃) holds
F₃(b₁,b₁,b₃,b₂,b₄) = b₄ ) ) and
E4: for b₁ being Element of F₁() ex b₂ being set st
( b₂ in F₂(b₁,b₁) & ( for b₃ being Element of F₁()
for b₄ being set st b₄ in F₂(b₃,b₁) holds
F₃(b₃,b₁,b₁,b₄,b₂) = b₄ ) )

proof end;

scheme :: YELLOW18:sch 5
s5{ F₁() -> non empty set , F₂( set , set ) -> set , F₃( set , set , set , set , set ) -> set } :

for b₁, b₂ being non empty transitive AltCatStr st the carrier of b₁ = F₁() & ( for b₃, b₄ being object of b₁ holds <^b₃,b₄^> = F₂(b₃,b₄) ) & ( for b₃, b₄, b₅ being object of b₁ st <^b₃,b₄^> <> {} & <^b₄,b₅^> <> {} holds
for b₆ being Morphism of b₃,b₄
for b₇ being Morphism of b₄,b₅ holds b₇ * b₆ = F₃(b₃,b₄,b₅,b₆,b₇) ) & the carrier of b₂ = F₁() & ( for b₃, b₄ being object of b₂ holds <^b₃,b₄^> = F₂(b₃,b₄) ) & ( for b₃, b₄, b₅ being object of b₂ st <^b₃,b₄^> <> {} & <^b₄,b₅^> <> {} holds
for b₆ being Morphism of b₃,b₄
for b₇ being Morphism of b₄,b₅ holds b₇ * b₆ = F₃(b₃,b₄,b₅,b₆,b₇) ) holds
AltCatStr(# the carrier of b₁,the Arrows of b₁,the Comp of b₁ #) = AltCatStr(# the carrier of b₂,the Arrows of b₂,the Comp of b₂ #)

proof end;

scheme :: YELLOW18:sch 6
s6{ F₁() -> non empty set , P₁[ set , set , set ], F₂( set , set ) -> set , F₃( set , set , set , set , set ) -> set } :

ex b₁ being strict category st
( the carrier of b₁ = F₁() & ( for b₂, b₃ being object of b₁
for b₄ being set holds
( b₄ in <^b₂,b₃^> iff ( b₄ in F₂(b₂,b₃) & P₁[b₂,b₃,b₄] ) ) ) & ( for b₂, b₃, b₄ being object of b₁ st <^b₂,b₃^> <> {} & <^b₃,b₄^> <> {} holds
for b₅ being Morphism of b₂,b₃
for b₆ being Morphism of b₃,b₄ holds b₆ * b₅ = F₃(b₂,b₃,b₄,b₅,b₆) ) )

provided

E1: for b₁, b₂, b₃ being Element of F₁()
for b₄, b₅ being set st b₄ in F₂(b₁,b₂) & P₁[b₁,b₂,b₄] & b₅ in F₂(b₂,b₃) & P₁[b₂,b₃,b₅] holds
( F₃(b₁,b₂,b₃,b₄,b₅) in F₂(b₁,b₃) & P₁[b₁,b₃,F₃(b₁,b₂,b₃,b₄,b₅)] ) and
E2: for b₁, b₂, b₃, b₄ being Element of F₁()
for b₅, b₆, b₇ being set st b₅ in F₂(b₁,b₂) & P₁[b₁,b₂,b₅] & b₆ in F₂(b₂,b₃) & P₁[b₂,b₃,b₆] & b₇ in F₂(b₃,b₄) & P₁[b₃,b₄,b₇] holds
F₃(b₁,b₃,b₄,F₃(b₁,b₂,b₃,b₅,b₆),b₇) = F₃(b₁,b₂,b₄,b₅,F₃(b₂,b₃,b₄,b₆,b₇)) and
E3: for b₁ being Element of F₁() ex b₂ being set st
( b₂ in F₂(b₁,b₁) & P₁[b₁,b₁,b₂] & ( for b₃ being Element of F₁()
for b₄ being set st b₄ in F₂(b₁,b₃) & P₁[b₁,b₃,b₄] holds
F₃(b₁,b₁,b₃,b₂,b₄) = b₄ ) ) and
E4: for b₁ being Element of F₁() ex b₂ being set st
( b₂ in F₂(b₁,b₁) & P₁[b₁,b₁,b₂] & ( for b₃ being Element of F₁()
for b₄ being set st b₄ in F₂(b₃,b₁) & P₁[b₃,b₁,b₄] holds
F₃(b₃,b₁,b₁,b₄,b₂) = b₄ ) )

proof end;

registration

let c₁ be Function-yielding Function;
let c₂, c₃, c₄ be set ;
cluster a₁ . a₂,a₃,a₄ -> Relation-like Function-like ;
coherence

proof end;

end;

scheme :: YELLOW18:sch 7
s7{ F₁() -> category, P₁[ set ], P₂[ set , set , set ] } :

ex b₁ being non empty strict subcategory of F₁() st
( ( for b₂ being object of F₁() holds
( b₂ is object of b₁ iff P₁[b₂] ) ) & ( for b₂, b₃ being object of F₁()
for b₄, b₅ being object of b₁ st b₄ = b₂ & b₅ = b₃ & <^b₂,b₃^> <> {} holds
for b₆ being Morphism of b₂,b₃ holds
( b₆ in <^b₄,b₅^> iff P₂[b₂,b₃,b₆] ) ) )

provided

E1: ex b₁ being object of F₁() st P₁[b₁] and
E2: for b₁, b₂, b₃ being object of F₁() st P₁[b₁] & P₁[b₂] & P₁[b₃] & <^b₁,b₂^> <> {} & <^b₂,b₃^> <> {} holds
for b₄ being Morphism of b₁,b₂
for b₅ being Morphism of b₂,b₃ st P₂[b₁,b₂,b₄] & P₂[b₂,b₃,b₅] holds
P₂[b₁,b₃,b₅ * b₄] and
E3: for b₁ being object of F₁() st P₁[b₁] holds
P₂[b₁,b₁, idm b₁]

proof end;

scheme :: YELLOW18:sch 8
s8{ F₁() -> category, F₂() -> category, F₃( set ) -> set , F₄( set , set , set ) -> set } :

ex b₁ being strict covariant Functor of F₁(),F₂() st
( ( for b₂ being object of F₁() holds b₁ . b₂ = F₃(b₂) ) & ( for b₂, b₃ being object of F₁() st <^b₂,b₃^> <> {} holds
for b₄ being Morphism of b₂,b₃ holds b₁ . b₄ = F₄(b₂,b₃,b₄) ) )

provided

E1: for b₁ being object of F₁() holds F₃(b₁) is object of F₂() and
E2: for b₁, b₂ being object of F₁() st <^b₁,b₂^> <> {} holds
for b₃ being Morphism of b₁,b₂ holds F₄(b₁,b₂,b₃) in the Arrows of F₂() . F₃(b₁),F₃(b₂) and
E3: for b₁, b₂, b₃ being object of F₁() st <^b₁,b₂^> <> {} & <^b₂,b₃^> <> {} holds
for b₄ being Morphism of b₁,b₂
for b₅ being Morphism of b₂,b₃
for b₆, b₇, b₈ being object of F₂() st b₆ = F₃(b₁) & b₇ = F₃(b₂) & b₈ = F₃(b₃) holds
for b₉ being Morphism of b₆,b₇
for b₁₀ being Morphism of b₇,b₈ st b₉ = F₄(b₁,b₂,b₄) & b₁₀ = F₄(b₂,b₃,b₅) holds
F₄(b₁,b₃,(b₅ * b₄)) = b₁₀ * b₉ and
E4: for b₁ being object of F₁()
for b₂ being object of F₂() st b₂ = F₃(b₁) holds
F₄(b₁,b₁,(idm b₁)) = idm b₂

proof end;

theorem Th1: :: YELLOW18:1

for b₁, b₂ being category
for b₃, b₄ being covariant Functor of b₁,b₂ st ( for b₅ being object of b₁ holds b₃ . b₅ = b₄ . b₅ ) & ( for b₅, b₆ being object of b₁ st <^b₅,b₆^> <> {} holds
for b₇ being Morphism of b₅,b₆ holds b₃ . b₇ = b₄ . b₇ ) holds
FunctorStr(# the ObjectMap of b₃,the MorphMap of b₃ #) = FunctorStr(# the ObjectMap of b₄,the MorphMap of b₄ #)

proof end;

scheme :: YELLOW18:sch 9
s9{ F₁() -> category, F₂() -> category, F₃( set ) -> set , F₄( set , set , set ) -> set } :

ex b₁ being strict contravariant Functor of F₁(),F₂() st
( ( for b₂ being object of F₁() holds b₁ . b₂ = F₃(b₂) ) & ( for b₂, b₃ being object of F₁() st <^b₂,b₃^> <> {} holds
for b₄ being Morphism of b₂,b₃ holds b₁ . b₄ = F₄(b₂,b₃,b₄) ) )

provided

E2: for b₁ being object of F₁() holds F₃(b₁) is object of F₂() and
E3: for b₁, b₂ being object of F₁() st <^b₁,b₂^> <> {} holds
for b₃ being Morphism of b₁,b₂ holds F₄(b₁,b₂,b₃) in the Arrows of F₂() . F₃(b₂),F₃(b₁) and
E4: for b₁, b₂, b₃ being object of F₁() st <^b₁,b₂^> <> {} & <^b₂,b₃^> <> {} holds
for b₄ being Morphism of b₁,b₂
for b₅ being Morphism of b₂,b₃
for b₆, b₇, b₈ being object of F₂() st b₆ = F₃(b₁) & b₇ = F₃(b₂) & b₈ = F₃(b₃) holds
for b₉ being Morphism of b₇,b₆
for b₁₀ being Morphism of b₈,b₇ st b₉ = F₄(b₁,b₂,b₄) & b₁₀ = F₄(b₂,b₃,b₅) holds
F₄(b₁,b₃,(b₅ * b₄)) = b₉ * b₁₀ and
E5: for b₁ being object of F₁()
for b₂ being object of F₂() st b₂ = F₃(b₁) holds
F₄(b₁,b₁,(idm b₁)) = idm b₂

proof end;

theorem Th2: :: YELLOW18:2

for b₁, b₂ being category
for b₃, b₄ being contravariant Functor of b₁,b₂ st ( for b₅ being object of b₁ holds b₃ . b₅ = b₄ . b₅ ) & ( for b₅, b₆ being object of b₁ st <^b₅,b₆^> <> {} holds
for b₇ being Morphism of b₅,b₆ holds b₃ . b₇ = b₄ . b₇ ) holds
FunctorStr(# the ObjectMap of b₃,the MorphMap of b₃ #) = FunctorStr(# the ObjectMap of b₄,the MorphMap of b₄ #)

proof end;

definition

let c₁, c₂, c₃ be non empty set ;
let c₄ be Function of [:c₁,c₂:],c₃;
redefine attr one-to-one as a₄ is one-to-one means :: YELLOW18:def 1
for b₁, b₂ being Element of a₁
for b₃, b₄ being Element of a₂ st a₄ . b₁,b₃ = a₄ . b₂,b₄ holds
( b₁ = b₂ & b₃ = b₄ );
compatibility

proof end;

end;

:: deftheorem Def1 defines one-to-one YELLOW18:def 1 :

scheme :: YELLOW18:sch 10
s10{ F₁() -> category, F₂() -> category, F₃() -> covariant Functor of F₁(),F₂(), F₄( set ) -> set , F₅( set , set , set ) -> set } :

F₃() is bijective

provided

E3: for b₁ being object of F₁() holds F₃() . b₁ = F₄(b₁) and
E4: for b₁, b₂ being object of F₁() st <^b₁,b₂^> <> {} holds
for b₃ being Morphism of b₁,b₂ holds F₃() . b₃ = F₅(b₁,b₂,b₃) and
E5: for b₁, b₂ being object of F₁() st F₄(b₁) = F₄(b₂) holds
b₁ = b₂ and
E6: for b₁, b₂ being object of F₁() st <^b₁,b₂^> <> {} holds
for b₃, b₄ being Morphism of b₁,b₂ st F₅(b₁,b₂,b₃) = F₅(b₁,b₂,b₄) holds
b₃ = b₄ and
E7: for b₁, b₂ being object of F₂() st <^b₁,b₂^> <> {} holds
for b₃ being Morphism of b₁,b₂ ex b₄, b₅ being object of F₁()ex b₆ being Morphism of b₄,b₅ st
( b₁ = F₄(b₄) & b₂ = F₄(b₅) & <^b₄,b₅^> <> {} & b₃ = F₅(b₄,b₅,b₆) )

proof end;

scheme :: YELLOW18:sch 11
s11{ F₁() -> category, F₂() -> category, F₃( set ) -> set , F₄( set , set , set ) -> set } :

F₁(),F₂() are_isomorphic

provided

E3: ex b₁ being covariant Functor of F₁(),F₂() st
( ( for b₂ being object of F₁() holds b₁ . b₂ = F₃(b₂) ) & ( for b₂, b₃ being object of F₁() st <^b₂,b₃^> <> {} holds
for b₄ being Morphism of b₂,b₃ holds b₁ . b₄ = F₄(b₂,b₃,b₄) ) ) and
E4: for b₁, b₂ being object of F₁() st F₃(b₁) = F₃(b₂) holds
b₁ = b₂ and
E5: for b₁, b₂ being object of F₁() st <^b₁,b₂^> <> {} holds
for b₃, b₄ being Morphism of b₁,b₂ st F₄(b₁,b₂,b₃) = F₄(b₁,b₂,b₄) holds
b₃ = b₄ and
E6: for b₁, b₂ being object of F₂() st <^b₁,b₂^> <> {} holds
for b₃ being Morphism of b₁,b₂ ex b₄, b₅ being object of F₁()ex b₆ being Morphism of b₄,b₅ st
( b₁ = F₃(b₄) & b₂ = F₃(b₅) & <^b₄,b₅^> <> {} & b₃ = F₄(b₄,b₅,b₆) )

proof end;

scheme :: YELLOW18:sch 12
s12{ F₁() -> category, F₂() -> category, F₃() -> contravariant Functor of F₁(),F₂(), F₄( set ) -> set , F₅( set , set , set ) -> set } :

F₃() is bijective

provided

E3: for b₁ being object of F₁() holds F₃() . b₁ = F₄(b₁) and
E4: for b₁, b₂ being object of F₁() st <^b₁,b₂^> <> {} holds
for b₃ being Morphism of b₁,b₂ holds F₃() . b₃ = F₅(b₁,b₂,b₃) and
E5: for b₁, b₂ being object of F₁() st F₄(b₁) = F₄(b₂) holds
b₁ = b₂ and
E6: for b₁, b₂ being object of F₁() st <^b₁,b₂^> <> {} holds
for b₃, b₄ being Morphism of b₁,b₂ st F₅(b₁,b₂,b₃) = F₅(b₁,b₂,b₄) holds
b₃ = b₄ and
E7: for b₁, b₂ being object of F₂() st <^b₁,b₂^> <> {} holds
for b₃ being Morphism of b₁,b₂ ex b₄, b₅ being object of F₁()ex b₆ being Morphism of b₄,b₅ st
( b₂ = F₄(b₄) & b₁ = F₄(b₅) & <^b₄,b₅^> <> {} & b₃ = F₅(b₄,b₅,b₆) )

proof end;

scheme :: YELLOW18:sch 13
s13{ F₁() -> category, F₂() -> category, F₃( set ) -> set , F₄( set , set , set ) -> set } :

F₁(),F₂() are_anti-isomorphic

provided

E3: ex b₁ being contravariant Functor of F₁(),F₂() st
( ( for b₂ being object of F₁() holds b₁ . b₂ = F₃(b₂) ) & ( for b₂, b₃ being object of F₁() st <^b₂,b₃^> <> {} holds
for b₄ being Morphism of b₂,b₃ holds b₁ . b₄ = F₄(b₂,b₃,b₄) ) ) and
E4: for b₁, b₂ being object of F₁() st F₃(b₁) = F₃(b₂) holds
b₁ = b₂ and
E5: for b₁, b₂ being object of F₁() st <^b₁,b₂^> <> {} holds
for b₃, b₄ being Morphism of b₁,b₂ st F₄(b₁,b₂,b₃) = F₄(b₁,b₂,b₄) holds
b₃ = b₄ and
E6: for b₁, b₂ being object of F₂() st <^b₁,b₂^> <> {} holds
for b₃ being Morphism of b₁,b₂ ex b₄, b₅ being object of F₁()ex b₆ being Morphism of b₄,b₅ st
( b₂ = F₃(b₄) & b₁ = F₃(b₅) & <^b₄,b₅^> <> {} & b₃ = F₄(b₄,b₅,b₆) )

proof end;

definition

let c₁, c₂ be category;
pred c₁,c₂ are_equivalent means :: YELLOW18:def 2
ex b₁ being covariant Functor of a₁,a₂ex b₂ being covariant Functor of a₂,a₁ st
( b₂ * b₁, id a₁ are_naturally_equivalent & b₁ * b₂, id a₂ are_naturally_equivalent );
reflexivity

proof end;

symmetry ;

end;

:: deftheorem Def2 defines are_equivalent YELLOW18:def 2 :

theorem Th3: :: YELLOW18:3

for b₁, b₂, b₃ being non empty reflexive AltGraph
for b₄, b₅ being feasible FunctorStr of b₁,b₂
for b₆, b₇ being FunctorStr of b₂,b₃ st FunctorStr(# the ObjectMap of b₄,the MorphMap of b₄ #) = FunctorStr(# the ObjectMap of b₅,the MorphMap of b₅ #) & FunctorStr(# the ObjectMap of b₆,the MorphMap of b₆ #) = FunctorStr(# the ObjectMap of b₇,the MorphMap of b₇ #) holds
b₆ * b₄ = b₇ * b₅

proof end;

theorem Th4: :: YELLOW18:4

for b₁, b₂, b₃ being category st b₁,b₂ are_equivalent & b₂,b₃ are_equivalent holds
b₁,b₃ are_equivalent

proof end;

theorem Th5: :: YELLOW18:5

for b₁, b₂ being category st b₁,b₂ are_isomorphic holds
b₁,b₂ are_equivalent

proof end;

scheme :: YELLOW18:sch 14
s14{ F₁() -> category, F₂() -> category, F₃() -> covariant Functor of F₁(),F₂(), F₄() -> covariant Functor of F₁(),F₂(), F₅( set ) -> set } :

ex b₁ being natural_transformation of F₃(),F₄() st
( F₃() is_naturally_transformable_to F₄() & ( for b₂ being object of F₁() holds b₁ ! b₂ = F₅(b₂) ) )

provided

E6: for b₁ being object of F₁() holds F₅(b₁) in <^(F₃() . b₁),(F₄() . b₁)^> and
E7: for b₁, b₂ being object of F₁() st <^b₁,b₂^> <> {} holds
for b₃ being Morphism of b₁,b₂
for b₄ being Morphism of (F₃() . b₁),(F₄() . b₁) st b₄ = F₅(b₁) holds
for b₅ being Morphism of (F₃() . b₂),(F₄() . b₂) st b₅ = F₅(b₂) holds
b₅ * (F₃() . b₃) = (F₄() . b₃) * b₄

proof end;

scheme :: YELLOW18:sch 15
s15{ F₁() -> category, F₂() -> category, F₃() -> covariant Functor of F₁(),F₂(), F₄() -> covariant Functor of F₁(),F₂(), F₅( set ) -> set } :

ex b₁ being natural_equivalence of F₃(),F₄() st
( F₃(),F₄() are_naturally_equivalent & ( for b₂ being object of F₁() holds b₁ ! b₂ = F₅(b₂) ) )

provided

E6: for b₁ being object of F₁() holds
( F₅(b₁) in <^(F₃() . b₁),(F₄() . b₁)^> & <^(F₄() . b₁),(F₃() . b₁)^> <> {} & ( for b₂ being Morphism of (F₃() . b₁),(F₄() . b₁) st b₂ = F₅(b₁) holds
b₂ is iso ) ) and
E7: for b₁, b₂ being object of F₁() st <^b₁,b₂^> <> {} holds
for b₃ being Morphism of b₁,b₂
for b₄ being Morphism of (F₃() . b₁),(F₄() . b₁) st b₄ = F₅(b₁) holds
for b₅ being Morphism of (F₃() . b₂),(F₄() . b₂) st b₅ = F₅(b₂) holds
b₅ * (F₃() . b₃) = (F₄() . b₃) * b₄

proof end;

definition

let c₁, c₂ be non empty AltCatStr ;
pred c₁,c₂ are_opposite means :Def3: :: YELLOW18:def 3
( the carrier of a₂ = the carrier of a₁ & the Arrows of a₂ = ~ the Arrows of a₁ & ( for b₁, b₂, b₃ being object of a₁
for b₄, b₅, b₆ being object of a₂ st b₄ = b₁ & b₅ = b₂ & b₆ = b₃ holds
the Comp of a₂ . b₄,b₅,b₆ = ~ (the Comp of a₁ . b₃,b₂,b₁) ) );
symmetry

proof end;

end;

:: deftheorem Def3 defines are_opposite YELLOW18:def 3 :

theorem Th6: :: YELLOW18:6

for b₁, b₂ being non empty AltCatStr st b₁,b₂ are_opposite holds
for b₃ being object of b₁ holds b₃ is object of b₂

proof end;

theorem Th7: :: YELLOW18:7

for b₁, b₂ being non empty AltCatStr st b₁,b₂ are_opposite holds
for b₃, b₄ being object of b₁
for b₅, b₆ being object of b₂ st b₅ = b₃ & b₆ = b₄ holds
<^b₃,b₄^> = <^b₆,b₅^>

proof end;

theorem Th8: :: YELLOW18:8

for b₁, b₂ being non empty AltCatStr st b₁,b₂ are_opposite holds
for b₃, b₄ being object of b₁
for b₅, b₆ being object of b₂ st b₅ = b₃ & b₆ = b₄ holds
for b₇ being Morphism of b₃,b₄ holds b₇ is Morphism of b₆,b₅ by Th7;

theorem Th9: :: YELLOW18:9

for b₁, b₂ being non empty transitive AltCatStr holds
( b₁,b₂ are_opposite iff ( the carrier of b₂ = the carrier of b₁ & ( for b₃, b₄, b₅ being object of b₁
for b₆, b₇, b₈ being object of b₂ st b₆ = b₃ & b₇ = b₄ & b₈ = b₅ holds
( <^b₃,b₄^> = <^b₇,b₆^> & ( <^b₃,b₄^> <> {} & <^b₄,b₅^> <> {} implies for b₉ being Morphism of b₃,b₄
for b₁₀ being Morphism of b₄,b₅
for b₁₁ being Morphism of b₇,b₆
for b₁₂ being Morphism of b₈,b₇ st b₁₁ = b₉ & b₁₂ = b₁₀ holds
b₁₁ * b₁₂ = b₁₀ * b₉ ) ) ) ) )

proof end;

theorem Th10: :: YELLOW18:10

for b₁, b₂ being category st b₁,b₂ are_opposite holds
for b₃ being object of b₁
for b₄ being object of b₂ st b₃ = b₄ holds
idm b₃ = idm b₄

proof end;

theorem Th11: :: YELLOW18:11

for b₁ being non empty transitive AltCatStr ex b₂ being non empty transitive strict AltCatStr st b₁,b₂ are_opposite

proof end;

theorem Th12: :: YELLOW18:12

for b₁, b₂ being non empty transitive AltCatStr st b₁,b₂ are_opposite & b₁ is associative holds
b₂ is associative

proof end;

theorem Th13: :: YELLOW18:13

for b₁, b₂ being non empty transitive AltCatStr st b₁,b₂ are_opposite & b₁ is with_units holds
b₂ is with_units

proof end;

theorem Th14: :: YELLOW18:14

for b₁, b₂, b₃ being non empty AltCatStr st b₁,b₂ are_opposite holds
( b₁,b₃ are_opposite iff AltCatStr(# the carrier of b₂,the Arrows of b₂,the Comp of b₂ #) = AltCatStr(# the carrier of b₃,the Arrows of b₃,the Comp of b₃ #) )

proof end;

definition

let c₁ be non empty transitive AltCatStr ;
func c₁ opp -> non empty transitive strict AltCatStr means :Def4: :: YELLOW18:def 4
a₁,a₂ are_opposite ;
uniqueness by Th14;
existence by Th11;

end;

:: deftheorem Def4 defines opp YELLOW18:def 4 :

registration

let c₁ be non empty transitive associative AltCatStr ;
cluster a₁ opp -> non empty transitive strict associative ;
coherence

proof end;

end;

registration

let c₁ be non empty transitive with_units AltCatStr ;
cluster a₁ opp -> non empty transitive strict with_units ;
coherence

proof end;

end;

definition

let c₁, c₂ be category;
assume E16: c₁,c₂ are_opposite ;
deffunc H₁( set ) -> set = a₁;
deffunc H₂( set , set , set ) -> set = a₃;
E17: for b₁ being object of c₁ holds H₁(b₁) is object of c₂ by E16, Def3;

E18: now

let c₃, c₄ be object of c₁;
assume E19: <^c₃,c₄^> <> {} ;
let c₅ be Morphism of c₃,c₄;
reconsider c₆ = c₃, c₇ = c₄ as object of c₂ by E16, Def3;
<^c₃,c₄^> = <^c₇,c₆^> by E16, Th9
.= the Arrows of c₂ . c₄,c₃ ;
hence H₂(c₃,c₄,c₅) in the Arrows of c₂ . H₁(c₄),H₁(c₃) by E19;

end;

E19: for b₁, b₂, b₃ being object of c₁ st <^b₁,b₂^> <> {} & <^b₂,b₃^> <> {} holds
for b₄ being Morphism of b₁,b₂
for b₅ being Morphism of b₂,b₃
for b₆, b₇, b₈ being object of c₂ st b₆ = H₁(b₁) & b₇ = H₁(b₂) & b₈ = H₁(b₃) holds
for b₉ being Morphism of b₇,b₆
for b₁₀ being Morphism of b₈,b₇ st b₉ = H₂(b₁,b₂,b₄) & b₁₀ = H₂(b₂,b₃,b₅) holds
H₂(b₁,b₃,b₅ * b₄) = b₉ * b₁₀ by E16, Th9;
E20: for b₁ being object of c₁
for b₂ being object of c₂ st b₂ = H₁(b₁) holds
H₂(b₁,b₁, idm b₁) = idm b₂ by E16, Th10;
func dualizing-func c₁,c₂ -> strict contravariant Functor of a₁,a₂ means :Def5: :: YELLOW18:def 5
( ( for b₁ being object of a₁ holds a₃ . b₁ = b₁ ) & ( for b₁, b₂ being object of a₁ st <^b₁,b₂^> <> {} holds
for b₃ being Morphism of b₁,b₂ holds a₃ . b₃ = b₃ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines dualizing-func YELLOW18:def 5 :

theorem Th15: :: YELLOW18:15

for b₁, b₂ being category st b₁,b₂ are_opposite holds
(dualizing-func b₁,b₂) * (dualizing-func b₂,b₁) = id b₂

proof end;

theorem Th16: :: YELLOW18:16

for b₁, b₂ being category st b₁,b₂ are_opposite holds
dualizing-func b₁,b₂ is bijective

proof end;

registration

let c₁ be category;
cluster dualizing-func a₁,(a₁ opp ) -> strict contravariant bijective ;
coherence

proof end;

cluster dualizing-func (a₁ opp ),a₁ -> strict contravariant bijective ;
coherence

proof end;

end;

theorem Th17: :: YELLOW18:17

for b₁, b₂ being category st b₁,b₂ are_opposite holds
b₁,b₂ are_anti-isomorphic

proof end;

theorem Th18: :: YELLOW18:18

for b₁, b₂, b₃ being category st b₁,b₂ are_opposite holds
( b₁,b₃ are_isomorphic iff b₂,b₃ are_anti-isomorphic )

proof end;

theorem Th19: :: YELLOW18:19

for b₁, b₂, b₃, b₄ being category st b₁,b₂ are_opposite & b₃,b₄ are_opposite & b₁,b₃ are_isomorphic holds
b₂,b₄ are_isomorphic

proof end;

theorem Th20: :: YELLOW18:20

for b₁, b₂, b₃, b₄ being category st b₁,b₂ are_opposite & b₃,b₄ are_opposite & b₁,b₃ are_anti-isomorphic holds
b₂,b₄ are_anti-isomorphic

proof end;

E20: now

let c₁, c₂ be category;
assume E21: c₁,c₂ are_opposite ;
let c₃, c₄ be object of c₁;
assume E22: ( <^c₃,c₄^> <> {} & <^c₄,c₃^> <> {} ) ;
let c₅, c₆ be object of c₂;
assume E23: ( c₅ = c₃ & c₆ = c₄ ) ;
let c₇ be Morphism of c₃,c₄;
let c₈ be Morphism of c₆,c₅;
assume E24: c₈ = c₇ ;
thus ( c₇ is retraction implies c₈ is coretraction )

proof

given c₉ being Morphism of c₄,c₃ such that E25: c₉ is_right_inverse_of c₇ ; :: according to ALTCAT_3:def 2
reconsider c₁₀ = c₉ as Morphism of c₅,c₆ by E21, E23, Th7;
take c₁₀ ; :: according to ALTCAT_3:def 3
c₇ * c₉ = idm c₄ by E25, ALTCAT_3:def 1
.= idm c₆ by E21, E23, Th10 ;
hence c₁₀ * c₈ = idm c₆ by E21, E22, E23, E24, Th9; :: according to ALTCAT_3:def 1

end;

thus ( c₇ is coretraction implies c₈ is retraction )

proof

given c₉ being Morphism of c₄,c₃ such that E25: c₉ is_left_inverse_of c₇ ; :: according to ALTCAT_3:def 3
reconsider c₁₀ = c₉ as Morphism of c₅,c₆ by E21, E23, Th7;
take c₁₀ ; :: according to ALTCAT_3:def 2
c₉ * c₇ = idm c₃ by E25, ALTCAT_3:def 1
.= idm c₅ by E21, E23, Th10 ;
hence c₈ * c₁₀ = idm c₅ by E21, E22, E23, E24, Th9; :: according to ALTCAT_3:def 1

end;

theorem Th21: :: YELLOW18:21

for b₁, b₂ being category st b₁,b₂ are_opposite holds
for b₃, b₄ being object of b₁ st <^b₃,b₄^> <> {} & <^b₄,b₃^> <> {} holds
for b₅, b₆ being object of b₂ st b₅ = b₃ & b₆ = b₄ holds
for b₇ being Morphism of b₃,b₄
for b₈ being Morphism of b₆,b₅ st b₈ = b₇ holds
( b₇ is retraction iff b₈ is coretraction )

proof end;

theorem Th22: :: YELLOW18:22

proof end;

theorem Th23: :: YELLOW18:23

for b₁, b₂ being category st b₁,b₂ are_opposite holds
for b₃, b₄ being object of b₁ st <^b₃,b₄^> <> {} & <^b₄,b₃^> <> {} holds
for b₅, b₆ being object of b₂ st b₅ = b₃ & b₆ = b₄ holds
for b₇ being Morphism of b₃,b₄
for b₈ being Morphism of b₆,b₅ st b₈ = b₇ & b₇ is retraction & b₇ is coretraction holds
b₈ " = b₇ "

proof end;

theorem Th24: :: YELLOW18:24

proof end;

theorem Th25: :: YELLOW18:25

for b₁, b₂, b₃, b₄ being category st b₁,b₂ are_opposite & b₃,b₄ are_opposite holds
for b₅, b₆ being covariant Functor of b₂,b₃ st b₅,b₆ are_naturally_equivalent holds
((dualizing-func b₃,b₄) * b₆) * (dualizing-func b₁,b₂),((dualizing-func b₃,b₄) * b₅) * (dualizing-func b₁,b₂) are_naturally_equivalent

proof end;

theorem Th26: :: YELLOW18:26

for b₁, b₂, b₃, b₄ being category st b₁,b₂ are_opposite & b₃,b₄ are_opposite & b₁,b₃ are_equivalent holds
b₂,b₄ are_equivalent

proof end;

definition

let c₁, c₂ be category;
pred c₁,c₂ are_dual means :Def6: :: YELLOW18:def 6
a₁,a₂ opp are_equivalent ;
symmetry

proof end;

end;

:: deftheorem Def6 defines are_dual YELLOW18:def 6 :

theorem Th27: :: YELLOW18:27

for b₁, b₂ being category st b₁,b₂ are_anti-isomorphic holds
b₁,b₂ are_dual

proof end;

theorem Th28: :: YELLOW18:28

for b₁, b₂, b₃ being category st b₁,b₂ are_opposite holds
( b₁,b₃ are_equivalent iff b₂,b₃ are_dual )

proof end;

theorem Th29: :: YELLOW18:29

for b₁, b₂, b₃ being category st b₁,b₂ are_dual & b₂,b₃ are_equivalent holds
b₁,b₃ are_dual

proof end;

theorem Th30: :: YELLOW18:30

for b₁, b₂, b₃ being category st b₁,b₂ are_dual & b₂,b₃ are_dual holds
b₁,b₃ are_equivalent

proof end;

theorem Th31: :: YELLOW18:31

for b₁, b₂, b₃ being set holds
( b₃ in Funcs b₁,b₂ iff ( b₃ is Function & proj1 b₃ = b₁ & proj2 b₃ c= b₂ ) )

proof end;

definition

let c₁ be 1-sorted ;
mode ManySortedSet of a₁ is ManySortedSet of the carrier of a₁;

end;

definition

let c₁ be category;
attr a₁ is para-functional means :: YELLOW18:def 7
ex b₁ being ManySortedSet of a₁ st
for b₂, b₃ being object of a₁ holds <^b₂,b₃^> c= Funcs (b₁ . b₂),(b₁ . b₃);

end;

:: deftheorem Def7 defines para-functional YELLOW18:def 7 :

registration

cluster quasi-functional -> para-functional AltCatStr ;
coherence

proof end;

end;

definition

let c₁ be category;
let c₂ be set ;
func c₁ -carrier_of c₂ -> set means :Def8: :: YELLOW18:def 8
ex b₁ being object of a₁ st
( b₁ = a₂ & a₃ = proj1 (idm b₁) ) if a₂ is object of a₁
otherwise a₃ = {} ;
consistency ;
existence

proof end;

uniqueness ;

end;

:: deftheorem Def8 defines -carrier_of YELLOW18:def 8 :

notation

let c₁ be category;
let c₂ be object of c₁;
synonym the_carrier_of c₂ for c₁ -carrier_of c₂;

end;

definition

let c₁ be category;
let c₂ be object of c₁;
redefine func c₁ -carrier_of c₂ -> set equals :: YELLOW18:def 9
proj1 (idm a₂);
compatibility by Def8;

end;

:: deftheorem Def9 defines -carrier_of YELLOW18:def 9 :

theorem Th32: :: YELLOW18:32

for b₁ being non empty set
for b₂ being object of (EnsCat b₁) holds idm b₂ = id b₂

proof end;

theorem Th33: :: YELLOW18:33

for b₁ being non empty set
for b₂ being object of (EnsCat b₁) holds the_carrier_of b₂ = b₂

proof end;

definition

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

end;

:: deftheorem Def10 defines set-id-inheriting YELLOW18:def 10 :

registration

let c₁ be non empty set ;
cluster EnsCat a₁ -> para-functional set-id-inheriting ;
coherence

proof end;

end;

definition

let c₁ be category;
attr a₁ is concrete means :Def11: :: YELLOW18:def 11
( a₁ is para-functional & a₁ is semi-functional & a₁ is set-id-inheriting );

end;

:: deftheorem Def11 defines concrete YELLOW18:def 11 :

registration

cluster concrete -> semi-functional para-functional set-id-inheriting AltCatStr ;
coherence by Def11;
cluster semi-functional para-functional set-id-inheriting -> concrete AltCatStr ;
coherence by Def11;

end;

registration

cluster strict quasi-functional semi-functional para-functional set-id-inheriting concrete AltCatStr ;
existence

proof end;

end;

theorem Th34: :: YELLOW18:34

for b₁ being category holds
( b₁ is para-functional iff for b₂, b₃ being object of b₁ holds <^b₂,b₃^> c= Funcs (the_carrier_of b₂),(the_carrier_of b₃) )

proof end;

theorem Th35: :: YELLOW18:35

for b₁ being para-functional category
for b₂, b₃ being object of b₁ st <^b₂,b₃^> <> {} holds
for b₄ being Morphism of b₂,b₃ holds b₄ is Function of the_carrier_of b₂, the_carrier_of b₃

proof end;

registration

let c₁ be para-functional category;
let c₂, c₃ be object of c₁;
cluster -> Relation-like Function-like Element of <^a₂,a₃^>;
coherence

proof end;

end;

theorem Th36: :: YELLOW18:36

for b₁ being para-functional category
for b₂, b₃ being object of b₁ st <^b₂,b₃^> <> {} holds
for b₄ being Morphism of b₂,b₃ holds
( dom b₄ = the_carrier_of b₂ & rng b₄ c= the_carrier_of b₃ )

proof end;

theorem Th37: :: YELLOW18:37

for b₁ being semi-functional para-functional category
for b₂ being object of b₁ holds the_carrier_of b₂ = dom (idm b₂) by FUNCT_5:21;

theorem Th38: :: YELLOW18:38

for b₁ being semi-functional para-functional category
for b₂, b₃, b₄ being object of b₁ st <^b₂,b₃^> <> {} & <^b₃,b₄^> <> {} holds
for b₅ being Morphism of b₂,b₃
for b₆ being Morphism of b₃,b₄ holds b₆ * b₅ = b₆ * b₅

proof end;

theorem Th39: :: YELLOW18:39

for b₁ being semi-functional para-functional category
for b₂ being object of b₁ st id (the_carrier_of b₂) in <^b₂,b₂^> holds
idm b₂ = id (the_carrier_of b₂)

proof end;

scheme :: YELLOW18:sch 16
s16{ F₁() -> non empty set , F₂( set , set ) -> set , F₃( set ) -> set } :

ex b₁ being strict concrete category st
( the carrier of b₁ = F₁() & ( for b₂ being object of b₁ holds the_carrier_of b₂ = F₃(b₂) ) & ( for b₂, b₃ being object of b₁ holds <^b₂,b₃^> = F₂(b₂,b₃) ) )

provided

E37: for b₁, b₂, b₃ being Element of F₁()
for b₄, b₅ being Function st b₄ in F₂(b₁,b₂) & b₅ in F₂(b₂,b₃) holds
b₅ * b₄ in F₂(b₁,b₃) and
E38: for b₁, b₂ being Element of F₁() holds F₂(b₁,b₂) c= Funcs F₃(b₁),F₃(b₂) and
E39: for b₁ being Element of F₁() holds id F₃(b₁) in F₂(b₁,b₁)

proof end;

scheme :: YELLOW18:sch 17
s17{ F₁() -> non empty set , P₁[ set , set , set ], F₂( set ) -> set } :

ex b₁ being strict concrete category st
( the carrier of b₁ = F₁() & ( for b₂ being object of b₁ holds the_carrier_of b₂ = F₂(b₂) ) & ( for b₂, b₃ being Element of F₁()
for b₄ being Function holds
( b₄ in the Arrows of b₁ . b₂,b₃ iff ( b₄ in Funcs F₂(b₂),F₂(b₃) & P₁[b₂,b₃,b₄] ) ) ) )

provided

E37: for b₁, b₂, b₃ being Element of F₁()
for b₄, b₅ being Function st P₁[b₁,b₂,b₄] & P₁[b₂,b₃,b₅] holds
P₁[b₁,b₃,b₅ * b₄] and
E38: for b₁ being Element of F₁() holds P₁[b₁,b₁, id F₂(b₁)]

proof end;

scheme :: YELLOW18:sch 18
s18{ F₁() -> non empty set , F₂( set ) -> set , P₁[ set , set ], P₂[ set , set , set ] } :

ex b₁ being strict concrete category st
( the carrier of b₁ = F₁() & ( for b₂ being object of b₁
for b₃ being set holds
( b₃ in the_carrier_of b₂ iff ( b₃ in F₂(b₂) & P₁[b₂,b₃] ) ) ) & ( for b₂, b₃ being Element of F₁()
for b₄ being Function holds
( b₄ in the Arrows of b₁ . b₂,b₃ iff ( b₄ in Funcs (b₁ -carrier_of b₂),(b₁ -carrier_of b₃) & P₂[b₂,b₃,b₄] ) ) ) )

provided

E37: for b₁, b₂, b₃ being Element of F₁()
for b₄, b₅ being Function st P₂[b₁,b₂,b₄] & P₂[b₂,b₃,b₅] holds
P₂[b₁,b₃,b₅ * b₄] and
E38: for b₁ being Element of F₁()
for b₂ being set st ( for b₃ being set holds
( b₃ in b₂ iff ( b₃ in F₂(b₁) & P₁[b₁,b₃] ) ) ) holds
P₂[b₁,b₁, id b₂]

proof end;

scheme :: YELLOW18:sch 19
s19{ F₁() -> non empty set , F₂( set , set ) -> set } :

for b₁, b₂ being semi-functional para-functional category st the carrier of b₁ = F₁() & ( for b₃, b₄ being object of b₁ holds <^b₃,b₄^> = F₂(b₃,b₄) ) & the carrier of b₂ = F₁() & ( for b₃, b₄ being object of b₂ holds <^b₃,b₄^> = F₂(b₃,b₄) ) holds
AltCatStr(# the carrier of b₁,the Arrows of b₁,the Comp of b₁ #) = AltCatStr(# the carrier of b₂,the Arrows of b₂,the Comp of b₂ #)

proof end;

scheme :: YELLOW18:sch 20
s20{ F₁() -> non empty set , P₁[ set , set , set ], F₂( set ) -> set } :

for b₁, b₂ being semi-functional para-functional category st the carrier of b₁ = F₁() & ( for b₃, b₄ being Element of F₁()
for b₅ being Function holds
( b₅ in the Arrows of b₁ . b₃,b₄ iff ( b₅ in Funcs F₂(b₃),F₂(b₄) & P₁[b₃,b₄,b₅] ) ) ) & the carrier of b₂ = F₁() & ( for b₃, b₄ being Element of F₁()
for b₅ being Function holds
( b₅ in the Arrows of b₂ . b₃,b₄ iff ( b₅ in Funcs F₂(b₃),F₂(b₄) & P₁[b₃,b₄,b₅] ) ) ) holds
AltCatStr(# the carrier of b₁,the Arrows of b₁,the Comp of b₁ #) = AltCatStr(# the carrier of b₂,the Arrows of b₂,the Comp of b₂ #)

proof end;

scheme :: YELLOW18:sch 21
s21{ F₁() -> non empty set , F₂( set ) -> set , P₁[ set , set ], P₂[ set , set , set ] } :

for b₁, b₂ being semi-functional para-functional category st the carrier of b₁ = F₁() & ( for b₃ being object of b₁
for b₄ being set holds
( b₄ in the_carrier_of b₃ iff ( b₄ in F₂(b₃) & P₁[b₃,b₄] ) ) ) & ( for b₃, b₄ being Element of F₁()
for b₅ being Function holds
( b₅ in the Arrows of b₁ . b₃,b₄ iff ( b₅ in Funcs (b₁ -carrier_of b₃),(b₁ -carrier_of b₄) & P₂[b₃,b₄,b₅] ) ) ) & the carrier of b₂ = F₁() & ( for b₃ being object of b₂
for b₄ being set holds
( b₄ in the_carrier_of b₃ iff ( b₄ in F₂(b₃) & P₁[b₃,b₄] ) ) ) & ( for b₃, b₄ being Element of F₁()
for b₅ being Function holds
( b₅ in the Arrows of b₂ . b₃,b₄ iff ( b₅ in Funcs (b₂ -carrier_of b₃),(b₂ -carrier_of b₄) & P₂[b₃,b₄,b₅] ) ) ) holds
AltCatStr(# the carrier of b₁,the Arrows of b₁,the Comp of b₁ #) = AltCatStr(# the carrier of b₂,the Arrows of b₂,the Comp of b₂ #)

proof end;

theorem Th40: :: YELLOW18:40

for b₁ being concrete category
for b₂, b₃ being object of b₁ st <^b₂,b₃^> <> {} & <^b₃,b₂^> <> {} holds
for b₄ being Morphism of b₂,b₃ st b₄ is retraction holds
rng b₄ = the_carrier_of b₃

proof end;

theorem Th41: :: YELLOW18:41

for b₁ being concrete category
for b₂, b₃ being object of b₁ st <^b₂,b₃^> <> {} & <^b₃,b₂^> <> {} holds
for b₄ being Morphism of b₂,b₃ st b₄ is coretraction holds
b₄ is one-to-one

proof end;

theorem Th42: :: YELLOW18:42

for b₁ being concrete category
for b₂, b₃ being object of b₁ st <^b₂,b₃^> <> {} & <^b₃,b₂^> <> {} holds
for b₄ being Morphism of b₂,b₃ st b₄ is iso holds
( b₄ is one-to-one & rng b₄ = the_carrier_of b₃ )

proof end;

theorem Th43: :: YELLOW18:43

for b₁ being semi-functional para-functional category
for b₂, b₃ being object of b₁ st <^b₂,b₃^> <> {} holds
for b₄ being Morphism of b₂,b₃ st b₄ is one-to-one & b₄ " in <^b₃,b₂^> holds
b₄ is iso

proof end;

theorem Th44: :: YELLOW18:44

for b₁ being concrete category
for b₂, b₃ being object of b₁ st <^b₂,b₃^> <> {} & <^b₃,b₂^> <> {} holds
for b₄ being Morphism of b₂,b₃ st b₄ is iso holds
b₄ " = b₄ "

proof end;

scheme :: YELLOW18:sch 22
s22{ F₁() -> semi-functional para-functional category, F₂() -> semi-functional para-functional category, F₃( set ) -> set , F₄( set ) -> set , F₅( set , set , set ) -> Function, F₆( set , set , set ) -> Function, F₇( set ) -> Function, F₈( set ) -> Function } :

F₁(),F₂() are_equivalent

provided

E41: ex b₁ being covariant Functor of F₁(),F₂() st
( ( for b₂ being object of F₁() holds b₁ . b₂ = F₃(b₂) ) & ( for b₂, b₃ being object of F₁() st <^b₂,b₃^> <> {} holds
for b₄ being Morphism of b₂,b₃ holds b₁ . b₄ = F₅(b₂,b₃,b₄) ) ) and
E42: ex b₁ being covariant Functor of F₂(),F₁() st
( ( for b₂ being object of F₂() holds b₁ . b₂ = F₄(b₂) ) & ( for b₂, b₃ being object of F₂() st <^b₂,b₃^> <> {} holds
for b₄ being Morphism of b₂,b₃ holds b₁ . b₄ = F₆(b₂,b₃,b₄) ) ) and
E43: for b₁, b₂ being object of F₁() st b₁ = F₄(F₃(b₂)) holds
( F₇(b₂) in <^b₁,b₂^> & F₇(b₂) " in <^b₂,b₁^> & F₇(b₂) is one-to-one ) and
E44: for b₁, b₂ being object of F₂() st b₂ = F₃(F₄(b₁)) holds
( F₈(b₁) in <^b₁,b₂^> & F₈(b₁) " in <^b₂,b₁^> & F₈(b₁) is one-to-one ) and
E45: for b₁, b₂ being object of F₁() st <^b₁,b₂^> <> {} holds
for b₃ being Morphism of b₁,b₂ holds F₇(b₂) * F₆(F₃(b₁),F₃(b₂),F₅(b₁,b₂,b₃)) = b₃ * F₇(b₁) and
E46: for b₁, b₂ being object of F₂() st <^b₁,b₂^> <> {} holds
for b₃ being Morphism of b₁,b₂ holds F₅(F₄(b₁),F₄(b₂),F₆(b₁,b₂,b₃)) * F₈(b₁) = F₈(b₂) * b₃

proof end;

definition

let c₁ be category;
defpred S₁[ set , set ] means a₁ = a₂ `22 ;
defpred S₂[ set , set , Function] means ex b₁, b₂ being object of c₁ex b₃ being Morphism of b₁,b₂ st
( b₁ = a₁ & b₂ = a₂ & <^b₁,b₂^> <> {} & ( for b₄ being object of c₁ st <^b₄,b₁^> <> {} holds
for b₅ being Morphism of b₄,b₁ holds a₃ . [b₅,[b₄,b₁]] = [(b₃ * b₅),[b₄,b₂]] ) );
deffunc H₁( set ) -> set = Union (disjoin the Arrows of c₁);
E41: for b₁, b₂, b₃ being Element of c₁
for b₄, b₅ being Function st S₂[b₁,b₂,b₄] & S₂[b₂,b₃,b₅] holds
S₂[b₁,b₃,b₅ * b₄]

proof end;

E42: for b₁ being Element of c₁
for b₂ being set st ( for b₃ being set holds
( b₃ in b₂ iff ( b₃ in H₁(b₁) & S₁[b₁,b₃] ) ) ) holds
S₂[b₁,b₁, id b₂]

proof end;

func Concretized c₁ -> strict concrete category means :Def12: :: YELLOW18:def 12
( the carrier of a₂ = the carrier of a₁ & ( for b₁ being object of a₂
for b₂ being set holds
( b₂ in the_carrier_of b₁ iff ( b₂ in Union (disjoin the Arrows of a₁) & b₁ = b₂ `22 ) ) ) & ( for b₁, b₂ being Element of a₁
for b₃ being Function holds
( b₃ in the Arrows of a₂ . b₁,b₂ iff ( b₃ in Funcs (a₂ -carrier_of b₁),(a₂ -carrier_of b₂) & ex b₄, b₅ being object of a₁ex b₆ being Morphism of b₄,b₅ st
( b₄ = b₁ & b₅ = b₂ & <^b₄,b₅^> <> {} & ( for b₇ being object of a₁ st <^b₇,b₄^> <> {} holds
for b₈ being Morphism of b₇,b₄ holds b₃ . [b₈,[b₇,b₄]] = [(b₆ * b₈),[b₇,b₅]] ) ) ) ) ) );
uniqueness

proof end;

existence

proof end;

end;

:: deftheorem Def12 defines Concretized YELLOW18:def 12 :

theorem Th45: :: YELLOW18:45

for b₁ being category
for b₂ being object of b₁
for b₃ being set holds
( b₃ in (Concretized b₁) -carrier_of b₂ iff ex b₄ being object of b₁ex b₅ being Morphism of b₄,b₂ st
( <^b₄,b₂^> <> {} & b₃ = [b₅,[b₄,b₂]] ) )

proof end;

registration

let c₁ be category;
let c₂ be object of c₁;
cluster (Concretized a₁) -carrier_of a₂ -> non empty ;
coherence

proof end;

end;

theorem Th46: :: YELLOW18:46

for b₁ being category
for b₂, b₃ being object of b₁ st <^b₂,b₃^> <> {} holds
for b₄ being Morphism of b₂,b₃ ex b₅ being Function of (Concretized b₁) -carrier_of b₂,(Concretized b₁) -carrier_of b₃ st
( b₅ in the Arrows of (Concretized b₁) . b₂,b₃ & ( for b₆ being object of b₁
for b₇ being Morphism of b₆,b₂ st <^b₆,b₂^> <> {} holds
b₅ . [b₇,[b₆,b₂]] = [(b₄ * b₇),[b₆,b₃]] ) )

proof end;

theorem Th47: :: YELLOW18:47

for b₁ being category
for b₂, b₃ being object of b₁ st <^b₂,b₃^> <> {} holds
for b₄, b₅ being Function st b₄ in the Arrows of (Concretized b₁) . b₂,b₃ & b₅ in the Arrows of (Concretized b₁) . b₂,b₃ & b₄ . [(idm b₂),[b₂,b₂]] = b₅ . [(idm b₂),[b₂,b₂]] holds
b₄ = b₅

proof end;

scheme :: YELLOW18:sch 23
s23{ F₁() -> set , F₂() -> ManySortedSet of F₁(), F₃() -> ManySortedSet of F₁(), P₁[ set , set , set ] } :

ex b₁ being ManySortedFunction of F₂(),F₃() st
for b₂, b₃ being set st b₂ in F₁() & b₃ in F₂() . b₂ holds
( (b₁ . b₂) . b₃ in F₃() . b₂ & P₁[b₂,b₃,(b₁ . b₂) . b₃] )

provided

E45: for b₁, b₂ being set st b₁ in F₁() & b₂ in F₂() . b₁ holds
ex b₃ being set st
( b₃ in F₃() . b₁ & P₁[b₁,b₂,b₃] )

proof end;

definition

let c₁ be category;
set c₂ = Concretized c₁;
func Concretization c₁ -> strict covariant Functor of a₁, Concretized a₁ means :Def13: :: YELLOW18:def 13
( ( for b₁ being object of a₁ holds a₂ . b₁ = b₁ ) & ( for b₁, b₂ being object of a₁ st <^b₁,b₂^> <> {} holds
for b₃ being Morphism of b₁,b₂ holds (a₂ . b₃) . [(idm b₁),[b₁,b₁]] = [b₃,[b₁,b₂]] ) );
uniqueness

proof end;

existence

proof end;

end;

:: deftheorem Def13 defines Concretization YELLOW18:def 13 :

registration

let c₁ be category;
cluster Concretization a₁ -> strict covariant bijective ;
coherence

proof end;

end;

theorem Th48: :: YELLOW18:48

for b₁ being category holds b₁, Concretized b₁ are_isomorphic

proof end;