:: Exponential Objects
::  by Marco Riccardi
:: 
:: Received August 15, 2015
:: Copyright (c) 2015-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies FUNCT_1, TARSKI, ZFMISC_1, XBOOLE_0, RELAT_1, SUBSET_1, WELLORD1,
      CAT_1, CAT_4, ALTCAT_1, GRAPH_1, BINOP_1, STRUCT_0, PARTFUN1, MONOID_0,
      NATTRA_1, MSSUBFAM, CARD_1, FUNCTOR0, MOD_4, CAT_6, XTUPLE_0, RECDEF_2,
      MCART_1, PBOOLE, WELLORD2, FACIRC_1, FUNCT_2, NEWTON, POLYNOM2, CAT_7,
      CAT_8, PZFMISC1, FUNCOP_1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2,
      ORDINAL1, PARTFUN1, FINSEQ_1, STRUCT_0, FUNCOP_1, RELSET_1, BINOP_1,
      GRAPH_1, CAT_1, CAT_2, CAT_3, NUMBERS, NAT_1, XTUPLE_0, ALG_1, WELLORD2,
      CARD_1, CAT_6, ENUMSET1, WELLORD1, CAT_7, NATTRA_1, ISOCAT_1;
 constructors NUMBERS, FUNCT_2, CLASSES2, FINSEQ_1, FUNCOP_1, RELAT_2,
      PARTFUN1, RELSET_1, BINOP_1, FUNCT_4, CAT_1, CAT_2, CAT_3, NAT_1,
      XXREAL_0, WELLORD2, XREAL_0, CARD_1, VALUED_0, ISOCAT_1, STRUCT_0, CAT_6,
      REALSET1, WELLORD1, ORDERS_2, CAT_7, NATTRA_1;
 registrations XBOOLE_0, FUNCT_1, ORDINAL1, XTUPLE_0, CARD_1, STRUCT_0,
      RELSET_1, FUNCT_2, PARTFUN1, CAT_1, NAT_1, CAT_6, CAT_7;
 requirements SUBSET, BOOLE, NUMERALS;


begin :: Preliminaries

theorem :: CAT_8:1
  for C being composable associative CategoryStr,
      f1,f2,f3 being morphism of C st f1 |> f2 & f2 |> f3 holds
   f1(*)f2(*)f3 = f1(*)(f2(*)f3);

theorem :: CAT_8:2
  for C being composable associative CategoryStr,
      f1,f2,f3,f4 being morphism of C st f1 |> f2 & f2 |> f3 & f3 |> f4 holds
  f1(*)f2(*)f3(*)f4 = (f1(*)f2)(*)(f3(*)f4) &
  f1(*)f2(*)f3(*)f4 = f1(*)(f2(*)f3)(*)f4 &
  f1(*)f2(*)f3(*)f4 = f1(*)(f2(*)f3(*)f4) &
  f1(*)f2(*)f3(*)f4 = f1(*)(f2(*)(f3(*)f4));

theorem :: CAT_8:3
  for C being composable CategoryStr,
      f,f1,f2 being morphism of C st f1 |> f2
  holds
  (f1(*)f2 |> f iff f2 |> f) &
  (f |> f1(*)f2 iff f |> f1);

theorem :: CAT_8:4
  for C being composable with_identities CategoryStr,
      f1,f2 being morphism of C st f1 |> f2
  holds
  (f1 is identity implies f1(*)f2 = f2) &
  (f2 is identity implies f1(*)f2 = f1);

theorem :: CAT_8:5
  for C being non empty with_identities CategoryStr, f being morphism of C
  ex f1,f2 being morphism of C st f1 is identity & f2 is identity &
  f1 |> f & f |> f2;

theorem :: CAT_8:6
  for C being CategoryStr, a,b being Object of C
  for f being Morphism of a,b st Hom(a,b) = {f} for g being
  Morphism of a,b holds f = g;

theorem :: CAT_8:7
  for C being CategoryStr, a,b being Object of C
  for f being Morphism of a,b st Hom(a,b) <> {} & for g being
  Morphism of a,b holds f = g holds Hom(a,b) = {f};

theorem :: CAT_8:8
  for x being object, C being CategoryStr st
  the carrier of C = {x} & the composition of C = {[[x,x],x]}
  holds C is non empty category;

theorem :: CAT_8:9
  for C1,C2 being category, F being Functor of C1,C2 st
  F is isomorphism holds F is bijective;

