:: Object-Free Definition of Categories
:: by Marco Riccardi
::
:: Received October 7, 2013
:: Copyright (c) 2013-2021 Association of Mizar Users

definition

attr c₁ is strict ;
struct CategoryStr -> 1-sorted ;
aggr CategoryStr(# carrier, composition #) -> CategoryStr ;
sel composition c₁ -> PartFunc of [: the carrier of c₁, the carrier of c₁:], the carrier of c₁;

end;

definition

let C be CategoryStr ;

func Mor C -> set equals :: CAT_6:def 1
the carrier of C;

correctness
coherence
the carrier of C is set ;
;

end;

:: deftheorem defines Mor CAT_6:def 1 :
for C being CategoryStr holds Mor C = the carrier of C;

definition

let C be CategoryStr ;
mode morphism of C is Element of Mor C;

end;

definition

let C be CategoryStr ;
let f1, f2 be morphism of C;

pred f1,f2 are_composable means :Def2: :: CAT_6:def 2
[f1,f2] in dom the composition of C;

end;

:: deftheorem Def2 defines are_composable CAT_6:def 2 :
for C being CategoryStr
for f1, f2 being morphism of C holds
( f1,f2 are_composable iff [f1,f2] in dom the composition of C );

notation

let C be CategoryStr ;
let f1, f2 be morphism of C;
synonym f1 |> f2 for f1,f2 are_composable ;

end;

definition

let C be CategoryStr ;
let f1, f2 be morphism of C;
assume A1: f1 |> f2 ;

func f1 (*) f2 -> morphism of C equals :Def3: :: CAT_6:def 3
the composition of C . (f1,f2);

correctness
coherence
the composition of C . (f1,f2) is morphism of C;

proof end;

end;

:: deftheorem Def3 defines (*) CAT_6:def 3 :
for C being CategoryStr
for f1, f2 being morphism of C st f1 |> f2 holds
f1 (*) f2 = the composition of C . (f1,f2);

definition

let C be CategoryStr ;
let f be morphism of C;

attr f is left_identity means :Def4: :: CAT_6:def 4
for f1 being morphism of C st f |> f1 holds
f (*) f1 = f1;

attr f is right_identity means :Def5: :: CAT_6:def 5
for f1 being morphism of C st f1 |> f holds
f1 (*) f = f1;

end;

:: deftheorem Def4 defines left_identity CAT_6:def 4 :
for C being CategoryStr
for f being morphism of C holds
( f is left_identity iff for f1 being morphism of C st f |> f1 holds
f (*) f1 = f1 );

:: deftheorem Def5 defines right_identity CAT_6:def 5 :
for C being CategoryStr
for f being morphism of C holds
( f is right_identity iff for f1 being morphism of C st f1 |> f holds
f1 (*) f = f1 );

definition

let C be CategoryStr ;

attr C is with_left_identities means :Def6: :: CAT_6:def 6
for f1 being morphism of C st f1 in the carrier of C holds
ex f being morphism of C st
( f |> f1 & f is left_identity );

attr C is with_right_identities means :Def7: :: CAT_6:def 7
for f1 being morphism of C st f1 in the carrier of C holds
ex f being morphism of C st
( f1 |> f & f is right_identity );

attr C is left_composable means :: CAT_6:def 8
for f, f1, f2 being morphism of C st f1 |> f2 holds
( f1 (*) f2 |> f iff f2 |> f );

attr C is right_composable means :Def9: :: CAT_6:def 9
for f, f1, f2 being morphism of C st f1 |> f2 holds
( f |> f1 (*) f2 iff f |> f1 );

attr C is associative means :Def10: :: CAT_6:def 10
for f1, f2, f3 being morphism of C st f1 |> f2 & f2 |> f3 & f1 (*) f2 |> f3 & f1 |> f2 (*) f3 holds
f1 (*) (f2 (*) f3) = (f1 (*) f2) (*) f3;

end;

:: deftheorem Def6 defines with_left_identities CAT_6:def 6 :
for C being CategoryStr holds
( C is with_left_identities iff for f1 being morphism of C st f1 in the carrier of C holds
ex f being morphism of C st
( f |> f1 & f is left_identity ) );

:: deftheorem Def7 defines with_right_identities CAT_6:def 7 :
for C being CategoryStr holds
( C is with_right_identities iff for f1 being morphism of C st f1 in the carrier of C holds
ex f being morphism of C st
( f1 |> f & f is right_identity ) );

:: deftheorem defines left_composable CAT_6:def 8 :
for C being CategoryStr holds
( C is left_composable iff for f, f1, f2 being morphism of C st f1 |> f2 holds
( f1 (*) f2 |> f iff f2 |> f ) );

:: deftheorem Def9 defines right_composable CAT_6:def 9 :
for C being CategoryStr holds
( C is right_composable iff for f, f1, f2 being morphism of C st f1 |> f2 holds
( f |> f1 (*) f2 iff f |> f1 ) );

:: deftheorem Def10 defines associative CAT_6:def 10 :
for C being CategoryStr holds
( C is associative iff for f1, f2, f3 being morphism of C st f1 |> f2 & f2 |> f3 & f1 (*) f2 |> f3 & f1 |> f2 (*) f3 holds
f1 (*) (f2 (*) f3) = (f1 (*) f2) (*) f3 );

definition

let C be CategoryStr ;

attr C is composable means :Def11: :: CAT_6:def 11
( C is left_composable & C is right_composable );

attr C is with_identities means :Def12: :: CAT_6:def 12
( C is with_left_identities & C is with_right_identities );

end;

:: deftheorem Def11 defines composable CAT_6:def 11 :
for C being CategoryStr holds
( C is composable iff ( C is left_composable & C is right_composable ) );

:: deftheorem Def12 defines with_identities CAT_6:def 12 :
for C being CategoryStr holds
( C is with_identities iff ( C is with_left_identities & C is with_right_identities ) );

definition

let C be CategoryStr ;

func C opp -> strict CategoryStr equals :: CAT_6:def 13
CategoryStr(# the carrier of C,(~ the composition of C) #);

coherence
CategoryStr(# the carrier of C,(~ the composition of C) #) is strict CategoryStr ;

end;

:: deftheorem defines opp CAT_6:def 13 :
for C being CategoryStr holds C opp = CategoryStr(# the carrier of C,(~ the composition of C) #);

theorem :: CAT_6:1

for C being CategoryStr
for f1, f2 being morphism of C st C is empty holds
not f1 |> f2 ;

theorem :: CAT_6:2

for C being CategoryStr
for f1, f2 being morphism of C
for g1, g2 being morphism of (C opp) st f1 = g1 & f2 = g2 holds
( f1 |> f2 iff g2 |> g1 ) by FUNCT_4:42;

theorem Th3: :: CAT_6:3

for C being CategoryStr
for f1, f2 being morphism of C
for g1, g2 being morphism of (C opp) st f1 = g1 & f2 = g2 & f1 |> f2 holds
f1 (*) f2 = g2 (*) g1

proof end;

theorem Th4: :: CAT_6:4

for C being CategoryStr holds
( C is left_composable iff C opp is right_composable )

proof end;

theorem Th5: :: CAT_6:5

for C being CategoryStr holds
( C is right_composable iff C opp is left_composable )

proof end;

theorem Th6: :: CAT_6:6

for C being CategoryStr holds
( C is with_left_identities iff C opp is with_right_identities )

proof end;

theorem Th7: :: CAT_6:7

for C being CategoryStr holds
( C is with_right_identities iff C opp is with_left_identities )

proof end;

theorem Th8: :: CAT_6:8

for C being CategoryStr holds
( C is associative iff C opp is associative )

proof end;

registration

cluster with_left_identities non with_right_identities associative composable for CategoryStr ;

correctness
existence
ex b₁ being CategoryStr st
( b₁ is with_left_identities & not b₁ is with_right_identities & b₁ is composable & b₁ is associative );

proof end;

end;

registration

cluster non with_left_identities with_right_identities associative composable for CategoryStr ;

correctness
existence
ex b₁ being CategoryStr st
( not b₁ is with_left_identities & b₁ is with_right_identities & b₁ is composable & b₁ is associative );

proof end;

end;

registration

cluster non left_composable right_composable associative with_identities for CategoryStr ;

correctness
existence
ex b₁ being CategoryStr st
( not b₁ is left_composable & b₁ is right_composable & b₁ is with_identities & b₁ is associative );

proof end;

end;

registration

cluster left_composable non right_composable associative with_identities for CategoryStr ;

correctness
existence
ex b₁ being CategoryStr st
( b₁ is left_composable & not b₁ is right_composable & b₁ is with_identities & b₁ is associative );

proof end;

end;

registration

cluster non associative composable with_identities for CategoryStr ;

correctness
existence
ex b₁ being CategoryStr st
( not b₁ is associative & b₁ is composable & b₁ is with_identities );

proof end;

end;

registration

cluster empty for CategoryStr ;

correctness
existence
ex b₁ being CategoryStr st b₁ is empty ;

proof end;

end;

registration

cluster empty -> with_left_identities with_right_identities left_composable right_composable associative for CategoryStr ;

correctness
coherence
for b₁ being CategoryStr st b₁ is empty holds
( b₁ is left_composable & b₁ is right_composable & b₁ is with_left_identities & b₁ is with_right_identities & b₁ is associative );

proof end;

end;

registration

cluster strict with_left_identities with_right_identities left_composable right_composable associative for CategoryStr ;

correctness
existence
ex b₁ being CategoryStr st
( b₁ is strict & b₁ is with_left_identities & b₁ is with_right_identities & b₁ is left_composable & b₁ is right_composable & b₁ is associative );

proof end;

end;

registration

cluster strict associative composable with_identities for CategoryStr ;

correctness
existence
ex b₁ being CategoryStr st
( b₁ is strict & b₁ is with_identities & b₁ is composable & b₁ is associative );

proof end;

end;

definition

mode category is associative composable with_identities CategoryStr ;

end;

definition

let C be CategoryStr ;
let f be morphism of C;

attr f is identity means :: CAT_6:def 14
( f is left_identity & f is right_identity );

end;

:: deftheorem defines identity CAT_6:def 14 :
for C being CategoryStr
for f being morphism of C holds
( f is identity iff ( f is left_identity & f is right_identity ) );

theorem Th9: :: CAT_6:9

for C being CategoryStr
for f being morphism of C st C is with_identities holds
( f is left_identity iff f is right_identity )

proof end;

theorem Th10: :: CAT_6:10

for C being CategoryStr
for f being morphism of C st C is empty holds
f is identity

proof end;

theorem Th11: :: CAT_6:11

for C being CategoryStr
for f1, f2 being morphism of C
for g1, g2 being morphism of CategoryStr(# the carrier of C, the composition of C #) st f1 = g1 & f2 = g2 & f1 |> f2 holds
f1 (*) f2 = g1 (*) g2

proof end;

theorem Th12: :: CAT_6:12

for C being CategoryStr holds
( C is left_composable iff CategoryStr(# the carrier of C, the composition of C #) is left_composable )

proof end;

theorem Th13: :: CAT_6:13

for C being CategoryStr holds
( C is right_composable iff CategoryStr(# the carrier of C, the composition of C #) is right_composable )

proof end;

theorem :: CAT_6:14

for C being CategoryStr holds
( C is composable iff CategoryStr(# the carrier of C, the composition of C #) is composable ) by Th12, Th13;

theorem :: CAT_6:15

for C being CategoryStr holds
( C is associative iff CategoryStr(# the carrier of C, the composition of C #) is associative )

proof end;

theorem Th16: :: CAT_6:16

for C being CategoryStr
for f being morphism of C
for g being morphism of CategoryStr(# the carrier of C, the composition of C #) st f = g holds
( f is left_identity iff g is left_identity )

proof end;

theorem Th17: :: CAT_6:17

for C being CategoryStr holds
( C is with_left_identities iff CategoryStr(# the carrier of C, the composition of C #) is with_left_identities )

proof end;

theorem Th18: :: CAT_6:18

for C being CategoryStr
for f being morphism of C
for g being morphism of CategoryStr(# the carrier of C, the composition of C #) st f = g holds
( f is right_identity iff g is right_identity )

proof end;

theorem Th19: :: CAT_6:19

for C being CategoryStr holds
( C is with_right_identities iff CategoryStr(# the carrier of C, the composition of C #) is with_right_identities )

proof end;

theorem :: CAT_6:20

for C being CategoryStr holds
( C is with_identities iff CategoryStr(# the carrier of C, the composition of C #) is with_identities ) by Th17, Th19;

definition

let C be CategoryStr ;

attr C is discrete means :Def15: :: CAT_6:def 15
for f being morphism of C holds f is identity ;

end;

:: deftheorem Def15 defines discrete CAT_6:def 15 :
for C being CategoryStr holds
( C is discrete iff for f being morphism of C holds f is identity );

Lm1: the empty CategoryStr opp is discrete

proof end;

registration

cluster empty strict associative composable with_identities discrete for CategoryStr ;

correctness
existence
ex b₁ being CategoryStr st
( b₁ is strict & b₁ is empty & b₁ is discrete & b₁ is with_identities & b₁ is composable & b₁ is associative );

proof end;

end;

theorem Th21: :: CAT_6:21

for C being discrete CategoryStr
for f1, f2 being morphism of C st f1 |> f2 holds
( f1 = f2 & f1 (*) f2 = f2 )

proof end;

registration

cluster discrete -> associative composable for CategoryStr ;

correctness
coherence
for b₁ being CategoryStr st b₁ is discrete holds
( b₁ is composable & b₁ is associative );

proof end;

end;

definition

let X be set ;

func DiscreteCat X -> strict discrete category means :Def16: :: CAT_6:def 16
the carrier of it = X;

existence
ex b₁ being strict discrete category st the carrier of b₁ = X

proof end;

uniqueness
for b₁, b₂ being strict discrete category st the carrier of b₁ = X & the carrier of b₂ = X holds
b₁ = b₂

proof end;

end;

:: deftheorem Def16 defines DiscreteCat CAT_6:def 16 :
for X being set
for b₂ being strict discrete category holds
( b₂ = DiscreteCat X iff the carrier of b₂ = X );

registration

cluster strict associative composable with_identities for CategoryStr ;

correctness
existence
ex b₁ being category st b₁ is strict ;

proof end;

cluster empty strict associative composable with_identities for CategoryStr ;

correctness
existence
ex b₁ being category st
( b₁ is strict & b₁ is empty );

proof end;

cluster non empty strict associative composable with_identities for CategoryStr ;

correctness
existence
ex b₁ being category st
( b₁ is strict & not b₁ is empty );

proof end;

end;

definition

let C be CategoryStr ;

func Ob C -> Subset of (Mor C) equals :: CAT_6:def 17
{ f where f is morphism of C : ( f is identity & f in Mor C ) } ;

correctness
coherence
{ f where f is morphism of C : ( f is identity & f in Mor C ) } is Subset of (Mor C);

proof end;

end;

:: deftheorem defines Ob CAT_6:def 17 :
for C being CategoryStr holds Ob C = { f where f is morphism of C : ( f is identity & f in Mor C ) } ;

definition

let C be CategoryStr ;
mode Object of C is Element of Ob C;

end;

registration

let C be non empty with_identities CategoryStr ;

cluster Ob C -> non empty ;

correctness
coherence
not Ob C is empty ;

proof end;

end;

theorem Th22: :: CAT_6:22

for C being non empty with_identities CategoryStr
for f being morphism of C holds
( f is identity iff f is Object of C )

proof end;

theorem Th23: :: CAT_6:23

for C being non empty with_identities CategoryStr
for f, f1 being morphism of C
for o being Object of C st f = o holds
( ( f |> f1 implies f (*) f1 = f1 ) & ( f1 |> f implies f1 (*) f = f1 ) & f |> f )

proof end;

theorem Th24: :: CAT_6:24

for C being non empty with_identities CategoryStr
for f being morphism of C st f is identity holds
f |> f

proof end;

theorem Th25: :: CAT_6:25

for C1, C2 being with_identities CategoryStr st CategoryStr(# the carrier of C1, the composition of C1 #) = CategoryStr(# the carrier of C2, the composition of C2 #) holds
for f1 being morphism of C1
for f2 being morphism of C2 st f1 = f2 holds
( f1 is identity iff f2 is identity )

proof end;

Lm2: for C being CategoryStr holds
( C is with_identities iff for f being morphism of C st f in Mor C holds
( ex c being morphism of C st
( c |> f & c is identity ) & ex d being morphism of C st
( f |> d & d is identity ) ) )

proof end;

Lm3: for C being CategoryStr holds
( C is composable iff for f, g, h being morphism of C holds
( ( h (*) g |> f & h |> g implies g |> f ) & ( h |> g (*) f & g |> f implies h |> g ) & ( g |> f & h |> g implies ( h (*) g |> f & h |> g (*) f ) ) ) )

proof end;

definition

let C be composable with_identities CategoryStr ;
let f be morphism of C;

func dom f -> Object of C means :Def18: :: CAT_6:def 18
ex f1 being morphism of C st
( it = f1 & f |> f1 & f1 is identity ) if not C is empty
otherwise it = the Object of C;

existence
( ( not C is empty implies ex b₁ being Object of C ex f1 being morphism of C st
( b₁ = f1 & f |> f1 & f1 is identity ) ) & ( C is empty implies ex b₁ being Object of C st b₁ = the Object of C ) )

proof end;

uniqueness
for b₁, b₂ being Object of C holds
( ( not C is empty & ex f1 being morphism of C st
( b₁ = f1 & f |> f1 & f1 is identity ) & ex f1 being morphism of C st
( b₂ = f1 & f |> f1 & f1 is identity ) implies b₁ = b₂ ) & ( C is empty & b₁ = the Object of C & b₂ = the Object of C implies b₁ = b₂ ) )

proof end;

correctness
consistency
for b₁ being Object of C holds verum;
;

func cod f -> Object of C means :Def19: :: CAT_6:def 19
ex f1 being morphism of C st
( it = f1 & f1 |> f & f1 is identity ) if not C is empty
otherwise it = the Object of C;

existence
( ( not C is empty implies ex b₁ being Object of C ex f1 being morphism of C st
( b₁ = f1 & f1 |> f & f1 is identity ) ) & ( C is empty implies ex b₁ being Object of C st b₁ = the Object of C ) )

proof end;

uniqueness
for b₁, b₂ being Object of C holds
( ( not C is empty & ex f1 being morphism of C st
( b₁ = f1 & f1 |> f & f1 is identity ) & ex f1 being morphism of C st
( b₂ = f1 & f1 |> f & f1 is identity ) implies b₁ = b₂ ) & ( C is empty & b₁ = the Object of C & b₂ = the Object of C implies b₁ = b₂ ) )

proof end;

correctness
consistency
for b₁ being Object of C holds verum;
;

end;

:: deftheorem Def18 defines dom CAT_6:def 18 :
for C being composable with_identities CategoryStr
for f being morphism of C
for b₃ being Object of C holds
( ( not C is empty implies ( b₃ = dom f iff ex f1 being morphism of C st
( b₃ = f1 & f |> f1 & f1 is identity ) ) ) & ( C is empty implies ( b₃ = dom f iff b₃ = the Object of C ) ) );

:: deftheorem Def19 defines cod CAT_6:def 19 :
for C being composable with_identities CategoryStr
for f being morphism of C
for b₃ being Object of C holds
( ( not C is empty implies ( b₃ = cod f iff ex f1 being morphism of C st
( b₃ = f1 & f1 |> f & f1 is identity ) ) ) & ( C is empty implies ( b₃ = cod f iff b₃ = the Object of C ) ) );

theorem Th26: :: CAT_6:26

for C being composable with_identities CategoryStr
for f, f1 being morphism of C st f |> f1 & f1 is identity holds
dom f = f1

proof end;

theorem Th27: :: CAT_6:27

for C being composable with_identities CategoryStr
for f, f1 being morphism of C st f1 |> f & f1 is identity holds
cod f = f1

proof end;

definition

let C be with_identities CategoryStr ;
let o be Object of C;

func id- o -> morphism of C equals :: CAT_6:def 20
o;

correctness
coherence
o is morphism of C;

proof end;

end;

:: deftheorem defines id- CAT_6:def 20 :
for C being with_identities CategoryStr
for o being Object of C holds id- o = o;

definition

let C, D be CategoryStr ;
mode Functor of C,D is Function of C,D;

end;

definition

let C, D be with_identities CategoryStr ;
let F be Functor of C,D;
let f be morphism of C;

func F . f -> morphism of D equals :Def21: :: CAT_6:def 21
F . f if not C is empty
otherwise the Object of D;

correctness
coherence
( ( not C is empty implies F . f is morphism of D ) & ( C is empty implies the Object of D is morphism of D ) );
consistency
for b₁ being morphism of D holds verum;

proof end;

end;

:: deftheorem Def21 defines . CAT_6:def 21 :
for C, D being with_identities CategoryStr
for F being Functor of C,D
for f being morphism of C holds
( ( not C is empty implies F . f = F . f ) & ( C is empty implies F . f = the Object of D ) );

definition

let C, D be with_identities CategoryStr ;
let F be Functor of C,D;

attr F is identity-preserving means :Def22: :: CAT_6:def 22
for f being morphism of C st f is identity holds
F . f is identity ;

attr F is multiplicative means :Def23: :: CAT_6:def 23
for f1, f2 being morphism of C st f1 |> f2 holds
( F . f1 |> F . f2 & F . (f1 (*) f2) = (F . f1) (*) (F . f2) );

attr F is antimultiplicative means :: CAT_6:def 24
for f1, f2 being morphism of C st f1 |> f2 holds
( F . f2 |> F . f1 & F . (f1 (*) f2) = (F . f2) (*) (F . f1) );

end;

:: deftheorem Def22 defines identity-preserving CAT_6:def 22 :
for C, D being with_identities CategoryStr
for F being Functor of C,D holds
( F is identity-preserving iff for f being morphism of C st f is identity holds
F . f is identity );

:: deftheorem Def23 defines multiplicative CAT_6:def 23 :
for C, D being with_identities CategoryStr
for F being Functor of C,D holds
( F is multiplicative iff for f1, f2 being morphism of C st f1 |> f2 holds
( F . f1 |> F . f2 & F . (f1 (*) f2) = (F . f1) (*) (F . f2) ) );

:: deftheorem defines antimultiplicative CAT_6:def 24 :
for C, D being with_identities CategoryStr
for F being Functor of C,D holds
( F is antimultiplicative iff for f1, f2 being morphism of C st f1 |> f2 holds
( F . f2 |> F . f1 & F . (f1 (*) f2) = (F . f2) (*) (F . f1) ) );

registration

let C, D be with_identities CategoryStr ;

cluster Relation-like the carrier of C -defined the carrier of D -valued Function-like V28( the carrier of C, the carrier of D) identity-preserving for Element of bool [: the carrier of C, the carrier of D:];

correctness
existence
ex b₁ being Functor of C,D st b₁ is identity-preserving ;

proof end;

end;

registration

let C be empty with_identities CategoryStr ;
let D be with_identities CategoryStr ;

cluster Relation-like non-empty empty-yielding the carrier of C -defined the carrier of D -valued empty trivial non proper V9() V10() V11() V13() V14() V15() V16() V17() V18() Function-like one-to-one constant functional total V28( the carrier of C, the carrier of D) V31() V100() V101() identity-preserving multiplicative antimultiplicative for Element of bool [: the carrier of C, the carrier of D:];

correctness
existence
ex b₁ being Functor of C,D st
( b₁ is identity-preserving & b₁ is multiplicative & b₁ is antimultiplicative );

proof end;

end;

registration

let C be with_identities CategoryStr ;
let D be non empty with_identities CategoryStr ;

cluster Relation-like the carrier of C -defined the carrier of D -valued Function-like total V28( the carrier of C, the carrier of D) identity-preserving multiplicative antimultiplicative for Element of bool [: the carrier of C, the carrier of D:];

correctness
existence
ex b₁ being Functor of C,D st
( b₁ is identity-preserving & b₁ is multiplicative & b₁ is antimultiplicative );

proof end;

end;

theorem :: CAT_6:28

ex C, D being category ex F being Functor of C,D st
( F is multiplicative & not F is identity-preserving )

proof end;

theorem Th29: :: CAT_6:29

for C, D being with_identities CategoryStr st not C is empty & D is empty holds
for F being Functor of C,D holds
( not F is multiplicative & not F is antimultiplicative )

proof end;

theorem :: CAT_6:30

ex C, D being category ex F being Functor of C,D st
( not F is multiplicative & F is identity-preserving )

proof end;

definition

let C, D be with_identities CategoryStr ;
let F be Functor of C,D;

attr F is covariant means :Def25: :: CAT_6:def 25
( F is identity-preserving & F is multiplicative );

attr F is contravariant means :: CAT_6:def 26
( F is identity-preserving & F is antimultiplicative );

end;

:: deftheorem Def25 defines covariant CAT_6:def 25 :
for C, D being with_identities CategoryStr
for F being Functor of C,D holds
( F is covariant iff ( F is identity-preserving & F is multiplicative ) );

:: deftheorem defines contravariant CAT_6:def 26 :
for C, D being with_identities CategoryStr
for F being Functor of C,D holds
( F is contravariant iff ( F is identity-preserving & F is antimultiplicative ) );

registration

let C be empty with_identities CategoryStr ;
let D be with_identities CategoryStr ;

cluster Relation-like non-empty empty-yielding the carrier of C -defined the carrier of D -valued empty trivial non proper V9() V10() V11() V13() V14() V15() V16() V17() V18() Function-like one-to-one constant functional total V28( the carrier of C, the carrier of D) V31() V100() V101() covariant contravariant for Element of bool [: the carrier of C, the carrier of D:];

correctness
existence
ex b₁ being Functor of C,D st
( b₁ is covariant & b₁ is contravariant );

proof end;

end;

registration

let C be with_identities CategoryStr ;
let D be non empty with_identities CategoryStr ;

cluster Relation-like the carrier of C -defined the carrier of D -valued Function-like total V28( the carrier of C, the carrier of D) covariant contravariant for Element of bool [: the carrier of C, the carrier of D:];

correctness
existence
ex b₁ being Functor of C,D st
( b₁ is covariant & b₁ is contravariant );

proof end;

end;

theorem :: CAT_6:31

for C, D being with_identities CategoryStr st not C is empty & D is empty holds
for F being Functor of C,D holds
( not F is covariant & not F is contravariant ) by Th29;

definition

let C, D be non empty with_identities CategoryStr ;
let F be covariant Functor of C,D;
let f be Object of C;
:: original: .
redefine func F . f -> Object of D;
coherence
F . f is Object of D

proof end;

end;

theorem Th32: :: CAT_6:32

for C, D being non empty composable with_identities CategoryStr
for F being covariant Functor of C,D
for f being morphism of C holds
( F . (dom f) = dom (F . f) & F . (cod f) = cod (F . f) )

proof end;

theorem :: CAT_6:33

for C, D being non empty composable with_identities CategoryStr
for F being covariant Functor of C,D
for o being Object of C holds F . (id- o) = id- (F . o) by Def21;

definition

let C, D, E be with_identities CategoryStr ;
let F be Functor of C,D;
let G be Functor of D,E;
assume A1: ( ( F is covariant or F is contravariant ) & ( G is covariant or G is contravariant ) ) ;

func G (*) F -> Functor of C,E equals :Def27: :: CAT_6:def 27
F * G;

coherence
F * G is Functor of C,E

proof end;

end;

:: deftheorem Def27 defines (*) CAT_6:def 27 :
for C, D, E being with_identities CategoryStr
for F being Functor of C,D
for G being Functor of D,E st ( F is covariant or F is contravariant ) & ( G is covariant or G is contravariant ) holds
G (*) F = F * G;

theorem Th34: :: CAT_6:34

for C, D, E being with_identities CategoryStr
for F being Functor of C,D
for G being Functor of D,E
for f being morphism of C st F is covariant & G is covariant & not C is empty holds
(G (*) F) . f = G . (F . f)

proof end;

theorem :: CAT_6:35

for C, D, E being with_identities CategoryStr
for F being Functor of C,D
for G being Functor of D,E st F is covariant & G is covariant holds
G (*) F is covariant

proof end;

definition

let C be with_identities CategoryStr ;
:: original: id
redefine func id C -> Functor of C,C;
coherence
id C is Functor of C,C ;

end;

registration

let C be with_identities CategoryStr ;

cluster id C -> covariant ;

correctness
coherence
id C is covariant ;

proof end;

end;

definition

let C, D be with_identities CategoryStr ;

pred C,D are_isomorphic means :: CAT_6:def 28
ex F being Functor of C,D ex G being Functor of D,C st
( F is covariant & G is covariant & G (*) F = id C & F (*) G = id D );

reflexivity
for C being with_identities CategoryStr ex F, G being Functor of C,C st
( F is covariant & G is covariant & G (*) F = id C & F (*) G = id C )

proof end;

symmetry
for C, D being with_identities CategoryStr st ex F being Functor of C,D ex G being Functor of D,C st
( F is covariant & G is covariant & G (*) F = id C & F (*) G = id D ) holds
ex F being Functor of D,C ex G being Functor of C,D st
( F is covariant & G is covariant & G (*) F = id D & F (*) G = id C ) ;

end;

:: deftheorem defines are_isomorphic CAT_6:def 28 :
for C, D being with_identities CategoryStr holds
( C,D are_isomorphic iff ex F being Functor of C,D ex G being Functor of D,C st
( F is covariant & G is covariant & G (*) F = id C & F (*) G = id D ) );

notation

let C, D be with_identities CategoryStr ;
synonym C ~= D for C,D are_isomorphic ;

end;

Lm4: for C being CategoryStr
for f, g being morphism of C st g |> f holds
g (*) f = the composition of C . [g,f]

proof end;

Lm5: for C being composable CategoryStr holds
( C is associative iff for f, g, h being morphism of C st h |> g & g |> f holds
h (*) (g (*) f) = (h (*) g) (*) f )

proof end;

definition

let C be CategoryStr ;

func CompMap C -> PartFunc of [:(Mor C),(Mor C):],(Mor C) equals :: CAT_6:def 29
the composition of C;

correctness
coherence
the composition of C is PartFunc of [:(Mor C),(Mor C):],(Mor C);
;

end;

:: deftheorem defines CompMap CAT_6:def 29 :
for C being CategoryStr holds CompMap C = the composition of C;

definition

let C be composable with_identities CategoryStr ;

func SourceMap C -> Function of (Mor C),(Ob C) means :Def30: :: CAT_6:def 30
for f being Element of Mor C holds it . f = dom f if not C is empty
otherwise it = {} ;

correctness
consistency
for b₁ being Function of (Mor C),(Ob C) holds verum;
existence
( ( for b₁ being Function of (Mor C),(Ob C) holds verum ) & ( not C is empty implies ex b₁ being Function of (Mor C),(Ob C) st
for f being Element of Mor C holds b₁ . f = dom f ) & ( C is empty implies ex b₁ being Function of (Mor C),(Ob C) st b₁ = {} ) );
uniqueness
for b₁, b₂ being Function of (Mor C),(Ob C) holds
( ( not C is empty & ( for f being Element of Mor C holds b₁ . f = dom f ) & ( for f being Element of Mor C holds b₂ . f = dom f ) implies b₁ = b₂ ) & ( C is empty & b₁ = {} & b₂ = {} implies b₁ = b₂ ) );

proof end;

func TargetMap C -> Function of (Mor C),(Ob C) means :Def31: :: CAT_6:def 31
for f being Element of Mor C holds it . f = cod f if not C is empty
otherwise it = {} ;

correctness
consistency
for b₁ being Function of (Mor C),(Ob C) holds verum;
existence
( ( for b₁ being Function of (Mor C),(Ob C) holds verum ) & ( not C is empty implies ex b₁ being Function of (Mor C),(Ob C) st
for f being Element of Mor C holds b₁ . f = cod f ) & ( C is empty implies ex b₁ being Function of (Mor C),(Ob C) st b₁ = {} ) );
uniqueness
for b₁, b₂ being Function of (Mor C),(Ob C) holds
( ( not C is empty & ( for f being Element of Mor C holds b₁ . f = cod f ) & ( for f being Element of Mor C holds b₂ . f = cod f ) implies b₁ = b₂ ) & ( C is empty & b₁ = {} & b₂ = {} implies b₁ = b₂ ) );

proof end;

end;

:: deftheorem Def30 defines SourceMap CAT_6:def 30 :
for C being composable with_identities CategoryStr
for b₂ being Function of (Mor C),(Ob C) holds
( ( not C is empty implies ( b₂ = SourceMap C iff for f being Element of Mor C holds b₂ . f = dom f ) ) & ( C is empty implies ( b₂ = SourceMap C iff b₂ = {} ) ) );

:: deftheorem Def31 defines TargetMap CAT_6:def 31 :
for C being composable with_identities CategoryStr
for b₂ being Function of (Mor C),(Ob C) holds
( ( not C is empty implies ( b₂ = TargetMap C iff for f being Element of Mor C holds b₂ . f = cod f ) ) & ( C is empty implies ( b₂ = TargetMap C iff b₂ = {} ) ) );

definition

let C be with_identities CategoryStr ;

func IdMap C -> Function of (Ob C),(Mor C) means :Def32: :: CAT_6:def 32
for o being Element of Ob C holds it . o = id- o if not C is empty
otherwise it = {} ;

correctness
consistency
for b₁ being Function of (Ob C),(Mor C) holds verum;
existence
( ( for b₁ being Function of (Ob C),(Mor C) holds verum ) & ( not C is empty implies ex b₁ being Function of (Ob C),(Mor C) st
for o being Element of Ob C holds b₁ . o = id- o ) & ( C is empty implies ex b₁ being Function of (Ob C),(Mor C) st b₁ = {} ) );
uniqueness
for b₁, b₂ being Function of (Ob C),(Mor C) holds
( ( not C is empty & ( for o being Element of Ob C holds b₁ . o = id- o ) & ( for o being Element of Ob C holds b₂ . o = id- o ) implies b₁ = b₂ ) & ( C is empty & b₁ = {} & b₂ = {} implies b₁ = b₂ ) );

proof end;

end;

:: deftheorem Def32 defines IdMap CAT_6:def 32 :
for C being with_identities CategoryStr
for b₂ being Function of (Ob C),(Mor C) holds
( ( not C is empty implies ( b₂ = IdMap C iff for o being Element of Ob C holds b₂ . o = id- o ) ) & ( C is empty implies ( b₂ = IdMap C iff b₂ = {} ) ) );

theorem Th37: :: CAT_6:36

for C being non empty composable with_identities CategoryStr
for f, g being Element of Mor C holds
( [g,f] in dom (CompMap C) iff (SourceMap C) . g = (TargetMap C) . f )

proof end;

theorem Th38: :: CAT_6:37

for C being composable with_identities CategoryStr
for f, g being Element of Mor C st (SourceMap C) . g = (TargetMap C) . f holds
( (SourceMap C) . ((CompMap C) . (g,f)) = (SourceMap C) . f & (TargetMap C) . ((CompMap C) . (g,f)) = (TargetMap C) . g )

proof end;

theorem Th39: :: CAT_6:38

for C being associative composable with_identities CategoryStr
for f, g, h being Element of Mor C st (SourceMap C) . h = (TargetMap C) . g & (SourceMap C) . g = (TargetMap C) . f holds
(CompMap C) . (h,((CompMap C) . (g,f))) = (CompMap C) . (((CompMap C) . (h,g)),f)

proof end;

theorem Th40: :: CAT_6:39

for C being composable with_identities CategoryStr
for b being Element of Ob C holds
( (SourceMap C) . ((IdMap C) . b) = b & (TargetMap C) . ((IdMap C) . b) = b & ( for f being Element of Mor C st (TargetMap C) . f = b holds
(CompMap C) . (((IdMap C) . b),f) = f ) & ( for g being Element of Mor C st (SourceMap C) . g = b holds
(CompMap C) . (g,((IdMap C) . b)) = g ) )

proof end;

Lm6: for C being non empty category holds CatStr(# (Ob C),(Mor C),(SourceMap C),(TargetMap C),(CompMap C) #) is Category

proof end;

definition

let C be non empty category;

func Alter C -> strict Category equals :: CAT_6:def 33
CatStr(# (Ob C),(Mor C),(SourceMap C),(TargetMap C),(CompMap C) #);

coherence
CatStr(# (Ob C),(Mor C),(SourceMap C),(TargetMap C),(CompMap C) #) is strict Category by Lm6;

end;

:: deftheorem defines Alter CAT_6:def 33 :
for C being non empty category holds Alter C = CatStr(# (Ob C),(Mor C),(SourceMap C),(TargetMap C),(CompMap C) #);

Lm7: for C being Category holds CategoryStr(# the carrier' of C, the Comp of C #) is category

proof end;

definition

let A be Category;

func alter A -> strict category equals :: CAT_6:def 34
CategoryStr(# the carrier' of A, the Comp of A #);

coherence
CategoryStr(# the carrier' of A, the Comp of A #) is strict category by Lm7;

end;

:: deftheorem defines alter CAT_6:def 34 :
for A being Category holds alter A = CategoryStr(# the carrier' of A, the Comp of A #);

registration

let A be Category;

cluster alter A -> non empty strict ;

correctness
coherence
not alter A is empty ;
;

end;

theorem Th41: :: CAT_6:40

for A being Category
for a1, a2 being Morphism of A
for f1, f2 being morphism of (alter A) st a1 = f1 & a2 = f2 & [a1,a2] in dom the Comp of A holds
a1 (*) a2 = f1 (*) f2

proof end;

theorem Th42: :: CAT_6:41

for A being Category
for f being morphism of (alter A) holds
( f is identity iff ex o being Object of A st f = id o )

proof end;

theorem :: CAT_6:42

for A, B being Category
for F being Functor of A,B holds F is covariant Functor of (alter A),(alter B)

proof end;

theorem Th44: :: CAT_6:43

for C being non empty category
for a1, a2 being Morphism of (Alter C)
for f1, f2 being morphism of C st a1 = f1 & a2 = f2 & f1 |> f2 holds
a1 (*) a2 = f1 (*) f2

proof end;

theorem Th45: :: CAT_6:44

for C being non empty category
for f1 being morphism of C
for a1 being Morphism of (Alter C) st a1 = f1 holds
( dom f1 = dom a1 & cod f1 = cod a1 )

proof end;

theorem Th46: :: CAT_6:45

for C being non empty category
for o1 being Object of C
for o2 being Object of (Alter C) st o1 = o2 holds
id- o1 = id o2

proof end;

theorem Th47: :: CAT_6:46

for C being non empty category
for f being morphism of C holds
( f is identity iff ex o being Object of (Alter C) st f = id o )

proof end;

theorem :: CAT_6:47

for C, D being non empty category
for F being covariant Functor of C,D holds F is Functor of Alter C, Alter D

proof end;

theorem Th49: :: CAT_6:48

for C, D being Category
for F being covariant Functor of (alter C),(alter D) holds F is Functor of C,D

proof end;

theorem Th50: :: CAT_6:49

for C1, C2 being Category st alter C1 ~= alter C2 holds
C1 ~= C2

proof end;

theorem Th51: :: CAT_6:50

for C1, C2 being Category st the carrier' of C1 = the carrier' of C2 & the Comp of C1 = the Comp of C2 holds
C1 ~= C2

proof end;

theorem :: CAT_6:51

for C being Category holds C ~= Alter (alter C) by Th51;

theorem :: CAT_6:52

for C being non empty category holds C ~= alter (Alter C)

proof end;