:: Category of Functors between Alternative Categories :: by Robert Nieszczerzewski :: :: Received June 12, 1997 :: Copyright (c) 1997-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 RELAT_2, ALTCAT_1, XBOOLE_0, MSUALG_6, FUNCTOR0, CAT_1, FUNCT_1, PZFMISC1, NATTRA_1, PBOOLE, STRUCT_0, SUBSET_1, REALSET1, RELAT_1, FUNCT_2, CARD_3, CAT_2, ZFMISC_1, TARSKI, FUNCTOR2; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCTOR0, XTUPLE_0, MCART_1, DOMAIN_1, RELAT_1, STRUCT_0, CARD_3, FUNCT_1, PBOOLE, FUNCT_2, BINOP_1, MULTOP_1, ALTCAT_1; constructors DOMAIN_1, CARD_3, FUNCTOR0, RELSET_1, XTUPLE_0; registrations XBOOLE_0, SUBSET_1, RELSET_1, STRUCT_0, ALTCAT_1, FUNCTOR0, PBOOLE, FUNCT_1, RELAT_1; requirements SUBSET, BOOLE; begin registration let A be transitive with_units non empty AltCatStr, B be with_units non empty AltCatStr; cluster -> feasible id-preserving for Functor of A, B; end; registration let A be transitive with_units non empty AltCatStr, B be with_units non empty AltCatStr; cluster covariant -> Covariant comp-preserving for Functor of A, B; cluster Covariant comp-preserving -> covariant for Functor of A, B; cluster contravariant -> Contravariant comp-reversing for Functor of A, B; cluster Contravariant comp-reversing -> contravariant for Functor of A, B; end; theorem :: FUNCTOR2:1 for A,B being transitive with_units non empty AltCatStr, F being covariant Functor of A,B for a being Object of A holds F.idm a = idm (F.a ); begin :: Transformations definition let A,B be transitive with_units non empty AltCatStr, F1,F2 be Functor of A,B; pred F1 is_transformable_to F2 means :: FUNCTOR2:def 1 for a being Object of A holds <^ F1.a,F2.a^> <> {}; reflexivity; end; theorem :: FUNCTOR2:2 for A,B being transitive with_units non empty AltCatStr, F,F1, F2 being Functor of A,B holds F is_transformable_to F1 & F1 is_transformable_to F2 implies F is_transformable_to F2; definition let A,B be transitive with_units non empty AltCatStr, F1,F2 be Functor of A,B; assume F1 is_transformable_to F2; mode transformation of F1,F2 -> ManySortedSet of the carrier of A means :: FUNCTOR2:def 2 for a being Object of A holds it.a is Morphism of F1.a,F2.a; end; definition let A,B be transitive with_units non empty AltCatStr; let F be Functor of A,B; func idt F -> transformation of F,F means :: FUNCTOR2:def 3 for a being Object of A holds it.a = idm (F.a); end; definition let A,B be transitive with_units non empty AltCatStr, F1,F2 be Functor of A,B; assume F1 is_transformable_to F2; let t be transformation of F1,F2; let a be Object of A; func t!a -> Morphism of F1.a, F2.a means :: FUNCTOR2:def 4 it = t.a; end; definition let A,B be transitive with_units non empty AltCatStr, F,F1,F2 be Functor of A,B; assume F is_transformable_to F1 & F1 is_transformable_to F2; let t1 be transformation of F,F1; let t2 be transformation of F1,F2; func t2`*`t1 -> transformation of F,F2 means :: FUNCTOR2:def 5 for a being Object of A holds it!a = (t2!a) * (t1!a); end; theorem :: FUNCTOR2:3 for A,B being transitive with_units non empty AltCatStr, F1,F2 being Functor of A,B holds F1 is_transformable_to F2 implies for t1, t2 being transformation of F1,F2 st for a being Object of A holds t1!a = t2!a holds t1 = t2; theorem :: FUNCTOR2:4 for A,B being transitive with_units non empty AltCatStr, F being Functor of A,B holds for a being Object of A holds (idt F)!a = idm(F.a); theorem :: FUNCTOR2:5 for A,B being transitive with_units non empty AltCatStr, F1,F2 being Functor of A,B holds F1 is_transformable_to F2 implies for t being transformation of F1,F2 holds (idt F2)`*`t = t & t`*`(idt F1) = t; theorem :: FUNCTOR2:6 for A,B being category, F,F1,F2,F3 being Functor of A,B holds F is_transformable_to F1 & F1 is_transformable_to F2 & F2 is_transformable_to F3 implies for t1 being transformation of F,F1, t2 being transformation of F1,F2, t3 being transformation of F2,F3 holds t3`*`t2`*`t1 = t3`*`(t2`*`t1); begin definition let A,B be transitive with_units non empty AltCatStr, F1,F2 be covariant Functor of A,B; pred F1 is_naturally_transformable_to F2 means :: FUNCTOR2:def 6 F1 is_transformable_to F2 & ex t being transformation of F1,F2 st for a,b being Object of A st <^a,b^> <> {} for f being Morphism of a,b holds t!b*F1.f = F2.f*(t!a); reflexivity; end; theorem :: FUNCTOR2:7 for A,B be transitive with_units non empty AltCatStr, F be covariant Functor of A,B holds F is_naturally_transformable_to F; theorem :: FUNCTOR2:8 for A,B be category, F,F1,F2 be covariant Functor of A,B holds F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 implies F is_naturally_transformable_to F2; definition let A,B be transitive with_units non empty AltCatStr, F1,F2 be covariant Functor of A,B; assume F1 is_naturally_transformable_to F2; mode natural_transformation of F1,F2 -> transformation of F1,F2 means :: FUNCTOR2:def 7 for a,b being Object of A st <^a,b^> <> {} for f being Morphism of a,b holds it !b*F1.f = F2.f*(it!a); end; definition let A,B be transitive with_units non empty AltCatStr, F be covariant Functor of A,B; redefine func idt F -> natural_transformation of F,F; end; definition let A,B be category, F,F1,F2 be covariant Functor of A,B such that F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2; let t1 be natural_transformation of F,F1; let t2 be natural_transformation of F1,F2; func t2`*`t1 -> natural_transformation of F,F2 means :: FUNCTOR2:def 8 it = t2`*`t1; end; theorem :: FUNCTOR2:9 for A,B be transitive with_units non empty AltCatStr, F1,F2 be covariant Functor of A,B holds F1 is_naturally_transformable_to F2 implies for t being natural_transformation of F1,F2 holds (idt F2)`*`t = t & t`*`(idt F1) = t; theorem :: FUNCTOR2:10 for A,B be transitive with_units non empty AltCatStr, F,F1,F2 be covariant Functor of A,B holds F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 implies 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); theorem :: FUNCTOR2:11 for A,B be category, F,F1,F2,F3 be covariant Functor of A,B for t be natural_transformation of F,F1, t1 be natural_transformation of F1,F2 holds F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 implies for t3 being natural_transformation of F2,F3 holds t3`*`t1`*`t = t3`*`(t1`*`t); begin :: Category of Functors definition let I be set; let A,B be ManySortedSet of I; func Funcs(A,B) -> set means :: FUNCTOR2:def 9 for x be set holds x in it iff x is ManySortedFunction of A,B if for i being set st i in I holds B.i = {} implies A .i = {} otherwise it = {}; end; definition let A,B be transitive with_units non empty AltCatStr; func Funct(A,B) -> set means :: FUNCTOR2:def 10 for x being object holds x in it iff x is covariant strict Functor of A,B; end; definition let A,B be category; func Functors(A,B) -> strict non empty transitive AltCatStr means :: FUNCTOR2:def 11 the carrier of it = Funct(A,B) & (for F,G being strict covariant Functor of A,B, x being set holds x in (the Arrows of it).(F,G) iff F is_naturally_transformable_to G & x is natural_transformation of F,G) & for F,G ,H being strict covariant Functor of A,B st F is_naturally_transformable_to G & G is_naturally_transformable_to H for t1 being natural_transformation of F,G, t2 being natural_transformation of G,H ex f being Function st f = (the Comp of it).(F,G,H) & f.(t2,t1) = t2`*`t1; end;