theorem :: CAT_8:10
  for C1,C2,C3 being composable with_identities CategoryStr
  st C1 ~= C2 & C2 ~= C3 holds C1 ~= C3;

theorem :: CAT_8:11
  for C1,C2 being category st C1 ~= C2 holds C1 is empty iff C2 is empty;

registration
  let C1 be empty with_identities CategoryStr;
  let C2 be with_identities CategoryStr;
  cluster -> covariant for Functor of C1,C2;
end;

theorem :: CAT_8:12
  for C1,C2 being with_identities CategoryStr,
      f being morphism of C1, F being Functor of C1,C2
  st F is covariant & f is identity holds F.f is identity;

theorem :: CAT_8:13
  for C1,C2 being with_identities CategoryStr,
      f1,f2 being morphism of C1, F being Functor of C1,C2
  st F is covariant & f1 |> f2
  holds F.f1 |> F.f2 & F.(f1(*)f2) = (F.f1) (*) (F.f2);

theorem :: CAT_8:14
  for C being Category, f being (Morphism of C), g being morphism of alter C
  st f = g holds dom g = id dom f & cod g = id cod f;

theorem :: CAT_8:15
  ex f being morphism of OrdC 1 st f is identity &
  Ob OrdC 1 = {f} & Mor OrdC 1 = {f};

theorem :: CAT_8:16
  for C being non empty category, f1,f2 being morphism of C st
  MORPHISM(f1) = MORPHISM(f2) holds f1 = f2;

theorem :: CAT_8:17
  for C being non empty category, F1,F2 being covariant Functor of OrdC 2, C,
  f being morphism of OrdC 2 st f is non identity & F1.f = F2.f
  holds F1 = F2;

theorem :: CAT_8:18
  ex f1,f2 being morphism of (OrdC 3) st
  f1 is not identity & f2 is not identity & cod f1 = dom f2 &
  Ob (OrdC 3) = {dom f1, cod f1, cod f2} &
  Mor (OrdC 3) = {dom f1, cod f1, cod f2, f1, f2, f2(*)f1} &
  dom f1, cod f1, cod f2, f1, f2, f2(*)f1 are_mutually_distinct;

definition
  let C be non empty category;
  let f1,f2 be morphism of C such that
 f1 |> f2;
  func COMPOSITION(f1,f2) -> covariant Functor of (OrdC 3), C means
:: CAT_8:def 1
  for g1,g2 being morphism of OrdC 3 st g1 |> g2 & g1 is not identity &
  g2 is not identity holds it.g1 = f1 & it.g2 = f2;
end;

begin :: Terminal Objects

definition
  let C be CategoryStr;
  let a be Object of C;
  attr a is terminal means
:: CAT_8:def 2
  for b being Object of C holds
  Hom(b,a)<>{} & ex f being Morphism of b,a
  st for g being Morphism of b,a holds f = g;
end;

theorem :: CAT_8:19
  for C being CategoryStr, b being Object of C holds
  b is terminal iff for a being Object of C
  ex f being Morphism of a,b st Hom(a,b) = {f};

theorem :: CAT_8:20
  for C being with_identities non empty CategoryStr, a being Object of C holds
  a is terminal implies for h being Morphism of a,a holds id- a = h;

theorem :: CAT_8:21
  for C being composable with_identities non empty CategoryStr,
      a,b being Object of C
  holds a is terminal & b is terminal implies a,b are_isomorphic;

theorem :: CAT_8:22
  for C being non empty category, a,b being Object of C
  holds b is terminal & a,b are_isomorphic implies a is terminal;

theorem :: CAT_8:23
  for C being composable with_identities CategoryStr,
      a,b being Object of C, f being Morphism of a,b
  holds Hom(a,b) <> {} & a is terminal implies f is monomorphism;

definition
  let C be category;
  attr C is with_terminal_objects means
:: CAT_8:def 3
  ex a being Object of C st a is terminal;
end;

theorem :: CAT_8:24
  OrdC 1 is with_terminal_objects;

registration
  cluster with_terminal_objects for category;
end;

definition
  let C be category;
  attr C is terminal means
:: CAT_8:def 4
  for B being category holds ex F being Functor of B,C st F is covariant &
  for G being Functor of B,C st G is covariant holds F = G;
end;

registration
  cluster OrdC 1 -> non empty terminal;
end;

registration
  cluster strict non empty terminal for category;
  cluster strict non terminal for category;
