:: Natural Transformations. Discrete Categories
:: by Andrzej Trybulec
::
:: Received May 15, 1991
:: Copyright (c) 1991-2012 Association of Mizar Users


begin

definition
let A1 be set ;
let B1 be non empty set ;
let f be Function of A1,B1;
let Y1 be Subset of A1;
:: original:|
redefine funcf | Y1 ->  Function of Y1,B1;
coherence
 f | Y1 is Function of Y1,B1 by FUNCT_2:32;
end;

theorem Th1: :: NATTRA_1:1
for B1, B2, A1, A2 being non empty set
for f being Function of A1,B1
for g being Function of A2,B2
for Y1 being non empty Subset of A1
for Y2 being non empty Subset of A2 holds [:f,g:] | [:Y1,Y2:] = [:(f | Y1),(g | Y2):]
proofend;

definition
let A, B be non empty set ;
let A1 be non empty Subset of A;
let B1 be non empty Subset of B;
let f be PartFunc of [:A1,A1:],A1;
let g be PartFunc of [:B1,B1:],B1;
:: original:|:
redefine func|:f,g:| ->  PartFunc of [:[:A1,B1:],[:A1,B1:]:],[:A1,B1:];
coherence
 |:f,g:| is PartFunc of [:[:A1,B1:],[:A1,B1:]:],[:A1,B1:] by FUNCT_4:59;
end;

theorem Th2: :: NATTRA_1:2
for A1, A2 being non empty set
for Y1 being non empty Subset of A1
for Y2 being non empty Subset of A2
for f being PartFunc of [:A1,A1:],A1
for g being PartFunc of [:A2,A2:],A2
for F being PartFunc of [:Y1,Y1:],Y1 st F = f || Y1 holds
for G being PartFunc of [:Y2,Y2:],Y2 st G = g || Y2 holds
|:F,G:| = |:f,g:| || [:Y1,Y2:]
proofend;

theorem :: NATTRA_1:3
canceled;

theorem Th4: :: NATTRA_1:4
for o, m being set
for f, g being Morphism of (1Cat (o,m)) holds f = g
proofend;

theorem Th5: :: NATTRA_1:5
for A being Category
for a being Object of A holds [[(id a),(id a)],(id a)] in the Comp of A
proofend;

theorem Th6: :: NATTRA_1:6
for o, m being set holds the Comp of (1Cat (o,m)) = {[[m,m],m]}
proofend;

theorem Th7: :: NATTRA_1:7
for A being Category
for a being Object of A holds 1Cat (a,(id a)) is Subcategory of A
proofend;

