environ
vocabularies HIDDEN, FUNCT_1, TARSKI, ZFMISC_1, XBOOLE_0, RELAT_1, SUBSET_1, WELLORD1, CAT_1, ALTCAT_1, GRAPH_1, BINOP_1, STRUCT_0, PARTFUN1, FUNCOP_1, MONOID_0, NATTRA_1, MSSUBFAM, ALTCAT_2, ARYTM_0, NUMBERS, ARYTM_3, CARD_1, FUNCTOR0, MOD_4, CAT_6, NAT_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCT_3, FUNCT_4, RELAT_1, FUNCT_1, FUNCT_2, ORDINAL1, PARTFUN1, FINSEQ_1, STRUCT_0, FUNCOP_1, RELSET_1, BINOP_1, GRAPH_1, CAT_1, CAT_2, NUMBERS, NAT_1, XXREAL_0, XTUPLE_0, ALG_1, XCMPLX_0, WELLORD2, CARD_1, INT_1, VALUED_0, ISOCAT_1;
definitions ;
theorems TARSKI, XBOOLE_0, XTUPLE_0, ZFMISC_1, RELAT_1, FUNCT_1, STRUCT_0, FUNCT_2, SUBSET_1, BINOP_1, GRAPH_1, CAT_1, FUNCOP_1, FUNCT_4, NAT_1, ORDINAL1, ISOCAT_1;
schemes FUNCT_2;
registrations XBOOLE_0, SUBSET_1, ZFMISC_1, RELAT_1, FUNCT_1, ORDINAL1, XTUPLE_0, CARD_1, CLASSES2, STRUCT_0, RELSET_1, FUNCT_2, PARTFUN1, GRFUNC_1, BINOP_1, CAT_1, CARD_2, NAT_LAT, FINSET_1, XXREAL_0, XREAL_0, NAT_1, NUMBERS, VALUED_0, FINSEQ_1;
constructors HIDDEN, NUMBERS, FUNCT_2, CLASSES2, FINSEQ_1, STRUCT_0, FUNCOP_1, RELAT_2, PARTFUN1, RELSET_1, BINOP_1, FUNCT_4, CAT_1, CAT_2, NAT_1, XXREAL_0, WELLORD2, XREAL_0, CARD_1, XCMPLX_0, INT_1, VALUED_0, ISOCAT_1;
requirements HIDDEN, SUBSET, BOOLE, REAL, NUMERALS, ARITHM;
equalities ;
expansions ;
Lm1:
the empty CategoryStr opp is discrete
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 ) ) )
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 ) ) ) )
Lm4:
for C being CategoryStr
for f, g being morphism of C st g |> f holds
g (*) f = the composition of C . [g,f]
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 )
definition
let C be
composable with_identities CategoryStr ;
correctness
consistency
for b1 being Function of (Mor C),(Ob C) holds verum;
existence
( ( for b1 being Function of (Mor C),(Ob C) holds verum ) & ( not C is empty implies ex b1 being Function of (Mor C),(Ob C) st
for f being Element of Mor C holds b1 . f = dom f ) & ( C is empty implies ex b1 being Function of (Mor C),(Ob C) st b1 = {} ) );
uniqueness
for b1, b2 being Function of (Mor C),(Ob C) holds
( ( not C is empty & ( for f being Element of Mor C holds b1 . f = dom f ) & ( for f being Element of Mor C holds b2 . f = dom f ) implies b1 = b2 ) & ( C is empty & b1 = {} & b2 = {} implies b1 = b2 ) );
correctness
consistency
for b1 being Function of (Mor C),(Ob C) holds verum;
existence
( ( for b1 being Function of (Mor C),(Ob C) holds verum ) & ( not C is empty implies ex b1 being Function of (Mor C),(Ob C) st
for f being Element of Mor C holds b1 . f = cod f ) & ( C is empty implies ex b1 being Function of (Mor C),(Ob C) st b1 = {} ) );
uniqueness
for b1, b2 being Function of (Mor C),(Ob C) holds
( ( not C is empty & ( for f being Element of Mor C holds b1 . f = cod f ) & ( for f being Element of Mor C holds b2 . f = cod f ) implies b1 = b2 ) & ( C is empty & b1 = {} & b2 = {} implies b1 = b2 ) );
end;
Lm6:
for C being non empty category holds CatStr(# (Ob C),(Mor C),(SourceMap C),(TargetMap C),(CompMap C) #) is Category
Lm7:
for C being Category holds CategoryStr(# the carrier' of C, the Comp of C #) is category