end;

theorem :: CAT_8:25
  for C,D being terminal category holds C ~= D;

theorem :: CAT_8:26
  for C,D being category st C is terminal & C ~= D holds D is terminal;

theorem :: CAT_8:27
  for C being category holds C is non empty trivial iff C ~= OrdC 1;

theorem :: CAT_8:28
  for C,D being non empty category st C is trivial & D is trivial holds C ~= D;

registration
  cluster non empty trivial -> terminal for category;
  cluster terminal -> non empty trivial for category;
end;

definition
  let C be category;
  func C ->OrdC1 -> covariant Functor of C, OrdC 1 means
:: CAT_8:def 5
  not contradiction;
end;

theorem :: CAT_8:29
  for C,C1,C2 being category, F1 being Functor of C,C1,
  F2 being Functor of C,C2 st F1 is covariant & F2 is covariant
  holds (C1 ->OrdC1)(*)F1 = (C2 ->OrdC1)(*)F2;

begin :: Initial Objects

definition
  let C be CategoryStr;
  let a be Object of C;
  attr a is initial means
:: CAT_8:def 6
  for b being Object of C holds
  Hom(a,b)<>{} & ex f being Morphism of a,b
  st for g being Morphism of a,b holds f = g;
end;

theorem :: CAT_8:30
  for C being CategoryStr, b being Object of C holds
  b is initial iff for a being Object of C
  ex f being Morphism of b,a st Hom(b,a) = {f};

theorem :: CAT_8:31
  for C being with_identities non empty CategoryStr, a being Object of C holds
  a is initial implies for h being Morphism of a,a holds id- a = h;

theorem :: CAT_8:32
  for C being composable with_identities non empty CategoryStr,
      a,b being Object of C
  holds a is initial & b is initial implies a,b are_isomorphic;

theorem :: CAT_8:33
  for C being non empty category, a,b being Object of C
  holds b is initial & b,a are_isomorphic implies a is initial;

theorem :: CAT_8:34
  for C being composable with_identities CategoryStr,
      a,b being Object of C, f being Morphism of a,b
  holds Hom(a,b) <> {} & b is initial implies f is epimorphism;

definition
  let C be category;
  attr C is with_initial_objects means
:: CAT_8:def 7
  ex a being Object of C st a is initial;
end;

theorem :: CAT_8:35
  OrdC 1 is with_initial_objects;

registration
  cluster with_initial_objects for category;
end;

definition
  let C be category;
  attr C is initial means
:: CAT_8:def 8
  for C1 being category ex F being Functor of C,C1 st F is covariant &
  for F1 being Functor of C,C1 st F1 is covariant holds F = F1;
end;

registration
  cluster OrdC 0 -> empty initial;
end;

registration
  cluster strict empty initial for category;
  cluster strict non initial for category;
end;

theorem :: CAT_8:36
  for C,D being initial category holds C ~= D;

theorem :: CAT_8:37
  for C,D being category st C is initial & C ~= D holds D is initial;

registration
  cluster empty -> initial for category;
end;

definition
  let C be category;
  func OrdC0-> C -> covariant Functor of OrdC 0, C means
:: CAT_8:def 9
  not contradiction;
end;

theorem :: CAT_8:38
  for C,C1,C2 being category, F1 being Functor of C1,C,
  F2 being Functor of C2,C st F1 is covariant & F2 is covariant
  holds F1(*)(OrdC0-> C1) = F2(*)(OrdC0-> C2);


begin :: Categorical Products

definition
  let C be category;
  let a,b,c be Object of C;
  let p1 be Morphism of c,a such that Hom(c,a) <> {};
  let p2 be Morphism of c,b such that Hom(c,b) <> {};
  pred c,p1,p2 is_product_of a,b means
:: CAT_8:def 10
  for c1 being Object of C,
      q1 being Morphism of c1,a, q2 being Morphism of c1,b
  st Hom(c1,a) <> {} & Hom(c1,b) <> {}
  holds Hom(c1,c) <> {} & ex h being Morphism of c1,c st
   p1 * h = q1 & p2 * h = q2
   & for h1 being Morphism of c1,c st p1 * h1 = q1 & p2 * h1 = q2 holds h = h1;
end;