theorem Th8: :: NATTRA_1:8
for A being Category
for C being Subcategory of A holds
( the Source of C = the Source of A | the carrier' of C & the Target of C = the Target of A | the carrier' of C & the Comp of C = the Comp of A || the carrier' of C )
proofend;

theorem Th9: :: NATTRA_1:9
for A being Category
for O being non empty Subset of the carrier of A
for M being non empty Subset of the carrier' of A st ( for o being Element of A st o in O holds
id o in M ) holds
for DOM, COD being Function of M,O st DOM = the Source of A | M & COD = the Target of A | M holds
for COMP being PartFunc of [:M,M:],M st COMP = the Comp of A || M holds
CatStr(# O,M,DOM,COD,COMP #) is Subcategory of A
proofend;

theorem Th10: :: NATTRA_1:10
for C being strict Category
for A being strict Subcategory of C st the carrier of A = the carrier of C & the carrier' of A = the carrier' of C holds
A = C
proofend;

begin

definition
canceled;
end;

:: deftheorem  NATTRA_1:def_1_:_
canceled;

theorem :: NATTRA_1:11
for B, C, A being Category
for F being Functor of A,B
for G being Functor of B,C
for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (G * F) /. f = G /. (F /. f)
proofend;

:: The following theorems are analogues of theorems from CAT_1, with
:: the new concept of the application of a functor to a morphism
theorem :: NATTRA_1:12
for A, B being Category
for F1, F2 being Functor of A,B st ( for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds F1 . f = F2 . f ) holds
F1 = F2
proofend;

theorem Th13: :: NATTRA_1:13
for B, A being Category
for F being Functor of A,B
for a, b, c being Object of A st Hom (a,b) <> {} &amp; Hom (b,c) <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c holds F /. (g * f) = (F /. g) * (F /. f)
proofend;

theorem :: NATTRA_1:14
for A, B being Category
for F being Functor of A,B
for c being Object of A
for d being Object of B st F /. (id c) = id d holds
F . c = d
proofend;

theorem Th15: :: NATTRA_1:15
for B, A being Category
for F being Functor of A,B
for a being Object of A holds F /. (id a) = id (F . a)
proofend;

theorem :: NATTRA_1:16
for A being Category
for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (id A) /. f = f
proofend;

theorem Th17: :: NATTRA_1:17
for A being Category
for a, b, c, d being Object of A st Hom (a,b) meets Hom (c,d) holds
( a = c &amp; b = d )
proofend;

begin

definition
let A, B be Category;
let F1, F2 be Functor of A,B;
predF1 is_transformable_to F2 means :Def2: :: NATTRA_1:def 2
 for a being Object of A holds Hom ((F1 . a),(F2 . a)) <> {} ;
reflexivity
 for F1 being Functor of A,B
for a being Object of A holds Hom ((F1 . a),(F1 . a)) <> {} ;
end;

:: deftheorem Def2 defines is_transformable_to NATTRA_1:def_2_:_
 for A, B being Category
for F1, F2 being Functor of A,B holds
( F1 is_transformable_to F2 iff for a being Object of A holds Hom ((F1 . a),(F2 . a)) <> {} );

theorem Th18: :: NATTRA_1:18
for A, B being Category
for F, F1, F2 being Functor of A,B st F is_transformable_to F1 &amp; F1 is_transformable_to F2 holds
F is_transformable_to F2
proofend;

definition
let A, B be Category;
let F1, F2 be Functor of A,B;
assume A1: F1 is_transformable_to F2 ;
mode transformation of F1,F2 ->  Function of the carrier of A, the carrier' of B means :Def3: :: NATTRA_1:def 3
 for a being Object of A holds it . a is Morphism of F1 . a,F2 . a;
existence
 ex b1 being Function of the carrier of A, the carrier' of B st
for a being Object of A holds b1 . a is Morphism of F1 . a,F2 . a
proofend;
end;

:: deftheorem Def3 defines transformation NATTRA_1:def_3_:_
 for A, B being Category
for F1, F2 being Functor of A,B st F1 is_transformable_to F2 holds
for b5 being Function of the carrier of A, the carrier' of B holds
( b5 is transformation of F1,F2 iff for a being Object of A holds b5 . a is Morphism of F1 . a,F2 . a );

definition
let A, B be Category;
let F be Functor of A,B;
func id F ->  transformation of F,F means :Def4: :: NATTRA_1:def 4
 for a being Object of A holds it . a = id (F . a);
existence
 ex b1 being transformation of F,F st
for a being Object of A holds b1 . a = id (F . a)
proofend;
uniqueness
 for b1, b2 being transformation of F,F st ( for a being Object of A holds b1 . a = id (F . a) ) &amp; ( for a being Object of A holds b2 . a = id (F . a) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def4 defines id NATTRA_1:def_4_:_
 for A, B being Category
for F being Functor of A,B
for b4 being transformation of F,F holds
( b4 = id F iff for a being Object of A holds b4 . a = id (F . a) );

definition
let A, B be Category;
let F1, F2 be Functor of A,B;
assume A1: F1 is_transformable_to F2 ;
let t be transformation of F1,F2;
let a be Object of A;
funct . a ->  Morphism of F1 . a,F2 . a equals :Def5: :: NATTRA_1:def 5
t . a;
coherence
 t . a is Morphism of F1 . a,F2 . a by A1, Def3;
end;

:: deftheorem Def5 defines . NATTRA_1:def_5_:_
 for A, B being Category
for F1, F2 being Functor of A,B st F1 is_transformable_to F2 holds
for t being transformation of F1,F2
for a being Object of A holds t . a = t . a;

definition
let A, B be Category;
let F, F1, F2 be Functor of A,B;
assume that
A1: F is_transformable_to F1 and
A2: F1 is_transformable_to F2 ;
let t1 be transformation of F,F1;
let t2 be transformation of F1,F2;
funct2 `*` t1 ->  transformation of F,F2 means :Def6: :: NATTRA_1:def 6
 for a being Object of A holds it . a = (t2 . a) * (t1 . a);
existence
 ex b1 being transformation of F,F2 st
for a being Object of A holds b1 . a = (t2 . a) * (t1 . a)
proofend;
uniqueness
 for b1, b2 being transformation of F,F2 st ( for a being Object of A holds b1 . a = (t2 . a) * (t1 . a) ) &amp; ( for a being Object of A holds b2 . a = (t2 . a) * (t1 . a) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def6 defines `*` NATTRA_1:def_6_:_
 for A, B being Category
for F, F1, F2 being Functor of A,B st F is_transformable_to F1 &amp; F1 is_transformable_to F2 holds
for t1 being transformation of F,F1
for t2 being transformation of F1,F2
for b8 being transformation of F,F2 holds
( b8 = t2 `*` t1 iff for a being Object of A holds b8 . a = (t2 . a) * (t1 . a) );

theorem Th19: :: NATTRA_1:19
for B, A being Category
for F1, F2 being Functor of A,B st F1 is_transformable_to F2 holds
for t1, t2 being transformation of F1,F2 st ( for a being Object of A holds t1 . a = t2 . a ) holds
t1 = t2
proofend;

theorem Th20: :: NATTRA_1:20
for B, A being Category
for F being Functor of A,B
for a being Object of A holds (id F) . a = id (F . a)
proofend;

theorem Th21: :: NATTRA_1:21
for A, B being Category
for F1, F2 being Functor of A,B st F1 is_transformable_to F2 holds
for t being transformation of F1,F2 holds
( (id F2) `*` t = t &amp; t `*` (id F1) = t )
proofend;

theorem Th22: :: NATTRA_1:22
for A, B being Category
for F, F1, F2, F3 being Functor of A,B st F is_transformable_to F1 &amp; F1 is_transformable_to F2 &amp; F2 is_transformable_to F3 holds
for t1 being transformation of F,F1
for t2 being transformation of F1,F2
for t3 being transformation of F2,F3 holds (t3 `*` t2) `*` t1 = t3 `*` (t2 `*` t1)
proofend;

begin

Lm1:  for B, A being Category
for F being Functor of A,B
for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds ((id F) . b) * (F /. f) = (F /. f) * ((id F) . a)
proofend;

definition
let A, B be Category;
let F1, F2 be Functor of A,B;
predF1 is_naturally_transformable_to F2 means :Def7: :: NATTRA_1:def 7
( F1 is_transformable_to F2 &amp; ex t being transformation of F1,F2 st
for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (t . b) * (F1 /. f) = (F2 /. f) * (t . a) );
reflexivity
 for F1 being Functor of A,B holds
( F1 is_transformable_to F1 &amp; ex t being transformation of F1,F1 st
for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (t . b) * (F1 /. f) = (F1 /. f) * (t . a) )
proofend;
end;

:: deftheorem Def7 defines is_naturally_transformable_to NATTRA_1:def_7_:_
 for A, B being Category
for F1, F2 being Functor of A,B holds
( F1 is_naturally_transformable_to F2 iff ( F1 is_transformable_to F2 &amp; ex t being transformation of F1,F2 st
for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (t . b) * (F1 /. f) = (F2 /. f) * (t . a) ) );

Lm2:  for B, A being Category
for F, F1, F2 being Functor of A,B st F is_transformable_to F1 &amp; F1 is_transformable_to F2 holds
for t1 being transformation of F,F1 st ( for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (t1 . b) * (F /. f) = (F1 /. f) * (t1 . a) ) holds
for t2 being transformation of F1,F2 st ( for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (t2 . b) * (F1 /. f) = (F2 /. f) * (t2 . a) ) holds
for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds ((t2 `*` t1) . b) * (F /. f) = (F2 /. f) * ((t2 `*` t1) . a)
proofend;

theorem Th23: :: NATTRA_1:23
for A, B being Category
for F, F1, F2 being Functor of A,B st F is_naturally_transformable_to F1 &amp; F1 is_naturally_transformable_to F2 holds
F is_naturally_transformable_to F2
proofend;

definition
let A, B be Category;
let F1, F2 be Functor of A,B;
assume A1: F1 is_naturally_transformable_to F2 ;
mode natural_transformation of F1,F2 ->  transformation of F1,F2 means :Def8: :: NATTRA_1:def 8
 for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (it . b) * (F1 /. f) = (F2 /. f) * (it . a);
existence
 ex b1 being transformation of F1,F2 st
for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (b1 . b) * (F1 /. f) = (F2 /. f) * (b1 . a) by A1, Def7;
end;

:: deftheorem Def8 defines natural_transformation NATTRA_1:def_8_:_
 for A, B being Category
for F1, F2 being Functor of A,B st F1 is_naturally_transformable_to F2 holds
for b5 being transformation of F1,F2 holds
( b5 is natural_transformation of F1,F2 iff for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (b5 . b) * (F1 /. f) = (F2 /. f) * (b5 . a) );

definition
let A, B be Category;
let F be Functor of A,B;
:: original:id
redefine func id F ->  natural_transformation of F,F;
coherence
 id F is natural_transformation of F,F
proofend;
end;

definition
let A, B be Category;
let F, F1, F2 be Functor of A,B;
assume that
B1: F is_naturally_transformable_to F1 and
B2: F1 is_naturally_transformable_to F2 ;
let t1 be natural_transformation of F,F1;
let t2 be natural_transformation of F1,F2;
funct2 `*` t1 ->  natural_transformation of F,F2 equals :Def9: :: NATTRA_1:def 9
t2 `*` t1;
coherence
 t2 `*` t1 is natural_transformation of F,F2
proofend;
end;

:: deftheorem Def9 defines `*` NATTRA_1:def_9_:_
 for A, B being Category
for F, F1, F2 being Functor of A,B st F is_naturally_transformable_to F1 &amp; F1 is_naturally_transformable_to F2 holds
for t1 being natural_transformation of F,F1
for t2 being natural_transformation of F1,F2 holds t2 `*` t1 = t2 `*` t1;

theorem Th24: :: NATTRA_1:24
for A, B being Category
for F1, F2 being Functor of A,B st F1 is_naturally_transformable_to F2 holds
for t being natural_transformation of F1,F2 holds
( (id F2) `*` t = t &amp; t `*` (id F1) = t )
proofend;

theorem Th25: :: NATTRA_1:25
for B, A being Category
for F, F1, F2 being Functor of A,B st F is_naturally_transformable_to F1 &amp; F1 is_naturally_transformable_to F2 holds
for t1 being natural_transformation of F,F1
for t2 being natural_transformation of F1,F2
for a being Object of A holds (t2 `*` t1) . a = (t2 . a) * (t1 . a)
proofend;

theorem Th26: :: NATTRA_1:26
for A, B being Category
for F, F1, F2, F3 being Functor of A,B
for t being natural_transformation of F,F1
for t1 being natural_transformation of F1,F2 st F is_naturally_transformable_to F1 &amp; F1 is_naturally_transformable_to F2 &amp; F2 is_naturally_transformable_to F3 holds
for t3 being natural_transformation of F2,F3 holds (t3 `*` t1) `*` t = t3 `*` (t1 `*` t)
proofend;

:: Natural equivalences
definition
let A, B be Category;
let F1, F2 be Functor of A,B;
let IT be transformation of F1,F2;
attrIT is invertible  means :Def10: :: NATTRA_1:def 10
 for a being Object of A holds IT . a is invertible ;
end;

:: deftheorem Def10 defines invertible NATTRA_1:def_10_:_
 for A, B being Category
for F1, F2 being Functor of A,B
for IT being transformation of F1,F2 holds
( IT is invertible iff for a being Object of A holds IT . a is invertible );

definition
let A, B be Category;
let F1, F2 be Functor of A,B;
predF1,F2 are_naturally_equivalent  means :Def11: :: NATTRA_1:def 11
( F1 is_naturally_transformable_to F2 &amp; ex t being natural_transformation of F1,F2 st t is invertible );
reflexivity
 for F1 being Functor of A,B holds
( F1 is_naturally_transformable_to F1 &amp; ex t being natural_transformation of F1,F1 st t is invertible )
proofend;
end;

:: deftheorem Def11 defines are_naturally_equivalent NATTRA_1:def_11_:_
 for A, B being Category
for F1, F2 being Functor of A,B holds
( F1,F2 are_naturally_equivalent iff ( F1 is_naturally_transformable_to F2 &amp; ex t being natural_transformation of F1,F2 st t is invertible ) );

notation
let A, B be Category;
let F1, F2 be Functor of A,B;
synonym F1 ~= F2 for F1,F2 are_naturally_equivalent ;
end;

Lm3:  for A, B being Category
for F1, F2 being Functor of A,B
for t being transformation of F1,F2 st F1 is_transformable_to F2 &amp; t is invertible holds
F2 is_transformable_to F1
proofend;

definition
let A, B be Category;
let F1, F2 be Functor of A,B;
assume B1: F1 is_transformable_to F2 ;
let t1 be transformation of F1,F2;
assume B2: t1 is invertible ;
funct1 "  ->  transformation of F2,F1 means :Def12: :: NATTRA_1:def 12
 for a being Object of A holds it . a = (t1 . a) " ;
existence
 ex b1 being transformation of F2,F1 st
for a being Object of A holds b1 . a = (t1 . a) "
proofend;
uniqueness
 for b1, b2 being transformation of F2,F1 st ( for a being Object of A holds b1 . a = (t1 . a) " ) &amp; ( for a being Object of A holds b2 . a = (t1 . a) " ) holds
b1 = b2
proofend;
end;

:: deftheorem Def12 defines " NATTRA_1:def_12_:_
 for A, B being Category
for F1, F2 being Functor of A,B st F1 is_transformable_to F2 holds
for t1 being transformation of F1,F2 st t1 is invertible holds
for b6 being transformation of F2,F1 holds
( b6 = t1 " iff for a being Object of A holds b6 . a = (t1 . a) " );

Lm4: now__::_thesis:_for_A,_B_being_Category
for_F1,_F2_being_Functor_of_A,B
for_t1_being_natural_transformation_of_F1,F2_st_F1_is_naturally_transformable_to_F2_&amp;_t1_is_invertible_holds_
for_a,_b_being_Object_of_A_st_Hom_(a,b)_<>_{}_holds_
for_f_being_Morphism_of_a,b_holds_((t1_")_._b)_*_(F2_/._f)_=_(F1_/._f)_*_((t1_")_._a)
let A, B be Category; ::_thesis: for F1, F2 being Functor of A,B
for t1 being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 &amp; t1 is invertible holds
for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds ((t1 ") . b) * (F2 /. f) = (F1 /. f) * ((t1 ") . a)
let F1, F2 be Functor of A,B; ::_thesis: for t1 being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 &amp; t1 is invertible holds
for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds ((t1 ") . b) * (F2 /. f) = (F1 /. f) * ((t1 ") . a)
let t1 be natural_transformation of F1,F2; ::_thesis: ( F1 is_naturally_transformable_to F2 &amp; t1 is invertible implies for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds ((t1 ") . b) * (F2 /. f) = (F1 /. f) * ((t1 ") . a) )
assume that
A1: F1 is_naturally_transformable_to F2 and
A2: t1 is invertible ; ::_thesis: for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds ((t1 ") . b) * (F2 /. f) = (F1 /. f) * ((t1 ") . a)
let a, b be Object of A; ::_thesis: ( Hom (a,b) <> {} implies for f being Morphism of a,b holds ((t1 ") . b) * (F2 /. f) = (F1 /. f) * ((t1 ") . a) )
assume A3: Hom (a,b) <> {} ; ::_thesis: for f being Morphism of a,b holds ((t1 ") . b) * (F2 /. f) = (F1 /. f) * ((t1 ") . a)
A4: Hom ((F1 . a),(F1 . b)) <> {} by A3, CAT_1:84;
let f be Morphism of a,b; ::_thesis: ((t1 ") . b) * (F2 /. f) = (F1 /. f) * ((t1 ") . a)
A5: Hom ((F2 . a),(F2 . b)) <> {} by A3, CAT_1:84;
A6: F1 is_transformable_to F2 by A1, Def7;
A7: Hom ((F1 . b),(F2 . b)) <> {} by Def2, A1, Def7;
A8: t1 . b is invertible by A2, Def10;
then A9: Hom ((F2 . b),(F1 . b)) <> {} by A7, CAT_1:41;
A10: Hom ((F1 . a),(F2 . a)) <> {} by A1, Def7, Def2;
 (F2 /. f) * (t1 . a) = (t1 . b) * (F1 /. f) by A1, A3, Def8;
then A11: (((t1 . b) ") * (F2 /. f)) * (t1 . a) = ((t1 . b) ") * ((t1 . b) * (F1 /. f)) by A10, A9, A5, CAT_1:25
.= (((t1 . b) ") * (t1 . b)) * (F1 /. f) by A4, A7, A9, CAT_1:25
.= (id (F1 . b)) * (F1 /. f) by A8, CAT_1:def_17
.= F1 /. f by A4, CAT_1:28 ;
A12: t1 . a is invertible by A2, Def10;
then A13: Hom ((F2 . a),(F1 . a)) <> {} by A10, CAT_1:41;
then A14: Hom ((F2 . a),(F1 . b)) <> {} by A4, CAT_1:24;
then ((t1 . b) ") * (F2 /. f) = (((t1 . b) ") * (F2 /. f)) * (id (F2 . a)) by CAT_1:29
.= (((t1 . b) ") * (F2 /. f)) * ((t1 . a) * ((t1 . a) ")) by A12, CAT_1:def_17
.= (F1 /. f) * ((t1 . a) ") by A10, A13, A14, A11, CAT_1:25 ;
hence ((t1 ") . b) * (F2 /. f) = (F1 /. f) * ((t1 . a) ") by A2, A6, Def12
.= (F1 /. f) * ((t1 ") . a) by A2, A6, Def12 ;
::_thesis: verum
end;

Lm5:  for A, B being Category
for F1, F2 being Functor of A,B
for t1 being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 &amp; t1 is invertible holds
F2 is_naturally_transformable_to F1
proofend;

definition
let A, B be Category;
let F1, F2 be Functor of A,B;
let t1 be natural_transformation of F1,F2;
assume that
B1: F1 is_naturally_transformable_to F2 and
B2: t1 is invertible ;
funct1 "  ->  natural_transformation of F2,F1 equals :Def13: :: NATTRA_1:def 13
t1 " ;
coherence
 t1 " is natural_transformation of F2,F1
proofend;
end;

:: deftheorem Def13 defines " NATTRA_1:def_13_:_
 for A, B being Category
for F1, F2 being Functor of A,B
for t1 being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 &amp; t1 is invertible holds
t1 " = t1 " ;

theorem Th27: :: NATTRA_1:27
for A, B being Category
for F1, F2 being Functor of A,B
for t1 being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 &amp; t1 is invertible holds
for a being Object of A holds (t1 ") . a = (t1 . a) "
proofend;

theorem :: NATTRA_1:28
for A, B being Category
for F1, F2 being Functor of A,B st F1 ~= F2 holds
F2 ~= F1
proofend;

theorem Th29: :: NATTRA_1:29
for A, B being Category
for F1, F2, F3 being Functor of A,B st F1 ~= F2 &amp; F2 ~= F3 holds
F1 ~= F3
proofend;

definition
let A, B be Category;
let F1, F2 be Functor of A,B;
assume A1: F1,F2 are_naturally_equivalent ;
mode natural_equivalence of F1,F2 ->  natural_transformation of F1,F2 means :Def14: :: NATTRA_1:def 14
it is invertible ;
existence
 ex b1 being natural_transformation of F1,F2 st b1 is invertible by A1, Def11;
end;

:: deftheorem Def14 defines natural_equivalence NATTRA_1:def_14_:_
 for A, B being Category
for F1, F2 being Functor of A,B st F1,F2 are_naturally_equivalent holds
for b5 being natural_transformation of F1,F2 holds
( b5 is natural_equivalence of F1,F2 iff b5 is invertible );

theorem :: NATTRA_1:30
for A, B being Category
for F being Functor of A,B holds id F is natural_equivalence of F,F
proofend;

theorem :: NATTRA_1:31
for A, B being Category
for F1, F2, F3 being Functor of A,B st F1 ~= F2 &amp; F2 ~= F3 holds
for t being natural_equivalence of F1,F2
for t9 being natural_equivalence of F2,F3 holds t9 `*` t is natural_equivalence of F1,F3
proofend;

begin

definition
let A, B be Category;
mode NatTrans-DOMAIN of A,B ->  non empty set  means :Def15: :: NATTRA_1:def 15
 for x being set st x in it holds
ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st
( x = [[F1,F2],t] &amp; F1 is_naturally_transformable_to F2 );
existence
 ex b1 being non empty set st
for x being set st x in b1 holds
ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st
( x = [[F1,F2],t] &amp; F1 is_naturally_transformable_to F2 )
proofend;
end;

:: deftheorem Def15 defines NatTrans-DOMAIN NATTRA_1:def_15_:_
 for A, B being Category
for b3 being non empty set holds
( b3 is NatTrans-DOMAIN of A,B iff for x being set st x in b3 holds
ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st
( x = [[F1,F2],t] &amp; F1 is_naturally_transformable_to F2 ) );

definition
let A, B be Category;
func NatTrans (A,B) ->  NatTrans-DOMAIN of A,B means :Def16: :: NATTRA_1:def 16
 for x being set holds
( x in it iff ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st
( x = [[F1,F2],t] &amp; F1 is_naturally_transformable_to F2 ) );
existence
 ex b1 being NatTrans-DOMAIN of A,B st
for x being set holds
( x in b1 iff ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st
( x = [[F1,F2],t] &amp; F1 is_naturally_transformable_to F2 ) )
proofend;
uniqueness
 for b1, b2 being NatTrans-DOMAIN of A,B st ( for x being set holds
( x in b1 iff ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st
( x = [[F1,F2],t] &amp; F1 is_naturally_transformable_to F2 ) ) ) &amp; ( for x being set holds
( x in b2 iff ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st
( x = [[F1,F2],t] &amp; F1 is_naturally_transformable_to F2 ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def16 defines NatTrans NATTRA_1:def_16_:_
 for A, B being Category
for b3 being NatTrans-DOMAIN of A,B holds
( b3 = NatTrans (A,B) iff for x being set holds
( x in b3 iff ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st
( x = [[F1,F2],t] &amp; F1 is_naturally_transformable_to F2 ) ) );

theorem Th32: :: NATTRA_1:32
for A, B being Category
for F1, F2 being Functor of A,B
for t1 being natural_transformation of F1,F2 holds
( F1 is_naturally_transformable_to F2 iff [[F1,F2],t1] in NatTrans (A,B) )
proofend;

definition
let A, B be Category;
func Functors (A,B) ->  strict Category means :Def17: :: NATTRA_1:def 17
( the carrier of it = Funct (A,B) &amp; the carrier' of it = NatTrans (A,B) &amp; ( for f being Morphism of it holds
( dom f = (f `1) `1 &amp; cod f = (f `1) `2 ) ) &amp; ( for f, g being Morphism of it st dom g = cod f holds
[g,f] in dom the Comp of it ) &amp; ( for f, g being Morphism of it st [g,f] in dom the Comp of it holds
ex F, F1, F2 being Functor of A,B ex t being natural_transformation of F,F1 ex t1 being natural_transformation of F1,F2 st
( f = [[F,F1],t] &amp; g = [[F1,F2],t1] &amp; the Comp of it . [g,f] = [[F,F2],(t1 `*` t)] ) ) &amp; ( for a being Object of it
for F being Functor of A,B st F = a holds
id a = [[F,F],(id F)] ) );
existence
 ex b1 being strict Category st
( the carrier of b1 = Funct (A,B) &amp; the carrier' of b1 = NatTrans (A,B) &amp; ( for f being Morphism of b1 holds
( dom f = (f `1) `1 &amp; cod f = (f `1) `2 ) ) &amp; ( for f, g being Morphism of b1 st dom g = cod f holds
[g,f] in dom the Comp of b1 ) &amp; ( for f, g being Morphism of b1 st [g,f] in dom the Comp of b1 holds
ex F, F1, F2 being Functor of A,B ex t being natural_transformation of F,F1 ex t1 being natural_transformation of F1,F2 st
( f = [[F,F1],t] &amp; g = [[F1,F2],t1] &amp; the Comp of b1 . [g,f] = [[F,F2],(t1 `*` t)] ) ) &amp; ( for a being Object of b1
for F being Functor of A,B st F = a holds
id a = [[F,F],(id F)] ) )
proofend;
uniqueness
 for b1, b2 being strict Category st the carrier of b1 = Funct (A,B) &amp; the carrier' of b1 = NatTrans (A,B) &amp; ( for f being Morphism of b1 holds
( dom f = (f `1) `1 &amp; cod f = (f `1) `2 ) ) &amp; ( for f, g being Morphism of b1 st dom g = cod f holds
[g,f] in dom the Comp of b1 ) &amp; ( for f, g being Morphism of b1 st [g,f] in dom the Comp of b1 holds
ex F, F1, F2 being Functor of A,B ex t being natural_transformation of F,F1 ex t1 being natural_transformation of F1,F2 st
( f = [[F,F1],t] &amp; g = [[F1,F2],t1] &amp; the Comp of b1 . [g,f] = [[F,F2],(t1 `*` t)] ) ) &amp; ( for a being Object of b1
for F being Functor of A,B st F = a holds
id a = [[F,F],(id F)] ) &amp; the carrier of b2 = Funct (A,B) &amp; the carrier' of b2 = NatTrans (A,B) &amp; ( for f being Morphism of b2 holds
( dom f = (f `1) `1 &amp; cod f = (f `1) `2 ) ) &amp; ( for f, g being Morphism of b2 st dom g = cod f holds
[g,f] in dom the Comp of b2 ) &amp; ( for f, g being Morphism of b2 st [g,f] in dom the Comp of b2 holds
ex F, F1, F2 being Functor of A,B ex t being natural_transformation of F,F1 ex t1 being natural_transformation of F1,F2 st
( f = [[F,F1],t] &amp; g = [[F1,F2],t1] &amp; the Comp of b2 . [g,f] = [[F,F2],(t1 `*` t)] ) ) &amp; ( for a being Object of b2
for F being Functor of A,B st F = a holds
id a = [[F,F],(id F)] ) holds
b1 = b2
proofend;
end;

:: deftheorem Def17 defines Functors NATTRA_1:def_17_:_
 for A, B being Category
for b3 being strict Category holds
( b3 = Functors (A,B) iff ( the carrier of b3 = Funct (A,B) &amp; the carrier' of b3 = NatTrans (A,B) &amp; ( for f being Morphism of b3 holds
( dom f = (f `1) `1 &amp; cod f = (f `1) `2 ) ) &amp; ( for f, g being Morphism of b3 st dom g = cod f holds
[g,f] in dom the Comp of b3 ) &amp; ( for f, g being Morphism of b3 st [g,f] in dom the Comp of b3 holds
ex F, F1, F2 being Functor of A,B ex t being natural_transformation of F,F1 ex t1 being natural_transformation of F1,F2 st
( f = [[F,F1],t] &amp; g = [[F1,F2],t1] &amp; the Comp of b3 . [g,f] = [[F,F2],(t1 `*` t)] ) ) &amp; ( for a being Object of b3
for F being Functor of A,B st F = a holds
id a = [[F,F],(id F)] ) ) );

:: As immediate consequences of the definition we get
theorem Th33: :: NATTRA_1:33
for A, B being Category
for F, F1 being Functor of A,B
for t being natural_transformation of F,F1
for f being Morphism of (Functors (A,B)) st f = [[F,F1],t] holds
( dom f = F &amp; cod f = F1 )
proofend;

theorem :: NATTRA_1:34
for A, B being Category
for a, b being Object of (Functors (A,B))
for f being Morphism of a,b st Hom (a,b) <> {} holds
ex F, F1 being Functor of A,B ex t being natural_transformation of F,F1 st
( a = F &amp; b = F1 &amp; f = [[F,F1],t] )
proofend;

theorem Th35: :: NATTRA_1:35
for A, B being Category
for F2, F3, F, F1 being Functor of A,B
for t being natural_transformation of F,F1
for t9 being natural_transformation of F2,F3
for f, g being Morphism of (Functors (A,B)) st f = [[F,F1],t] &amp; g = [[F2,F3],t9] holds
( [g,f] in dom the Comp of (Functors (A,B)) iff F1 = F2 )
proofend;

theorem :: NATTRA_1:36
for A, B being Category
for F, F1, F2 being Functor of A,B
for t being natural_transformation of F,F1
for t1 being natural_transformation of F1,F2
for f, g being Morphism of (Functors (A,B)) st f = [[F,F1],t] &amp; g = [[F1,F2],t1] holds
g (*) f = [[F,F2],(t1 `*` t)]
proofend;

begin

definition
let C be Category;
attrC is discrete  means :Def18: :: NATTRA_1:def 18
 for f being Morphism of C ex a being Object of C st f = id a;
end;

:: deftheorem Def18 defines discrete NATTRA_1:def_18_:_
 for C being Category holds
( C is discrete iff for f being Morphism of C ex a being Object of C st f = id a );

registration
cluster non empty non void V55() Category-like transitive associative reflexive with_identities discrete for CatStr ;
existence
 ex b1 being Category st b1 is discrete
proofend;
end;

theorem Th37: :: NATTRA_1:37
for A being discrete Category
for a being Object of A holds Hom (a,a) = {(id a)}
proofend;

theorem Th38: :: NATTRA_1:38
for A being Category holds
( A is discrete iff ( ( for a being Object of A ex B being finite set st
( B = Hom (a,a) &amp; card B = 1 ) ) &amp; ( for a, b being Object of A st a <> b holds
Hom (a,b) = {} ) ) )
proofend;

theorem Th39: :: NATTRA_1:39
for o, m being set holds 1Cat (o,m) is discrete
proofend;

theorem :: NATTRA_1:40
for A being discrete Category
for C being Subcategory of A holds C is discrete
proofend;

theorem :: NATTRA_1:41
for A, B being Category st A is discrete &amp; B is discrete holds
[:A,B:] is discrete
proofend;

theorem Th42: :: NATTRA_1:42
for A being discrete Category
for B being Category
for F1, F2 being Functor of B,A st F1 is_transformable_to F2 holds
F1 = F2
proofend;

theorem Th43: :: NATTRA_1:43
for A being discrete Category
for B being Category
for F being Functor of B,A
for t being transformation of F,F holds t = id F
proofend;

theorem :: NATTRA_1:44
for A, B being Category st A is discrete holds
Functors (B,A) is discrete
proofend;

registration
let C be Category;
cluster non empty non void V55() strict Category-like transitive associative reflexive with_identities discrete for Subcategory of C;
existence
 ex b1 being Subcategory of C st
( b1 is strict &amp; b1 is discrete )
proofend;
end;

definition
let C be Category;
func IdCat C ->  strict discrete Subcategory of C means :Def19: :: NATTRA_1:def 19
( the carrier of it = the carrier of C &amp; the carrier' of it =  {  (id a) where a is Object of C : verum  }  );
existence
 ex b1 being strict discrete Subcategory of C st
( the carrier of b1 = the carrier of C &amp; the carrier' of b1 =  {  (id a) where a is Object of C : verum  }  )
proofend;
uniqueness
 for b1, b2 being strict discrete Subcategory of C st the carrier of b1 = the carrier of C &amp; the carrier' of b1 =  {  (id a) where a is Object of C : verum  }  &amp; the carrier of b2 = the carrier of C &amp; the carrier' of b2 =  {  (id a) where a is Object of C : verum  }  holds
b1 = b2
proofend;
end;

:: deftheorem Def19 defines IdCat NATTRA_1:def_19_:_
 for C being Category
for b2 being strict discrete Subcategory of C holds
( b2 = IdCat C iff ( the carrier of b2 = the carrier of C &amp; the carrier' of b2 =  {  (id a) where a is Object of C : verum  }  ) );

theorem Th45: :: NATTRA_1:45
for C being strict Category st C is discrete holds
IdCat C = C
proofend;

theorem :: NATTRA_1:46
for C being Category holds IdCat (IdCat C) = IdCat C by Th45;

theorem :: NATTRA_1:47
for o, m being set holds IdCat (1Cat (o,m)) = 1Cat (o,m)
proofend;

theorem :: NATTRA_1:48
for A, B being Category holds IdCat [:A,B:] = [:(IdCat A),(IdCat B):]
proofend;