:: FUNCTOR0 semantic presentation

scheme :: FUNCTOR0:sch 1
s1{ F₁() -> non empty set , F₂() -> Function, F₃() -> Element of F₁(), F₄() -> Element of F₁(), F₅( set , set ) -> set , P₁[ set , set ] } :

F₂() . F₃(),F₄() = F₅(F₃(),F₄())

provided

E1: F₂() = { [[b₁,b₂],F₅(b₁,b₂)] where B is Element of F₁(), B is Element of F₁() : P₁[b₁,b₂] } and
E2: P₁[F₃(),F₄()]

proof end;

theorem Th1: :: FUNCTOR0:1

for b₁ being set holds {} is Function of b₁, {}

proof end;

theorem Th2: :: FUNCTOR0:2

canceled;

theorem Th3: :: FUNCTOR0:3

for b₁ being set
for b₂ being ManySortedSet of b₁ holds b₂ * (id b₁) = b₂

proof end;

registration

let c₁ be empty Function;
cluster ~ a₁ -> empty ;
coherence

proof end;

let c₂ be Function;
cluster [:a₁,a₂:] -> empty ;
coherence

proof end;

cluster [:a₂,a₁:] -> empty ;
coherence

proof end;

end;

theorem Th4: :: FUNCTOR0:4

for b₁ being set
for b₂ being Function holds b₂ .: (id b₁) = (~ b₂) .: (id b₁)

proof end;

theorem Th5: :: FUNCTOR0:5

for b₁, b₂ being set
for b₃ being Function of b₁,b₂ holds
( b₃ is onto iff [:b₃,b₃:] is onto )

proof end;

registration

let c₁ be Function-yielding Function;
cluster ~ a₁ -> Function-yielding ;
coherence ;

end;

theorem Th6: :: FUNCTOR0:6

for b₁, b₂, b₃ being set holds ~ ([:b₁,b₂:] --> b₃) = [:b₂,b₁:] --> b₃

proof end;

theorem Th7: :: FUNCTOR0:7

for b₁, b₂ being Function st b₁ is one-to-one & b₂ is one-to-one holds
[:b₁,b₂:] " = [:(b₁ " ),(b₂ " ):]

proof end;

theorem Th8: :: FUNCTOR0:8

for b₁ being Function st [:b₁,b₁:] is one-to-one holds
b₁ is one-to-one

proof end;

theorem Th9: :: FUNCTOR0:9

for b₁ being Function st b₁ is one-to-one holds
~ b₁ is one-to-one

proof end;

theorem Th10: :: FUNCTOR0:10

for b₁, b₂ being Function st ~ [:b₁,b₂:] is one-to-one holds
[:b₂,b₁:] is one-to-one

proof end;

theorem Th11: :: FUNCTOR0:11

for b₁, b₂ being Function st b₁ is one-to-one & b₂ is one-to-one holds
(~ [:b₁,b₂:]) " = ~ ([:b₂,b₁:] " )

proof end;

theorem Th12: :: FUNCTOR0:12

for b₁, b₂ being set
for b₃ being Function of b₁,b₂ st b₃ is onto holds
id b₂ c= [:b₃,b₃:] .: (id b₁)

proof end;

theorem Th13: :: FUNCTOR0:13

for b₁, b₂ being Function-yielding Function
for b₃ being Function holds (b₂ ** b₁) * b₃ = (b₂ * b₃) ** (b₁ * b₃)

proof end;

definition

let c₁, c₂, c₃ be set ;
let c₄ be Function of [:c₁,c₂:],c₃;
redefine func ~ as ~ c₄ -> Function of [:a₂,a₁:],a₃;
coherence

proof end;

end;

theorem Th14: :: FUNCTOR0:14

for b₁, b₂, b₃ being set
for b₄ being Function of [:b₁,b₂:],b₃ st ~ b₄ is onto holds
b₄ is onto

proof end;

theorem Th15: :: FUNCTOR0:15

for b₁ being set
for b₂ being non empty set
for b₃ being Function of b₁,b₂ holds [:b₃,b₃:] .: (id b₁) c= id b₂

proof end;

definition

let c₁, c₂ be set ;
mode bifunction of a₁,a₂ is Function of [:a₁,a₁:],[:a₂,a₂:];

end;

definition

let c₁, c₂ be set ;
let c₃ be bifunction of c₁,c₂;
canceled;
attr a₃ is Covariant means :Def2: :: FUNCTOR0:def 2
ex b₁ being Function of a₁,a₂ st a₃ = [:b₁,b₁:];
attr a₃ is Contravariant means :Def3: :: FUNCTOR0:def 3
ex b₁ being Function of a₁,a₂ st a₃ = ~ [:b₁,b₁:];

end;

:: deftheorem Def1 FUNCTOR0:def 1 :

:: deftheorem Def2 defines Covariant FUNCTOR0:def 2 :

:: deftheorem Def3 defines Contravariant FUNCTOR0:def 3 :

theorem Th16: :: FUNCTOR0:16

for b₁ being set
for b₂ being non empty set
for b₃ being Element of b₂
for b₄ being bifunction of b₁,b₂ st b₄ = [:b₁,b₁:] --> [b₃,b₃] holds
( b₄ is Covariant & b₄ is Contravariant )

proof end;

registration

let c₁, c₂ be set ;
cluster Covariant Contravariant Relation of [:a₁,a₁:],[:a₂,a₂:];
existence

proof end;

end;

theorem Th17: :: FUNCTOR0:17

for b₁, b₂ being non empty set
for b₃ being Covariant Contravariant bifunction of b₁,b₂ ex b₄ being Element of b₂ st b₃ = [:b₁,b₁:] --> [b₄,b₄]