theorem :: CAT_8:39
  for C being non empty category, c1,c2,a,b being Object of C,
      p1 being Morphism of a,c1, p2 being Morphism of a,c2,
      q1 being Morphism of b,c1, q2 being Morphism of b,c2
  st Hom(a,c1) <> {} & Hom(a,c2) <> {} & Hom(b,c1) <> {} & Hom(b,c2) <> {} &
     a,p1,p2 is_product_of c1,c2 & b,q1,q2 is_product_of c1,c2
  holds a,b are_isomorphic;

theorem :: CAT_8:40
  for C being category, c1,c2,d being Object of C,
      p1 being Morphism of d,c1, p2 being Morphism of d,c2
  st Hom(d,c1) <> {} & Hom(d,c2) <> {} &
     d,p1,p2 is_product_of c1,c2 holds d,p2,p1 is_product_of c2,c1;

definition
  let C be category;
  attr C is with_binary_products means
:: CAT_8:def 11
  for a,b being Object of C holds ex d being Object of C,
  p1 being Morphism of d,a, p2 being Morphism of d,b st
  Hom(d,a) <> {} & Hom(d,b) <> {} & d,p1,p2 is_product_of a,b;
end;

theorem :: CAT_8:41
  OrdC 1 is with_binary_products;

registration
  cluster with_binary_products non empty for category;
end;

definition
  let C be with_binary_products category;
  let c1,c2 be Object of C;
  mode categorical_product of c1,c2 -> triple object means
:: CAT_8:def 12
  ex d being Object of C, p1 being Morphism of d,c1, p2 being Morphism of d,c2
  st it = [d,p1,p2] & Hom(d,c1) <> {} & Hom(d,c2) <> {} &
  d,p1,p2 is_product_of c1,c2;
end;

definition
  let C be with_binary_products category;
  let c1,c2 be Object of C;
  func c1 [x] c2 -> Object of C equals
:: CAT_8:def 13
  (the categorical_product of c1,c2)`1_3;
end;

definition
  let C be with_binary_products category;
  let c1,c2 be Object of C;
  func pr1(c1,c2) -> Morphism of c1 [x] c2,c1 equals
:: CAT_8:def 14
  (the categorical_product of c1,c2)`2_3;
  func pr2(c1,c2) -> Morphism of c1 [x] c2,c2 equals
:: CAT_8:def 15
  (the categorical_product of c1,c2)`3_3;
end;

theorem :: CAT_8:42
  for C being with_binary_products category, a,b being Object of C holds
  a [x] b, pr1(a,b), pr2(a,b) is_product_of a,b &
  Hom(a [x] b,a) <> {} & Hom(a [x] b,b) <> {};

theorem :: CAT_8:43
  for C being with_binary_products category, a,b,c being Object of C
  st Hom(c,a) <> {} & Hom(c,b) <> {} holds Hom(c,a [x] b)<> {};

theorem :: CAT_8:44
  for C being with_binary_products category, a,b,c,d being Object of C
  st Hom(a,b) <> {} & Hom(c,d) <> {} holds Hom(a [x] c,b [x] d)<> {};

definition
  let C be with_binary_products category;
  let a,b,c,d be Object of C;
  let f be Morphism of a,b such that
 Hom(a,b) <> {};
  let g be Morphism of c,d such that
 Hom(c,d) <> {};
  func f [x] g -> Morphism of a [x] c,b [x] d means
:: CAT_8:def 16
  f * pr1(a,c) = pr1(b,d) * it & g * pr2(a,c) = pr2(b,d) * it;
end;

definition
  let C1,C2,D be category;
  let P1 be Functor of D,C1 such that P1 is covariant;
  let P2 be Functor of D,C2 such that P2 is covariant;
  pred D,P1,P2 is_product_of C1,C2 means
:: CAT_8:def 17
  for D1 being category, G1 being Functor of D1,C1, G2 being Functor of D1,C2
  st G1 is covariant & G2 is covariant holds
  ex H being Functor of D1,D st H is covariant & P1 (*) H = G1 & P2 (*) H = G2
  & for H1 being Functor of D1,D
  st H1 is covariant & P1 (*) H1 = G1 & P2 (*) H1 = G2 holds H = H1;
end;

theorem :: CAT_8:45
  for C1,C2,A,B being category, P1 be Functor of A,C1, P2 be Functor of A,C2,
      Q1 be Functor of B,C1, Q2 be Functor of B,C2
  st P1 is covariant & P2 is covariant & Q1 is covariant & Q2 is covariant &
      A,P1,P2 is_product_of C1,C2 & B,Q1,Q2 is_product_of C1,C2
  holds A ~= B;

theorem :: CAT_8:46
  for C1,C2,D being category, P1 being Functor of D,C1,
      P2 being Functor of D,C2
  st P1 is covariant & P2 is covariant &
  D,P1,P2 is_product_of C1,C2 holds D,P2,P1 is_product_of C2,C1;

notation
  let C,C1,C2 be category;
  let F1 be Functor of C1,C;
  let F2 be Functor of C2,C;
  synonym F1 [|x|] F2 for [| F1, F2 |];
end;

theorem :: CAT_8:47
  for C1,C2 being category holds (C1 ->OrdC1)[|x|](C2 ->OrdC1),
  pr1(C1 ->OrdC1,C2 ->OrdC1),pr2(C1 ->OrdC1,C2 ->OrdC1) is_product_of C1,C2;

definition
  let C1,C2 be category;
  mode categorical_product of C1,C2 -> triple object means
:: CAT_8:def 18
  ex D being strict category, P1 being Functor of D,C1,
  P2 being Functor of D,C2 st it = [D,P1,P2] &
  P1 is covariant & P2 is covariant & D,P1,P2 is_product_of C1,C2;
end;

definition
  let C1,C2 be category;
  func C1 [x] C2 -> strict category equals
:: CAT_8:def 19
  (the categorical_product of C1,C2)`1_3;
