let A be Category; 1Cat (A,[[A,A],(id A)]) is Categorial
set F = [[A,A],(id A)];
set C = 1Cat (A,[[A,A],(id A)]);
thus
for x being Object of (1Cat (A,[[A,A],(id A)])) holds x is Category
by TARSKI:def 1; CAT_5:def 5,CAT_5:def 6 ( ( for a being Object of (1Cat (A,[[A,A],(id A)]))
for A being Category st a = A holds
id a = [[A,A],(id A)] ) & ( for m being Morphism of (1Cat (A,[[A,A],(id A)]))
for A, B being Category st A = dom m & B = cod m holds
ex F being Functor of A,B st m = [[A,B],F] ) & ( for m1, m2 being Morphism of (1Cat (A,[[A,A],(id A)]))
for A, B, C being Category
for F being Functor of A,B
for G being Functor of B,C st m1 = [[A,B],F] & m2 = [[B,C],G] holds
m2 (*) m1 = [[A,C],(G * F)] ) )
hereby ( ( for m being Morphism of (1Cat (A,[[A,A],(id A)]))
for A, B being Category st A = dom m & B = cod m holds
ex F being Functor of A,B st m = [[A,B],F] ) & ( for m1, m2 being Morphism of (1Cat (A,[[A,A],(id A)]))
for A, B, C being Category
for F being Functor of A,B
for G being Functor of B,C st m1 = [[A,B],F] & m2 = [[B,C],G] holds
m2 (*) m1 = [[A,C],(G * F)] ) )
let a be
Object of
(1Cat (A,[[A,A],(id A)]));
for D being Category st a = D holds
id a = [[D,D],(id D)]let D be
Category;
( a = D implies id a = [[D,D],(id D)] )assume
a = D
;
id a = [[D,D],(id D)]then
D = A
by TARSKI:def 1;
hence
id a = [[D,D],(id D)]
by TARSKI:def 1;
verum
end;
hereby for m1, m2 being Morphism of (1Cat (A,[[A,A],(id A)]))
for A, B, C being Category
for F being Functor of A,B
for G being Functor of B,C st m1 = [[A,B],F] & m2 = [[B,C],G] holds
m2 (*) m1 = [[A,C],(G * F)]
let m be
Morphism of
(1Cat (A,[[A,A],(id A)]));
for C1, C2 being Category st C1 = dom m & C2 = cod m holds
ex G being Functor of C1,C2 st m = [[C1,C2],G]let C1,
C2 be
Category;
( C1 = dom m & C2 = cod m implies ex G being Functor of C1,C2 st m = [[C1,C2],G] )assume that A1:
C1 = dom m
and A2:
C2 = cod m
;
ex G being Functor of C1,C2 st m = [[C1,C2],G]A3:
C1 = A
by A1, TARSKI:def 1;
A4:
C2 = A
by A2, TARSKI:def 1;
reconsider G =
id A as
Functor of
C1,
C2 by A2, A3, TARSKI:def 1;
take G =
G;
m = [[C1,C2],G]thus
m = [[C1,C2],G]
by A3, A4, TARSKI:def 1;
verum
end;
let m1, m2 be Morphism of (1Cat (A,[[A,A],(id A)])); for A, B, C being Category
for F being Functor of A,B
for G being Functor of B,C st m1 = [[A,B],F] & m2 = [[B,C],G] holds
m2 (*) m1 = [[A,C],(G * F)]
let A1, B, C be Category; for F being Functor of A1,B
for G being Functor of B,C st m1 = [[A1,B],F] & m2 = [[B,C],G] holds
m2 (*) m1 = [[A1,C],(G * F)]
let F1 be Functor of A1,B; for G being Functor of B,C st m1 = [[A1,B],F1] & m2 = [[B,C],G] holds
m2 (*) m1 = [[A1,C],(G * F1)]
let F2 be Functor of B,C; ( m1 = [[A1,B],F1] & m2 = [[B,C],F2] implies m2 (*) m1 = [[A1,C],(F2 * F1)] )
assume that
A5:
m1 = [[A1,B],F1]
and
A6:
m2 = [[B,C],F2]
; m2 (*) m1 = [[A1,C],(F2 * F1)]
A7:
[[A1,B],F1] = [[A,A],(id A)]
by A5, TARSKI:def 1;
A8:
[[B,C],F2] = [[A,A],(id A)]
by A6, TARSKI:def 1;
A9:
[A1,B] = [A,A]
by A7, XTUPLE_0:1;
A10:
[A,A] = [B,C]
by A8, XTUPLE_0:1;
A11:
F1 = id A
by A7, XTUPLE_0:1;
A12:
F2 = id A
by A8, XTUPLE_0:1;
A13:
A1 = A
by A9, XTUPLE_0:1;
A14:
C = A
by A10, XTUPLE_0:1;
F2 * F1 = id A
by A11, A12, FUNCT_2:17;
hence
m2 (*) m1 = [[A1,C],(F2 * F1)]
by A13, A14, TARSKI:def 1; verum