proof end;

definition

let c₁, c₂ be set ;
let c₃ be Function of c₁,c₂;
let c₄ be ManySortedSet of c₁;
let c₅ be ManySortedSet of c₂;
mode MSUnTrans of c₃,c₄,c₅ -> ManySortedSet of a₁ means :Def4: :: FUNCTOR0:def 4
ex b₁ being non empty set ex b₂ being ManySortedSet of b₁ex b₃ being Function of a₁,b₁ st
( a₃ = b₃ & a₅ = b₂ & a₆ is ManySortedFunction of a₄,b₂ * b₃ ) if a₂ <> {}
otherwise a₆ = [0] a₁;
existence

proof end;

consistency ;

end;

:: deftheorem Def4 defines MSUnTrans FUNCTOR0:def 4 :

definition

let c₁ be set ;
let c₂ be non empty set ;
let c₃ be Function of c₁,c₂;
let c₄ be ManySortedSet of c₁;
let c₅ be ManySortedSet of c₂;
redefine mode MSUnTrans of c₃,c₄,c₅ -> ManySortedSet of a₁ means :Def5: :: FUNCTOR0:def 5
a₆ is ManySortedFunction of a₄,a₅ * a₃;
compatibility

proof end;

end;

:: deftheorem Def5 defines MSUnTrans FUNCTOR0:def 5 :

registration

let c₁, c₂ be set ;
let c₃ be Function of c₁,c₂;
let c₄ be ManySortedSet of c₁;
let c₅ be ManySortedSet of c₂;
cluster -> Function-yielding MSUnTrans of a₃,a₄,a₅;
coherence

proof end;

end;

theorem Th18: :: FUNCTOR0:18

for b₁ being set
for b₂, b₃ being non empty set
for b₄ being Function of b₁,b₂
for b₅ being Function of b₂,b₃
for b₆ being ManySortedSet of b₂
for b₇ being ManySortedSet of b₃
for b₈ being MSUnTrans of b₅,b₆,b₇ holds b₈ * b₄ is MSUnTrans of b₅ * b₄,b₆ * b₄,b₇

proof end;

definition

let c₁ be set ;
let c₂ be non empty set ;
let c₃ be Function of c₁,c₂;
let c₄ be ManySortedSet of [:c₁,c₁:];
let c₅ be ManySortedSet of [:c₂,c₂:];
let c₆ be MSUnTrans of [:c₃,c₃:],c₄,c₅;
redefine func ~ as ~ c₆ -> MSUnTrans of [:a₃,a₃:], ~ a₄, ~ a₅;
coherence

proof end;

end;

theorem Th19: :: FUNCTOR0:19

for b₁, b₂ being non empty set
for b₃ being ManySortedSet of b₁
for b₄ being ManySortedSet of b₂
for b₅ being Element of b₂ st b₄ . b₅ <> {} holds
for b₆ being Element of b₄ . b₅
for b₇ being Function of b₁,b₂ st b₇ = b₁ --> b₅ holds
{ [b₈,((b₃ . b₈) --> b₆)] where B is Element of b₁ : verum } is MSUnTrans of b₇,b₃,b₄

proof end;

theorem Th20: :: FUNCTOR0:20

for b₁ being set
for b₂, b₃ being non empty set
for b₄ being Function of b₁,b₂
for b₅ being Function of b₂,b₃
for b₆ being ManySortedSet of b₁
for b₇ being ManySortedSet of b₂
for b₈ being ManySortedSet of b₃
for b₉ being MSUnTrans of b₄,b₆,b₇
for b₁₀ being MSUnTrans of b₅ * b₄,b₇ * b₄,b₈ st ( for b₁₁ being set st b₁₁ in b₁ & (b₇ * b₄) . b₁₁ = {} & not b₆ . b₁₁ = {} holds
(b₈ * (b₅ * b₄)) . b₁₁ = {} ) holds
b₁₀ ** b₉ is MSUnTrans of b₅ * b₄,b₆,b₈

proof end;

definition