end;

definition
  let C1,C2 be category;
  func pr1(C1,C2) -> Functor of C1 [x] C2, C1 equals
:: CAT_8:def 20
  (the categorical_product of C1,C2)`2_3;
  func pr2(C1,C2) -> Functor of C1 [x] C2, C2 equals
:: CAT_8:def 21
  (the categorical_product of C1,C2)`3_3;
end;

theorem :: CAT_8:48
  for C1,C2 being category holds
  C1 [x] C2,pr1(C1,C2),pr2(C1,C2) is_product_of C1,C2;

registration
  let C1,C2 be category;
  cluster pr1(C1,C2) -> covariant;
  cluster pr2(C1,C2) -> covariant;
end;

theorem :: CAT_8:49
  for C1,C2 being category holds
  C1 [x] C2 is non empty iff (C1 is non empty & C2 is non empty);

registration
  let C1 be empty category;
  let C2 be category;
  cluster C1 [x] C2 -> empty;
end;

registration
  let C1 be category;
  let C2 be empty category;
  cluster C1 [x] C2 -> empty;
end;

registration
  let C1 be non empty category;
  let C2 be non empty category;
  cluster C1 [x] C2 -> non empty;
end;

definition
  let C1,C2,D1,D2 be category;
  let F1 be Functor of C1,D1;
  let F2 be Functor of C2,D2;
  assume
 F1 is covariant & F2 is covariant;
  func F1 [x] F2 -> Functor of C1 [x] C2,D1 [x] D2 means
:: CAT_8:def 22
  it is covariant &
  F1(*)pr1(C1,C2) = pr1(D1,D2)(*)it & F2(*)pr2(C1,C2) = pr2(D1,D2)(*)it;
end;

theorem :: CAT_8:50
  for A1,A2,B1,B2,C1,C2 being category, F1 being Functor of A1,B1,
      F2 being Functor of A2,B2, G1 being Functor of B1,C1,
      G2 being Functor of B2,C2
  st F1 is covariant & G1 is covariant & F2 is covariant & G2 is covariant
  holds (G1 [x] G2)(*)(F1 [x] F2) = G1(*)F1 [x] G2(*)F2;

theorem :: CAT_8:51
  for C1,C2 being category holds id C1 [x] id C2 = id(C1 [x] C2);

notation
  let x,y be object;
  synonym KuratowskiPair(x,y) for [x,y];
end;

definition
  let C1,C2 be category;
  let f1 be morphism of C1;
  let f2 be morphism of C2;
  func [f1,f2] -> morphism of C1 [x] C2 means
:: CAT_8:def 23
  pr1(C1,C2).it = f1 & pr2(C1,C2).it = f2 if C1 is not empty & C2 is not empty
  otherwise it = the morphism of C1 [x] C2;
end;

theorem :: CAT_8:52
  for C1,C2 be category, f being morphism of C1 [x] C2
  ex f1 being morphism of C1, f2 being morphism of C2 st f = [f1,f2];

theorem :: CAT_8:53
  for C1,C2 being non empty category, f1,g1 being morphism of C1,
      f2,g2 being morphism of C2
  st [f1,f2] = [g1,g2] holds f1 = g1 & f2 = g2;

theorem :: CAT_8:54
  for C1,C2 being category, f1,g1 being morphism of C1,
      f2,g2 being morphism of C2
  holds [f1,f2] |> [g1,g2] iff f1 |> g1 & f2 |> g2;

theorem :: CAT_8:55
  for C1,C2 being category, f1,g1 being morphism of C1,
      f2,g2 being morphism of C2 st f1 |> g1 & f2 |> g2 holds
  [f1,f2](*)[g1,g2] = [f1(*)g1,f2(*)g2];

theorem :: CAT_8:56
  for C1,C2 be category, f1 being morphism of C1, f2 being morphism of C2,
  f being morphism of C1 [x] C2
  st f = [f1,f2] & C1 is non empty & C2 is non empty
  holds f is identity iff f1 is identity & f2 is identity;

theorem :: CAT_8:57
  for C1,C2 being non empty category, D1,D2 being category,
      F1 being Functor of C1,D1, F2 being Functor of C2,D2,
      c1 being morphism of C1, c2 being morphism of C2
  st F1 is covariant & F2 is covariant holds (F1[x]F2).[c1,c2] = [F1.c1,F2.c2];

begin :: Natural Transformations

definition
  let C1,C2 be category;
  let F1,F2 be Functor of C1,C2;
  let T be Functor of C1,C2;
  pred T is_natural_transformation_of F1,F2 means
:: CAT_8:def 24
  for f1,f2 being morphism of C1 st f1 |> f2
  holds T.f1 |> F1.f2 & F2.f1 |> T.f2 &
  T.(f1(*)f2) = (T.f1)(*)(F1.f2) & T.(f1(*)f2) = (F2.f1)(*)(T.f2);
end;

theorem :: CAT_8:58
  for C1,C2 being category, F1,F2 being Functor of C1,C2,
      T being Functor of C1,C2 st F1 is covariant & F2 is covariant holds
  T is_natural_transformation_of F1,F2 iff
  for f,f1,f2 being morphism of C1 st f1 is identity & f2 is identity &
    f1 |> f & f |> f2 holds T.f1 |> F1.f & F2.f |> T.f2 &
    T.f = (T.f1)(*)(F1.f) & T.f = (F2.f)(*)(T.f2);

theorem :: CAT_8:59
  for C1,C2 being non empty category, F1,F2 being covariant Functor of C1,C2,
      T being Function of Ob(C1), Mor(C2) holds
  (ex T1 being Functor of C1,C2
   st T = T1|Ob(C1) & T1 is_natural_transformation_of F1,F2) iff
  (for a being Object of C1 holds T.a in Hom(F1.a,F2.a)) &
  (for a1,a2 being Object of C1,f being Morphism of a1,a2 st Hom(a1,a2) <> {}
   holds (T.a2)(*)(F1.f) = (F2.f)(*)(T.a1));

theorem :: CAT_8:60
  for C,D being Category, F1,F2 being Functor of C,D,
  G1,G2,T being Functor of alter(C),alter(D) st F1 = G1 & F2 = G2 &
  T is_natural_transformation_of G1,G2
  holds (IdMap C)*T is natural_transformation of F1,F2;

definition
  let C,D be category;
  let F1,F2 be Functor of C,D;
  pred F1 is_naturally_transformable_to F2 means
:: CAT_8:def 25
  ex T being Functor of C,D st T is_natural_transformation_of F1,F2;
end;

definition
  let C,D be category;
  let F1,F2 be Functor of C,D;
  assume
 F1 is_naturally_transformable_to F2;
  mode natural_transformation of F1,F2 -> Functor of C,D means
:: CAT_8:def 26
  it is_natural_transformation_of F1,F2;
end;

theorem :: CAT_8:61
  for C,D being category, F being Functor of C,D
  st F is covariant holds F is_natural_transformation_of F,F;

definition
  let C,D be category;
  let F,F1,F2 be Functor of C,D;
  assume that
 F1 is_naturally_transformable_to F &
    F is_naturally_transformable_to F2 and
 F is covariant & F1 is covariant & F2 is covariant;
  let T1 be natural_transformation of F1,F;
  let T2 be natural_transformation of F,F2;
  func T2`*`T1 -> natural_transformation of F1,F2 means