let c₁, c₂ be 1-sorted ;
attr a₃ is strict;
struct BimapStr of c₁,c₂ -> ;
aggr BimapStr(# ObjectMap #) -> BimapStr of a₁,a₂;
sel ObjectMap c₃ -> bifunction of the carrier of a₁,the carrier of a₂;

end;

definition

let c₁, c₂ be non empty AltGraph ;
let c₃ be BimapStr of c₁,c₂;
let c₄ be object of c₁;
func c₃ . c₄ -> object of a₂ equals :: FUNCTOR0:def 6
(the ObjectMap of a₃ . a₄,a₄) `1 ;
coherence by MCART_1:10;

end;

:: deftheorem Def6 defines . FUNCTOR0:def 6 :

definition

let c₁, c₂ be 1-sorted ;
let c₃ be BimapStr of c₁,c₂;
attr a₃ is one-to-one means :Def7: :: FUNCTOR0:def 7
the ObjectMap of a₃ is one-to-one;
attr a₃ is onto means :Def8: :: FUNCTOR0:def 8
the ObjectMap of a₃ is onto;
attr a₃ is reflexive means :Def9: :: FUNCTOR0:def 9
the ObjectMap of a₃ .: (id the carrier of a₁) c= id the carrier of a₂;
attr a₃ is coreflexive means :Def10: :: FUNCTOR0:def 10
id the carrier of a₂ c= the ObjectMap of a₃ .: (id the carrier of a₁);

end;

:: deftheorem Def7 defines one-to-one FUNCTOR0:def 7 :

:: deftheorem Def8 defines onto FUNCTOR0:def 8 :

:: deftheorem Def9 defines reflexive FUNCTOR0:def 9 :

:: deftheorem Def10 defines coreflexive FUNCTOR0:def 10 :

definition

let c₁, c₂ be non empty AltGraph ;
let c₃ be BimapStr of c₁,c₂;
redefine attr a₃ is reflexive means :Def11: :: FUNCTOR0:def 11
for b₁ being object of a₁ holds the ObjectMap of a₃ . b₁,b₁ = [(a₃ . b₁),(a₃ . b₁)];
compatibility

proof end;

end;

:: deftheorem Def11 defines reflexive FUNCTOR0:def 11 :

theorem Th21: :: FUNCTOR0:21

for b₁, b₂ being non empty reflexive AltGraph
for b₃ being BimapStr of b₁,b₂ st b₃ is coreflexive holds
for b₄ being object of b₂ ex b₅ being object of b₁ st b₃ . b₅ = b₄

proof end;

definition

let c₁, c₂ be non empty AltGraph ;
let c₃ be BimapStr of c₁,c₂;
attr a₃ is feasible means :Def12: :: FUNCTOR0:def 12
for b₁, b₂ being object of a₁ st <^b₁,b₂^> <> {} holds
the Arrows of a₂ . (the ObjectMap of a₃ . b₁,b₂) <> {} ;

end;

:: deftheorem Def12 defines feasible FUNCTOR0:def 12 :

definition

let c₁, c₂ be AltGraph ;
attr a₃ is strict;
struct FunctorStr of c₁,c₂ -> BimapStr of a₁,a₂;
aggr FunctorStr(# ObjectMap, MorphMap #) -> FunctorStr of a₁,a₂;
sel MorphMap c₃ -> MSUnTrans of the ObjectMap of a₃,the Arrows of a₁,the Arrows of a₂;

end;

definition

let c₁, c₂ be 1-sorted ;
let c₃ be BimapStr of c₁,c₂;
attr a₃ is Covariant means :Def13: :: FUNCTOR0:def 13
the ObjectMap of a₃ is Covariant;
attr a₃ is Contravariant means :Def14: :: FUNCTOR0:def 14
the ObjectMap of a₃ is Contravariant;

end;

:: deftheorem Def13 defines Covariant FUNCTOR0:def 13 :

:: deftheorem Def14 defines Contravariant FUNCTOR0:def 14 :

registration

let c₁, c₂ be AltGraph ;
cluster Covariant FunctorStr of a₁,a₂;
existence

proof end;

cluster Contravariant FunctorStr of a₁,a₂;
existence

proof end;

end;

definition

let c₁, c₂ be AltGraph ;
let c₃ be FunctorStr of c₁,c₂;
let c₄, c₅ be object of c₁;
func Morph-Map c₃,c₄,c₅ -> set equals :: FUNCTOR0:def 15
the MorphMap of a₃ . a₄,a₅;
correctness ;

end;

:: deftheorem Def15 defines Morph-Map FUNCTOR0:def 15 :

registration

let c₁, c₂ be AltGraph ;
let c₃ be FunctorStr of c₁,c₂;
let c₄, c₅ be object of c₁;
cluster Morph-Map a₃,a₄,a₅ -> Relation-like Function-like ;
coherence

proof end;

end;

definition

let c₁, c₂ be non empty AltGraph ;
let c₃ be Covariant FunctorStr of c₁,c₂;
let c₄, c₅ be object of c₁;
redefine func Morph-Map as Morph-Map c₃,c₄,c₅ -> Function of <^a₄,a₅^>,<^(a₃ . a₄),(a₃ . a₅)^>;
coherence

proof end;

end;

definition

let c₁, c₂ be non empty AltGraph ;
let c₃ be Covariant FunctorStr of c₁,c₂;
let c₄, c₅ be object of c₁;
assume E32: ( <^c₄,c₅^> <> {} & <^(c₃ . c₄),(c₃ . c₅)^> <> {} ) ;
let c₆ be Morphism of c₄,c₅;
func c₃ . c₆ -> Morphism of (a₃ . a₄),(a₃ . a₅) equals :Def16: :: FUNCTOR0:def 16
(Morph-Map a₃,a₄,a₅) . a₆;
coherence

proof end;

end;

:: deftheorem Def16 defines . FUNCTOR0:def 16 :

definition

let c₁, c₂ be non empty AltGraph ;
let c₃ be Contravariant FunctorStr of c₁,c₂;
let c₄, c₅ be object of c₁;
redefine func Morph-Map as Morph-Map c₃,c₄,c₅ -> Function of <^a₄,a₅^>,<^(a₃ . a₅),(a₃ . a₄)^>;
coherence

proof end;

end;

definition

let c₁, c₂ be non empty AltGraph ;
let c₃ be Contravariant FunctorStr of c₁,c₂;
let c₄, c₅ be object of c₁;
assume E33: ( <^c₄,c₅^> <> {} & <^(c₃ . c₅),(c₃ . c₄)^> <> {} ) ;
let c₆ be Morphism of c₄,c₅;
func c₃ . c₆ -> Morphism of (a₃ . a₅),(a₃ . a₄) equals :Def17: :: FUNCTOR0:def 17
(Morph-Map a₃,a₄,a₅) . a₆;
coherence

proof end;

end;

:: deftheorem Def17 defines . FUNCTOR0:def 17 :

definition

let c₁, c₂ be non empty AltGraph ;
let c₃ be object of c₂;
assume E34: <^c₃,c₃^> <> {} ;
let c₄ be Morphism of c₃,c₃;
func c₁ --> c₄ -> strict FunctorStr of a₁,a₂ means :Def18: :: FUNCTOR0:def 18
( the ObjectMap of a₅ = [:the carrier of a₁,the carrier of a₁:] --> [a₃,a₃] & the MorphMap of a₅ = { [[b₁,b₂],(<^b₁,b₂^> --> a₄)] where B is object of a₁, B is object of a₁ : verum } );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def18 defines --> FUNCTOR0:def 18 :

theorem Th22: :: FUNCTOR0:22

for b₁, b₂ being non empty AltGraph
for b₃ being object of b₂ st <^b₃,b₃^> <> {} holds
for b₄ being Morphism of b₃,b₃
for b₅ being object of b₁ holds (b₁ --> b₄) . b₅ = b₃

proof end;

registration

let c₁ be non empty AltGraph ;
let c₂ be non empty reflexive AltGraph ;
let c₃ be object of c₂;
let c₄ be Morphism of c₃,c₃;
cluster a₁ --> a₄ -> feasible strict Covariant Contravariant ;
coherence

proof end;

end;

registration

let c₁ be non empty AltGraph ;
let c₂ be non empty reflexive AltGraph ;
cluster feasible Covariant Contravariant FunctorStr of a₁,a₂;
existence

proof end;

end;

theorem Th23: :: FUNCTOR0:23

for b₁, b₂ being non empty AltGraph
for b₃ being Covariant FunctorStr of b₁,b₂
for b₄, b₅ being object of b₁ holds the ObjectMap of b₃ . b₄,b₅ = [(b₃ . b₄),(b₃ . b₅)]

proof end;

definition

let c₁, c₂ be non empty AltGraph ;
let c₃ be Covariant FunctorStr of c₁,c₂;
redefine attr a₃ is feasible means :Def19: :: FUNCTOR0:def 19
for b₁, b₂ being object of a₁ st <^b₁,b₂^> <> {} holds
<^(a₃ . b₁),(a₃ . b₂)^> <> {} ;
compatibility

proof end;

end;

:: deftheorem Def19 defines feasible FUNCTOR0:def 19 :

theorem Th24: :: FUNCTOR0:24

for b₁, b₂ being non empty AltGraph
for b₃ being Contravariant FunctorStr of b₁,b₂
for b₄, b₅ being object of b₁ holds the ObjectMap of b₃ . b₄,b₅ = [(b₃ . b₅),(b₃ . b₄)]

proof end;

definition

let c₁, c₂ be non empty AltGraph ;
let c₃ be Contravariant FunctorStr of c₁,c₂;
redefine attr a₃ is feasible means :Def20: :: FUNCTOR0:def 20
for b₁, b₂ being object of a₁ st <^b₁,b₂^> <> {} holds
<^(a₃ . b₂),(a₃ . b₁)^> <> {} ;
compatibility

proof end;

end;

:: deftheorem Def20 defines feasible FUNCTOR0:def 20 :

registration

let c₁, c₂ be AltGraph ;
let c₃ be FunctorStr of c₁,c₂;
cluster the MorphMap of a₃ -> Function-yielding ;
coherence ;

end;

registration

cluster non empty reflexive AltCatStr ;
existence

proof end;

end;

definition

let c₁, c₂ be non empty with_units AltCatStr ;
let c₃ be FunctorStr of c₁,c₂;
attr a₃ is id-preserving means :Def21: :: FUNCTOR0:def 21
for b₁ being object of a₁ holds (Morph-Map a₃,b₁,b₁) . (idm b₁) = idm (a₃ . b₁);

end;

:: deftheorem Def21 defines id-preserving FUNCTOR0:def 21 :

theorem Th25: :: FUNCTOR0:25

for b₁, b₂ being non empty AltGraph
for b₃ being object of b₂ st <^b₃,b₃^> <> {} holds
for b₄ being Morphism of b₃,b₃
for b₅, b₆ being object of b₁
for b₇ being Morphism of b₅,b₆ st <^b₅,b₆^> <> {} holds
(Morph-Map (b₁ --> b₄),b₅,b₆) . b₇ = b₄

proof end;

registration

cluster non empty with_units -> non empty reflexive AltCatStr ;
coherence

proof end;

end;

registration

let c₁, c₂ be non empty with_units AltCatStr ;
let c₃ be object of c₂;
cluster a₁ --> (idm a₃) -> feasible strict Covariant Contravariant id-preserving ;
coherence

proof end;

end;

registration

let c₁ be non empty AltGraph ;
let c₂ be non empty reflexive AltGraph ;
let c₃ be object of c₂;
let c₄ be Morphism of c₃,c₃;
cluster a₁ --> a₄ -> reflexive feasible strict Covariant Contravariant ;
coherence

proof end;

end;

registration

let c₁ be non empty AltGraph ;
let c₂ be non empty reflexive AltGraph ;
cluster reflexive feasible FunctorStr of a₁,a₂;
existence

proof end;

end;

registration

let c₁, c₂ be non empty with_units AltCatStr ;
cluster reflexive feasible strict id-preserving FunctorStr of a₁,a₂;
existence

proof end;

end;

definition

let c₁, c₂ be non empty AltCatStr ;
let c₃ be FunctorStr of c₁,c₂;
attr a₃ is comp-preserving means :Def22: :: FUNCTOR0:def 22
for b₁, b₂, b₃ being object of a₁ st <^b₁,b₂^> <> {} & <^b₂,b₃^> <> {} holds
for b₄ being Morphism of b₁,b₂
for b₅ being Morphism of b₂,b₃ ex b₆ being Morphism of (a₃ . b₁),(a₃ . b₂)ex b₇ being Morphism of (a₃ . b₂),(a₃ . b₃) st
( b₆ = (Morph-Map a₃,b₁,b₂) . b₄ & b₇ = (Morph-Map a₃,b₂,b₃) . b₅ & (Morph-Map a₃,b₁,b₃) . (b₅ * b₄) = b₇ * b₆ );

end;

:: deftheorem Def22 defines comp-preserving FUNCTOR0:def 22 :

definition

let c₁, c₂ be non empty AltCatStr ;
let c₃ be FunctorStr of c₁,c₂;
attr a₃ is comp-reversing means :Def23: :: FUNCTOR0:def 23
for b₁, b₂, b₃ being object of a₁ st <^b₁,b₂^> <> {} & <^b₂,b₃^> <> {} holds
for b₄ being Morphism of b₁,b₂
for b₅ being Morphism of b₂,b₃ ex b₆ being Morphism of (a₃ . b₂),(a₃ . b₁)ex b₇ being Morphism of (a₃ . b₃),(a₃ . b₂) st
( b₆ = (Morph-Map a₃,b₁,b₂) . b₄ & b₇ = (Morph-Map a₃,b₂,b₃) . b₅ & (Morph-Map a₃,b₁,b₃) . (b₅ * b₄) = b₆ * b₇ );

end;

:: deftheorem Def23 defines comp-reversing FUNCTOR0:def 23 :

definition

let c₁ be non empty transitive AltCatStr ;
let c₂ be non empty reflexive AltCatStr ;
let c₃ be feasible Covariant FunctorStr of c₁,c₂;
redefine attr a₃ is comp-preserving means :: FUNCTOR0:def 24
for b₁, b₂, b₃ being object of a₁ st <^b₁,b₂^> <> {} & <^b₂,b₃^> <> {} holds
for b₄ being Morphism of b₁,b₂
for b₅ being Morphism of b₂,b₃ holds a₃ . (b₅ * b₄) = (a₃ . b₅) * (a₃ . b₄);
compatibility

proof end;

end;

:: deftheorem Def24 defines comp-preserving FUNCTOR0:def 24 :

definition

let c₁ be non empty transitive AltCatStr ;
let c₂ be non empty reflexive AltCatStr ;
let c₃ be feasible Contravariant FunctorStr of c₁,c₂;
redefine attr a₃ is comp-reversing means :: FUNCTOR0:def 25
for b₁, b₂, b₃ being object of a₁ st <^b₁,b₂^> <> {} & <^b₂,b₃^> <> {} holds
for b₄ being Morphism of b₁,b₂
for b₅ being Morphism of b₂,b₃ holds a₃ . (b₅ * b₄) = (a₃ . b₄) * (a₃ . b₅);
compatibility

proof end;

end;

:: deftheorem Def25 defines comp-reversing FUNCTOR0:def 25 :

theorem Th26: :: FUNCTOR0:26

for b₁ being non empty AltGraph
for b₂ being non empty reflexive AltGraph
for b₃ being object of b₂
for b₄ being Morphism of b₃,b₃
for b₅ being feasible Covariant FunctorStr of b₁,b₂ st b₅ = b₁ --> b₄ holds
for b₆, b₇ being object of b₁
for b₈ being Morphism of b₆,b₇ st <^b₆,b₇^> <> {} holds
b₅ . b₈ = b₄

proof end;

theorem Th27: :: FUNCTOR0:27

for b₁ being non empty AltGraph
for b₂ being non empty reflexive AltGraph
for b₃ being object of b₂
for b₄ being Morphism of b₃,b₃
for b₅, b₆ being object of b₁
for b₇ being Morphism of b₅,b₆ st <^b₅,b₆^> <> {} holds
(b₁ --> b₄) . b₇ = b₄

proof end;

registration

let c₁ be non empty transitive AltCatStr ;
let c₂ be non empty with_units AltCatStr ;
let c₃ be object of c₂;
cluster a₁ --> (idm a₃) -> reflexive feasible strict Covariant Contravariant comp-preserving comp-reversing ;
coherence

proof end;

end;

definition

let c₁ be non empty transitive with_units AltCatStr ;
let c₂ be non empty with_units AltCatStr ;
mode Functor of c₁,c₂ -> FunctorStr of a₁,a₂ means :Def26: :: FUNCTOR0:def 26
( a₃ is feasible & a₃ is id-preserving & ( ( a₃ is Covariant & a₃ is comp-preserving ) or ( a₃ is Contravariant & a₃ is comp-reversing ) ) );
existence

proof end;

end;

:: deftheorem Def26 defines Functor FUNCTOR0:def 26 :

definition

let c₁ be non empty transitive with_units AltCatStr ;
let c₂ be non empty with_units AltCatStr ;
let c₃ be Functor of c₁,c₂;
attr a₃ is covariant means :Def27: :: FUNCTOR0:def 27
( a₃ is Covariant & a₃ is comp-preserving );
attr a₃ is contravariant means :Def28: :: FUNCTOR0:def 28
( a₃ is Contravariant & a₃ is comp-reversing );

end;

:: deftheorem Def27 defines covariant FUNCTOR0:def 27 :

:: deftheorem Def28 defines contravariant FUNCTOR0:def 28 :

definition

let c₁ be AltCatStr ;
let c₂ be SubCatStr of c₁;
func incl c₂ -> strict FunctorStr of a₂,a₁ means :Def29: :: FUNCTOR0:def 29
( the ObjectMap of a₃ = id [:the carrier of a₂,the carrier of a₂:] & the MorphMap of a₃ = id the Arrows of a₂ );
existence

proof end;

correctness ;

end;

:: deftheorem Def29 defines incl FUNCTOR0:def 29 :

definition

let c₁ be AltGraph ;
func id c₁ -> strict FunctorStr of a₁,a₁ means :Def30: :: FUNCTOR0:def 30
( the ObjectMap of a₂ = id [:the carrier of a₁,the carrier of a₁:] & the MorphMap of a₂ = id the Arrows of a₁ );
existence

proof end;

correctness ;

end;

:: deftheorem Def30 defines id FUNCTOR0:def 30 :

registration

let c₁ be AltCatStr ;
let c₂ be SubCatStr of c₁;
cluster incl a₂ -> strict Covariant ;
coherence

proof end;

end;

theorem Th28: :: FUNCTOR0:28

for b₁ being non empty AltCatStr
for b₂ being non empty SubCatStr of b₁
for b₃ being object of b₂ holds (incl b₂) . b₃ = b₃

proof end;

theorem Th29: :: FUNCTOR0:29

for b₁ being non empty AltCatStr
for b₂ being non empty SubCatStr of b₁
for b₃, b₄ being object of b₂ holds <^b₃,b₄^> c= <^((incl b₂) . b₃),((incl b₂) . b₄)^>

proof end;

registration

let c₁ be non empty AltCatStr ;
let c₂ be non empty SubCatStr of c₁;
cluster incl a₂ -> feasible strict Covariant ;
coherence

proof end;

end;

definition

let c₁, c₂ be AltGraph ;
let c₃ be FunctorStr of c₁,c₂;
attr a₃ is faithful means :Def31: :: FUNCTOR0:def 31
the MorphMap of a₃ is "1-1";

end;

:: deftheorem Def31 defines faithful FUNCTOR0:def 31 :

definition

let c₁, c₂ be AltGraph ;
let c₃ be FunctorStr of c₁,c₂;
attr a₃ is full means :Def32: :: FUNCTOR0:def 32
ex b₁ being ManySortedSet of [:the carrier of a₁,the carrier of a₁:]ex b₂ being ManySortedFunction of the Arrows of a₁,b₁ st
( b₁ = the Arrows of a₂ * the ObjectMap of a₃ & b₂ = the MorphMap of a₃ & b₂ is "onto" );

end;

:: deftheorem Def32 defines full FUNCTOR0:def 32 :

definition

let c₁ be AltGraph ;
let c₂ be non empty AltGraph ;
let c₃ be FunctorStr of c₁,c₂;
redefine attr a₃ is full means :Def33: :: FUNCTOR0:def 33
ex b₁ being ManySortedFunction of the Arrows of a₁,the Arrows of a₂ * the ObjectMap of a₃ st
( b₁ = the MorphMap of a₃ & b₁ is "onto" );
compatibility

proof end;

end;

:: deftheorem Def33 defines full FUNCTOR0:def 33 :

definition

let c₁, c₂ be AltGraph ;
let c₃ be FunctorStr of c₁,c₂;
attr a₃ is injective means :Def34: :: FUNCTOR0:def 34
( a₃ is one-to-one & a₃ is faithful );
attr a₃ is surjective means :Def35: :: FUNCTOR0:def 35
( a₃ is full & a₃ is onto );

end;

:: deftheorem Def34 defines injective FUNCTOR0:def 34 :

:: deftheorem Def35 defines surjective FUNCTOR0:def 35 :

definition

let c₁, c₂ be AltGraph ;
let c₃ be FunctorStr of c₁,c₂;
attr a₃ is bijective means :Def36: :: FUNCTOR0:def 36
( a₃ is injective & a₃ is surjective );

end;

:: deftheorem Def36 defines bijective FUNCTOR0:def 36 :

registration

let c₁, c₂ be non empty transitive with_units AltCatStr ;
cluster feasible strict covariant contravariant Functor of a₁,a₂;
existence

proof end;

end;

theorem Th30: :: FUNCTOR0:30

for b₁ being non empty AltGraph
for b₂ being object of b₁ holds (id b₁) . b₂ = b₂

proof end;

theorem Th31: :: FUNCTOR0:31

for b₁ being non empty AltGraph
for b₂, b₃ being object of b₁ st <^b₂,b₃^> <> {} holds
for b₄ being Morphism of b₂,b₃ holds (Morph-Map (id b₁),b₂,b₃) . b₄ = b₄

proof end;

registration

let c₁ be non empty AltGraph ;
cluster id a₁ -> feasible strict Covariant ;
coherence

proof end;

end;

registration

let c₁ be non empty AltGraph ;
cluster feasible Covariant FunctorStr of a₁,a₁;
existence

proof end;

end;

theorem Th32: :: FUNCTOR0:32

for b₁ being non empty AltGraph
for b₂, b₃ being object of b₁ st <^b₂,b₃^> <> {} holds
for b₄ being feasible Covariant FunctorStr of b₁,b₁ st b₄ = id b₁ holds
for b₅ being Morphism of b₂,b₃ holds b₄ . b₅ = b₅

proof end;

registration

let c₁ be non empty transitive with_units AltCatStr ;
cluster id a₁ -> feasible strict Covariant id-preserving comp-preserving ;
coherence

proof end;

end;

definition

let c₁ be non empty transitive with_units AltCatStr ;
redefine func id as id c₁ -> strict covariant Functor of a₁,a₁;
coherence by Def26, Def27;

end;

registration

let c₁ be AltGraph ;
cluster id a₁ -> strict bijective ;
coherence

proof end;

end;

definition

let c₁ be non empty AltGraph ;
let c₂, c₃ be non empty reflexive AltGraph ;
let c₄ be feasible FunctorStr of c₁,c₂;
let c₅ be FunctorStr of c₂,c₃;
func c₅ * c₄ -> strict FunctorStr of a₁,a₃ means :Def37: :: FUNCTOR0:def 37
( the ObjectMap of a₆ = the ObjectMap of a₅ * the ObjectMap of a₄ & the MorphMap of a₆ = (the MorphMap of a₅ * the ObjectMap of a₄) ** the MorphMap of a₄ );
existence

proof end;

correctness ;

end;

:: deftheorem Def37 defines * FUNCTOR0:def 37 :

registration

let c₁ be non empty AltGraph ;
let c₂, c₃ be non empty reflexive AltGraph ;
let c₄ be feasible Covariant FunctorStr of c₁,c₂;
let c₅ be Covariant FunctorStr of c₂,c₃;
cluster a₅ * a₄ -> strict Covariant ;
correctness

proof end;

end;

registration

let c₁ be non empty AltGraph ;
let c₂, c₃ be non empty reflexive AltGraph ;
let c₄ be feasible Contravariant FunctorStr of c₁,c₂;
let c₅ be Covariant FunctorStr of c₂,c₃;
cluster a₅ * a₄ -> strict Contravariant ;
correctness

proof end;

end;

registration

let c₁ be non empty AltGraph ;
let c₂, c₃ be non empty reflexive AltGraph ;
let c₄ be feasible Covariant FunctorStr of c₁,c₂;
let c₅ be Contravariant FunctorStr of c₂,c₃;
cluster a₅ * a₄ -> strict Contravariant ;
correctness

proof end;

end;

registration

let c₁ be non empty AltGraph ;
let c₂, c₃ be non empty reflexive AltGraph ;
let c₄ be feasible Contravariant FunctorStr of c₁,c₂;
let c₅ be Contravariant FunctorStr of c₂,c₃;
cluster a₅ * a₄ -> strict Covariant ;
correctness

proof end;

end;

registration

let c₁ be non empty AltGraph ;
let c₂, c₃ be non empty reflexive AltGraph ;
let c₄ be feasible FunctorStr of c₁,c₂;
let c₅ be feasible FunctorStr of c₂,c₃;
cluster a₅ * a₄ -> feasible strict ;
coherence

proof end;

end;

theorem Th33: :: FUNCTOR0:33

for b₁ being non empty AltGraph
for b₂, b₃, b₄ being non empty reflexive AltGraph
for b₅ being feasible FunctorStr of b₁,b₂
for b₆ being feasible FunctorStr of b₂,b₃
for b₇ being FunctorStr of b₃,b₄ holds (b₇ * b₆) * b₅ = b₇ * (b₆ * b₅)

proof end;

theorem Th34: :: FUNCTOR0:34

for b₁ being non empty AltCatStr
for b₂, b₃ being non empty reflexive AltCatStr
for b₄ being reflexive feasible FunctorStr of b₁,b₂
for b₅ being FunctorStr of b₂,b₃
for b₆ being object of b₁ holds (b₅ * b₄) . b₆ = b₅ . (b₄ . b₆)

proof end;

theorem Th35: :: FUNCTOR0:35

for b₁ being non empty AltGraph
for b₂, b₃ being non empty reflexive AltGraph
for b₄ being reflexive feasible FunctorStr of b₁,b₂
for b₅ being FunctorStr of b₂,b₃
for b₆ being object of b₁ holds Morph-Map (b₅ * b₄),b₆,b₆ = (Morph-Map b₅,(b₄ . b₆),(b₄ . b₆)) * (Morph-Map b₄,b₆,b₆)

proof end;

registration

let c₁, c₂, c₃ be non empty with_units AltCatStr ;
let c₄ be reflexive feasible id-preserving FunctorStr of c₁,c₂;
let c₅ be id-preserving FunctorStr of c₂,c₃;
cluster a₅ * a₄ -> strict id-preserving ;
coherence

proof end;

end;

definition

let c₁, c₂ be non empty reflexive AltCatStr ;
let c₃ be non empty SubCatStr of c₁;
let c₄ be FunctorStr of c₁,c₂;
func c₄ | c₃ -> FunctorStr of a₃,a₂ equals :: FUNCTOR0:def 38
a₄ * (incl a₃);
correctness ;

end;

:: deftheorem Def38 defines | FUNCTOR0:def 38 :

definition

let c₁, c₂ be non empty AltGraph ;
let c₃ be FunctorStr of c₁,c₂;
assume E65: c₃ is bijective ;
func c₃ " -> strict FunctorStr of a₂,a₁ means :Def39: :: FUNCTOR0:def 39
( the ObjectMap of a₄ = the ObjectMap of a₃ " & ex b₁ being ManySortedFunction of the Arrows of a₁,the Arrows of a₂ * the ObjectMap of a₃ st
( b₁ = the MorphMap of a₃ & the MorphMap of a₄ = (b₁ "" ) * (the ObjectMap of a₃ " ) ) );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def39 defines " FUNCTOR0:def 39 :

theorem Th36: :: FUNCTOR0:36

for b₁, b₂ being non empty transitive with_units AltCatStr
for b₃ being feasible FunctorStr of b₁,b₂ st b₃ is bijective holds
( b₃ " is bijective & b₃ " is feasible )

proof end;

theorem Th37: :: FUNCTOR0:37

for b₁, b₂ being non empty transitive with_units AltCatStr
for b₃ being reflexive feasible FunctorStr of b₁,b₂ st b₃ is bijective & b₃ is coreflexive holds
b₃ " is reflexive

proof end;

theorem Th38: :: FUNCTOR0:38

for b₁, b₂ being non empty transitive with_units AltCatStr
for b₃ being reflexive feasible id-preserving FunctorStr of b₁,b₂ st b₃ is bijective & b₃ is coreflexive holds
b₃ " is id-preserving

proof end;

theorem Th39: :: FUNCTOR0:39

for b₁, b₂ being non empty transitive with_units AltCatStr
for b₃ being feasible FunctorStr of b₁,b₂ st b₃ is bijective & b₃ is Covariant holds
b₃ " is Covariant

proof end;

theorem Th40: :: FUNCTOR0:40

for b₁, b₂ being non empty transitive with_units AltCatStr
for b₃ being feasible FunctorStr of b₁,b₂ st b₃ is bijective & b₃ is Contravariant holds
b₃ " is Contravariant

proof end;

theorem Th41: :: FUNCTOR0:41

for b₁, b₂ being non empty transitive with_units AltCatStr
for b₃ being reflexive feasible FunctorStr of b₁,b₂ st b₃ is bijective & b₃ is coreflexive & b₃ is Covariant holds
for b₄, b₅ being object of b₂
for b₆ being Morphism of b₄,b₅ st <^b₄,b₅^> <> {} holds
(Morph-Map b₃,((b₃ " ) . b₄),((b₃ " ) . b₅)) . ((Morph-Map (b₃ " ),b₄,b₅) . b₆) = b₆

proof end;

theorem Th42: :: FUNCTOR0:42

for b₁, b₂ being non empty transitive with_units AltCatStr
for b₃ being reflexive feasible FunctorStr of b₁,b₂ st b₃ is bijective & b₃ is coreflexive & b₃ is Contravariant holds
for b₄, b₅ being object of b₂
for b₆ being Morphism of b₄,b₅ st <^b₄,b₅^> <> {} holds
(Morph-Map b₃,((b₃ " ) . b₅),((b₃ " ) . b₄)) . ((Morph-Map (b₃ " ),b₄,b₅) . b₆) = b₆

proof end;

theorem Th43: :: FUNCTOR0:43

for b₁, b₂ being non empty transitive with_units AltCatStr
for b₃ being reflexive feasible FunctorStr of b₁,b₂ st b₃ is bijective & b₃ is comp-preserving & b₃ is Covariant & b₃ is coreflexive holds
b₃ " is comp-preserving

proof end;

theorem Th44: :: FUNCTOR0:44

for b₁, b₂ being non empty transitive with_units AltCatStr
for b₃ being reflexive feasible FunctorStr of b₁,b₂ st b₃ is bijective & b₃ is comp-reversing & b₃ is Contravariant & b₃ is coreflexive holds
b₃ " is comp-reversing

proof end;

registration

let c₁ be 1-sorted ;
let c₂ be non empty 1-sorted ;
cluster Covariant -> reflexive BimapStr of a₁,a₂;
coherence

proof end;

end;

registration

let c₁ be 1-sorted ;
let c₂ be non empty 1-sorted ;
cluster Contravariant -> reflexive BimapStr of a₁,a₂;
coherence

proof end;

end;

theorem Th45: :: FUNCTOR0:45

for b₁, b₂ being 1-sorted
for b₃ being BimapStr of b₁,b₂ st b₃ is Covariant & b₃ is onto holds
b₃ is coreflexive

proof end;

theorem Th46: :: FUNCTOR0:46

for b₁, b₂ being 1-sorted
for b₃ being BimapStr of b₁,b₂ st b₃ is Contravariant & b₃ is onto holds
b₃ is coreflexive

proof end;

registration

let c₁ be non empty transitive with_units AltCatStr ;
let c₂ be non empty with_units AltCatStr ;
cluster covariant -> reflexive Functor of a₁,a₂;
coherence

proof end;

end;

registration

let c₁ be non empty transitive with_units AltCatStr ;
let c₂ be non empty with_units AltCatStr ;
cluster contravariant -> reflexive Functor of a₁,a₂;
coherence

proof end;

end;

theorem Th47: :: FUNCTOR0:47

for b₁ being non empty transitive with_units AltCatStr
for b₂ being non empty with_units AltCatStr
for b₃ being Functor of b₁,b₂ st b₃ is covariant & b₃ is onto holds
b₃ is coreflexive

proof end;

theorem Th48: :: FUNCTOR0:48

for b₁ being non empty transitive with_units AltCatStr
for b₂ being non empty with_units AltCatStr
for b₃ being Functor of b₁,b₂ st b₃ is contravariant & b₃ is onto holds
b₃ is coreflexive

proof end;

theorem Th49: :: FUNCTOR0:49

for b₁, b₂ being non empty transitive with_units AltCatStr
for b₃ being covariant Functor of b₁,b₂ st b₃ is bijective holds
ex b₄ being Functor of b₂,b₁ st
( b₄ = b₃ " & b₄ is bijective & b₄ is covariant )

proof end;

theorem Th50: :: FUNCTOR0:50

for b₁, b₂ being non empty transitive with_units AltCatStr
for b₃ being contravariant Functor of b₁,b₂ st b₃ is bijective holds
ex b₄ being Functor of b₂,b₁ st
( b₄ = b₃ " & b₄ is bijective & b₄ is contravariant )

proof end;

definition

let c₁, c₂ be non empty transitive with_units AltCatStr ;
pred c₁,c₂ are_isomorphic means :: FUNCTOR0:def 40
ex b₁ being Functor of a₁,a₂ st
( b₁ is bijective & b₁ is covariant );
reflexivity

proof end;

symmetry

proof end;

pred c₁,c₂ are_anti-isomorphic means :: FUNCTOR0:def 41
ex b₁ being Functor of a₁,a₂ st
( b₁ is bijective & b₁ is contravariant );
symmetry

proof end;

end;

:: deftheorem Def40 defines are_isomorphic FUNCTOR0:def 40 :

:: deftheorem Def41 defines are_anti-isomorphic FUNCTOR0:def 41 :