:: CAT_8:def 27
  for f,f1,f2 being morphism of C st f1 is identity & f2 is identity &
  f |> f1 & f2 |> f holds it.f = (T2.f2)(*)(F.f)(*)(T1.f1);
end;

theorem :: CAT_8:62
  for C,D being category, F,F1,F2 being Functor of C,D
  st F1 is_naturally_transformable_to F & F is_naturally_transformable_to F2 &
  F is covariant & F1 is covariant & F2 is covariant
  holds F1 is_naturally_transformable_to F2;

definition
  let C1,C2 be category;
  func Functors(C1,C2) -> strict category means
:: CAT_8:def 28
  the carrier of it = {[[F1,F2],T] where F1,F2 is Functor of C1,C2,
      T is natural_transformation of F1,F2: F1 is covariant & F2 is covariant
      & F1 is_naturally_transformable_to F2} &
  the composition of it = {[[x2,x1],x3] where x1,x2,x3 is
         Element of the carrier of it: ex F1,F2,F3 being Functor of C1,C2,
      T1 being natural_transformation of F1,F2,
      T2 being natural_transformation of F2,F3 st x1 = [[F1,F2],T1] &
      x2 = [[F2,F3],T2] & x3 = [[F1,F3],T2`*`T1]};
end;

registration
  let C1 be non empty category;
  let C2 be empty category;
  cluster Functors(C1,C2) -> empty;
end;

registration
  let C1 be empty category;
  let C2 be category;
  cluster Functors(C1,C2) -> non empty trivial;
end;

registration
  let C1 be non empty category;
  let C2 be non empty category;
  cluster Functors(C1,C2) -> non empty;
end;

theorem :: CAT_8:63
  for C1,C2 being non empty category, f1,f2 being morphism of Functors(C1,C2)
  holds f1 |> f2 iff ex F,F1,F2 being covariant Functor of C1,C2,
  T1 being natural_transformation of F1,F,
  T2 being natural_transformation of F,F2 st
  f1 = [[F,F2],T2] & f2 = [[F1,F],T1] & f1(*)f2 = [[F1,F2],T2`*`T1] &
  for g1,g2 being morphism of C1 st g2 |> g1 holds T2.g2 |> T1.g1 &
  (T2`*`T1).(g2(*)g1) = (T2.g2)(*)(T1.g1);

theorem :: CAT_8:64
  for C1,C2 being non empty category, f being morphism of Functors(C1,C2) holds
  f is identity iff ex F being covariant Functor of C1,C2 st f = [[F,F],F];

theorem :: CAT_8:65
  for C1,C2 being non empty category, f being morphism of Functors(C1,C2) holds
  ex F1,F2 being covariant Functor of C1,C2,
     T being natural_transformation of F1,F2 st f = [[F1,F2],T] &
     dom f = [[F1,F1],F1] & cod f = [[F2,F2],F2];

begin :: Exponential Objects

definition
  let C be with_binary_products non empty category;
  let a,b,c be Object of C;
  let e be Morphism of c [x] a, b such that Hom(c [x] a, b)<>{};
  pred c,e is_exponent_of a,b means
:: CAT_8:def 29
  for d being Object of C, f being Morphism of d [x] a,b st Hom(d [x] a,b)<>{}
  holds Hom(d,c)<>{} & ex h being Morphism of d,c st f = e * (h [x] id- a) &
  for h1 being Morphism of d,c st f = e * (h1 [x] id- a) holds h = h1;
end;

theorem :: CAT_8:66
  for C being with_binary_products category,
      a1,a2,b1,b2,c1,c2 being Object of C, f1 being Morphism of a1,b1,
      f2 being Morphism of a2,b2, g1 being Morphism of b1,c1,
      g2 being Morphism of b2,c2
  st Hom(a1,b1)<>{} & Hom(b1,c1)<>{} & Hom(a2,b2)<>{} & Hom(b2,c2)<>{}
  holds (g1 [x] g2) * (f1 [x] f2) = (g1*f1) [x] (g2*f2);

theorem :: CAT_8:67
  for C being with_binary_products non empty category, a,b being Object of C
  holds id- a [x] id- b = id-(a [x] b);

theorem :: CAT_8:68
  for C being with_binary_products non empty category,
      a,b,c1,c2 being Object of C,
      e1 being Morphism of c1 [x] a, b, e2 being Morphism of c2 [x] a, b
  st Hom(c1 [x] a, b)<>{} & Hom(c2 [x] a, b)<>{} & c1,e1 is_exponent_of a,b &
  c2,e2 is_exponent_of a,b holds c1,c2 are_isomorphic;

definition
  let C be with_binary_products non empty category;
  attr C is with_exponential_objects means
:: CAT_8:def 30
  for a,b being Object of C holds ex c being Object of C,
  e being Morphism of c [x] a,b st Hom(c [x] a, b)<>{} &
  c,e is_exponent_of a,b;
end;

registration
  cluster OrdC 1 -> with_binary_products;
end;

theorem :: CAT_8:69
  OrdC 1 is with_exponential_objects;

registration
  cluster with_exponential_objects for with_binary_products non empty category;
end;

definition
  let C be with_exponential_objects with_binary_products non empty category;
  let a,b be Object of C;
  mode categorical_exponent of a,b -> pair object means
:: CAT_8:def 31
  ex c being Object of C, e being Morphism of c [x] a,b st it = [c,e] &
  Hom(c [x] a, b)<>{} & c,e is_exponent_of a,b;
end;

definition
  let C be with_exponential_objects with_binary_products non empty category;
  let a,b be Object of C;
  func b |^ a -> Object of C equals
:: CAT_8:def 32
  (the categorical_exponent of a,b)`1;
end;

definition
  let C be with_exponential_objects with_binary_products non empty category;
  let a,b be Object of C;
  func eval(a,b) -> Morphism of b|^a [x] a, b equals
:: CAT_8:def 33
  (the categorical_exponent of a,b)`2;
end;

theorem :: CAT_8:70
  for C being with_exponential_objects with_binary_products non empty category,
      a,b being Object of C holds Hom(b|^a [x] a, b)<>{} &
      b|^a,eval(a,b) is_exponent_of a,b;

theorem :: CAT_8:71
  for C being with_exponential_objects with_binary_products non empty category,
      a,b,c being Object of C st Hom(c [x] a,b) <> {}
  holds
  ex L being Function of Hom(c [x] a,b), Hom(c,b|^a) st
  (for f being Morphism of c [x] a,b, h being Morphism of c,b|^a st h = L.f
  holds eval(a,b) * (h [x] id- a) = f) & L is bijective;

definition
  let A,B,C be category;
  let E be Functor of C [x] A, B such that E is covariant;
  pred C,E is_exponent_of A,B means
:: CAT_8:def 34
  for D being category, F being Functor of D [x] A, B st F is covariant holds
  ex H being Functor of D,C st H is covariant & F = E (*)(H [x] id A) &
  for H1 being Functor of D,C st H1 is covariant & F = E (*)(H1 [x] id A)
  holds H = H1;
end;

definition
  let C1,C2 be category;
  mode categorical_exponent of C1,C2 -> pair object means
:: CAT_8:def 35
  ex C being category, E being Functor of C [x] C1,C2 st
  it = [C,E] & E is covariant & C,E is_exponent_of C1,C2;
end;


definition
  let C1,C2 be category;
  func C2 |^ C1 -> category equals
:: CAT_8:def 36
  (the categorical_exponent of C1,C2)`1;
end;

definition
  let C1,C2 be category;
  func eval(C1,C2) -> Functor of C2|^C1 [x] C1, C2 equals
:: CAT_8:def 37
  (the categorical_exponent of C1,C2)`2;
end;

theorem :: CAT_8:72
  for C1,C2 being category holds C2|^C1,eval(C1,C2) is_exponent_of C1,C2;

theorem :: CAT_8:73
  for A,B,C1,C2 being category, E1 being Functor of C1 [x] A,B,
      E2 being Functor of C2 [x] A,B st E1 is covariant & E2 is covariant &
  C1,E1 is_exponent_of A,B & C2,E2 is_exponent_of A,B holds C1 ~= C2;

registration
  let C1,C2 be category;
  cluster eval(C1,C2) -> covariant;
end;

registration
  let C1 be non empty category;
  let C2 be empty category;
  cluster C2|^C1 -> empty;
end;

registration
  let C1 be empty category;
  let C2 be category;
  cluster C2|^C1 -> non empty trivial;
end;

registration
  let C1 be non empty category;
  let C2 be non empty category;
  cluster C2|^C1 -> non empty;
end;

theorem :: CAT_8:74
  for C1,C2 being category holds Functors(C1,C2) ~= C2|^C1;