:: ALTCAT_2 semantic presentation

theorem Th1: :: ALTCAT_2:1

for b₁, b₂, b₃, b₄ being set holds [:(b₁ --> b₃),(b₂ --> b₄):] = [:b₁,b₂:] --> [b₃,b₄]

proof end;

registration

let c₁ be set ;
cluster [0] a₁ -> Function-yielding ;
coherence

proof end;

end;

theorem Th2: :: ALTCAT_2:2

for b₁, b₂ being Function holds ~ (b₂ * b₁) = b₂ * (~ b₁)

proof end;

theorem Th3: :: ALTCAT_2:3

for b₁, b₂, b₃ being Function holds ~ (b₁ * [:b₂,b₃:]) = (~ b₁) * [:b₃,b₂:]

proof end;

registration

let c₁ be Function-yielding Function;
cluster ~ a₁ -> Function-yielding ;
coherence

proof end;

end;

theorem Th4: :: ALTCAT_2:4

for b₁ being set
for b₂, b₃, b₄ being ManySortedSet of b₁ st b₂ is_transformable_to b₃ holds
for b₅ being ManySortedFunction of b₂,b₃
for b₆ being ManySortedFunction of b₃,b₄ holds b₆ ** b₅ is ManySortedFunction of b₂,b₄

proof end;

definition

let c₁ be set ;
let c₂ be ManySortedSet of [:c₁,c₁:];
redefine func ~ as ~ c₂ -> ManySortedSet of [:a₁,a₁:];
coherence

proof end;

end;

theorem Th5: :: ALTCAT_2:5

for b₁ being set
for b₂ being non empty set
for b₃ being Function of b₁,b₂
for b₄, b₅ being ManySortedSet of b₂
for b₆ being ManySortedFunction of b₄,b₅ holds b₆ * b₃ is ManySortedFunction of b₄ * b₃,b₅ * b₃

proof end;

definition

let c₁ be set ;
let c₂, c₃ be ManySortedSet of [:c₁,c₁:];
let c₄ be ManySortedFunction of c₂,c₃;
redefine func ~ as ~ c₄ -> ManySortedFunction of ~ a₂, ~ a₃;
coherence

proof end;

end;

theorem Th6: :: ALTCAT_2:6

for b₁, b₂ being non empty set
for b₃ being ManySortedSet of [:b₁,b₂:]
for b₄ being Element of b₁
for b₅ being Element of b₂ holds (~ b₃) . b₅,b₄ = b₃ . b₄,b₅

proof end;

definition

let c₁ be set ;
let c₂, c₃ be ManySortedFunction of c₁;
redefine func ** as c₃ ** c₂ -> ManySortedFunction of a₁;
coherence

proof end;

end;

definition

let c₁, c₂ be Function;
pred c₁ cc= c₂ means :Def1: :: ALTCAT_2:def 1
( dom a₁ c= dom a₂ & ( for b₁ being set st b₁ in dom a₁ holds
a₁ . b₁ c= a₂ . b₁ ) );
reflexivity ;

end;

:: deftheorem Def1 defines cc= ALTCAT_2:def 1 :

definition

let c₁, c₂ be set ;
let c₃ be ManySortedSet of c₁;
let c₄ be ManySortedSet of c₂;
redefine pred cc= as c₃ cc= c₄ means :Def2: :: ALTCAT_2:def 2
( a₁ c= a₂ & ( for b₁ being set st b₁ in a₁ holds
a₃ . b₁ c= a₄ . b₁ ) );
compatibility

proof end;

end;

:: deftheorem Def2 defines cc= ALTCAT_2:def 2 :

theorem Th7: :: ALTCAT_2:7

canceled;

theorem Th8: :: ALTCAT_2:8

for b₁, b₂ being set
for b₃ being ManySortedSet of b₁
for b₄ being ManySortedSet of b₂ st b₃ cc= b₄ & b₄ cc= b₃ holds
b₃ = b₄

proof end;

theorem Th9: :: ALTCAT_2:9

for b₁, b₂, b₃ being set
for b₄ being ManySortedSet of b₁
for b₅ being ManySortedSet of b₂
for b₆ being ManySortedSet of b₃ st b₄ cc= b₅ & b₅ cc= b₆ holds
b₄ cc= b₆

proof end;

theorem Th10: :: ALTCAT_2:10

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ holds
( b₂ cc= b₃ iff b₂ c= b₃ )

proof end;

scheme :: ALTCAT_2:sch 1
s1{ F₁() -> non empty set , F₂( set ) -> set , P₁[ set ] } :

{ [b₁,F₂(b₁)] where B is Element of F₁() : P₁[b₁] } is Function

proof end;

scheme :: ALTCAT_2:sch 2
s2{ F₁() -> non empty set , F₂() -> Function, F₃( set ) -> set , P₁[ set ] } :

dom F₂() = { b₁ where B is Element of F₁() : P₁[b₁] }

provided

E5: F₂() = { [b₁,F₃(b₁)] where B is Element of F₁() : P₁[b₁] }

proof end;

scheme :: ALTCAT_2:sch 3
s3{ F₁() -> non empty set , F₂() -> Function, F₃() -> Element of F₁(), F₄( set ) -> set , P₁[ set ] } :

F₂() . F₃() = F₄(F₃())

provided

E5: F₂() = { [b₁,F₄(b₁)] where B is Element of F₁() : P₁[b₁] } and
E6: P₁[F₃()]

proof end;

theorem Th11: :: ALTCAT_2:11

for b₁ being Category
for b₂, b₃, b₄ being Object of b₁ holds [:(Hom b₃,b₄),(Hom b₂,b₃):] c= dom the Comp of b₁

proof end;

theorem Th12: :: ALTCAT_2:12

for b₁ being Category
for b₂, b₃, b₄ being Object of b₁ holds the Comp of b₁ .: [:(Hom b₃,b₄),(Hom b₂,b₃):] c= Hom b₂,b₄

proof end;

definition

let c₁ be CatStr ;
func the_hom_sets_of c₁ -> ManySortedSet of [:the Objects of a₁,the Objects of a₁:] means :Def3: :: ALTCAT_2:def 3
for b₁, b₂ being Object of a₁ holds a₂ . b₁,b₂ = Hom b₁,b₂;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines the_hom_sets_of ALTCAT_2:def 3 :

theorem Th13: :: ALTCAT_2:13

for b₁ being Category
for b₂ being Object of b₁ holds id b₂ in (the_hom_sets_of b₁) . b₂,b₂

proof end;

definition

let c₁ be Category;
func the_comps_of c₁ -> BinComp of (the_hom_sets_of a₁) means :Def4: :: ALTCAT_2:def 4
for b₁, b₂, b₃ being Object of a₁ holds a₂ . b₁,b₂,b₃ = the Comp of a₁ | [:((the_hom_sets_of a₁) . b₂,b₃),((the_hom_sets_of a₁) . b₁,b₂):];
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines the_comps_of ALTCAT_2:def 4 :

theorem Th14: :: ALTCAT_2:14

for b₁ being Category
for b₂, b₃, b₄ being Object of b₁ st Hom b₂,b₃ <> {} & Hom b₃,b₄ <> {} holds
for b₅ being Morphism of b₂,b₃
for b₆ being Morphism of b₃,b₄ holds ((the_comps_of b₁) . b₂,b₃,b₄) . b₆,b₅ = b₆ * b₅

proof end;

theorem Th15: :: ALTCAT_2:15

for b₁ being Category holds the_comps_of b₁ is associative

proof end;

theorem Th16: :: ALTCAT_2:16

for b₁ being Category holds
( the_comps_of b₁ is with_left_units & the_comps_of b₁ is with_right_units )

proof end;

definition

let c₁ be Category;
func Alter c₁ -> non empty strict AltCatStr equals :: ALTCAT_2:def 5
AltCatStr(# the Objects of a₁,(the_hom_sets_of a₁),(the_comps_of a₁) #);
correctness ;

end;

:: deftheorem Def5 defines Alter ALTCAT_2:def 5 :

theorem Th17: :: ALTCAT_2:17

for b₁ being Category holds Alter b₁ is associative

proof end;

theorem Th18: :: ALTCAT_2:18

for b₁ being Category holds Alter b₁ is with_units

proof end;

theorem Th19: :: ALTCAT_2:19

for b₁ being Category holds Alter b₁ is transitive

proof end;

registration

let c₁ be Category;
cluster Alter a₁ -> non empty transitive strict associative with_units ;
coherence by Th17, Th18, Th19;

end;

registration

cluster non empty strict AltGraph ;
existence

proof end;

end;

definition

let c₁ be AltGraph ;
attr a₁ is reflexive means :Def6: :: ALTCAT_2:def 6
for b₁ being set st b₁ in the carrier of a₁ holds
the Arrows of a₁ . b₁,b₁ <> {} ;

end;

:: deftheorem Def6 defines reflexive ALTCAT_2:def 6 :

definition

let c₁ be non empty AltGraph ;
redefine attr a₁ is reflexive means :: ALTCAT_2:def 7
for b₁ being object of a₁ holds <^b₁,b₁^> <> {} ;
compatibility

proof end;

end;

:: deftheorem Def7 defines reflexive ALTCAT_2:def 7 :

definition

let c₁ be non empty transitive AltCatStr ;
redefine attr a₁ is associative means :Def8: :: ALTCAT_2:def 8
for b₁, b₂, b₃, b₄ being object of a₁
for b₅ being Morphism of b₁,b₂
for b₆ being Morphism of b₂,b₃
for b₇ being Morphism of b₃,b₄ st <^b₁,b₂^> <> {} & <^b₂,b₃^> <> {} & <^b₃,b₄^> <> {} holds
(b₇ * b₆) * b₅ = b₇ * (b₆ * b₅);
compatibility

proof end;

end;

:: deftheorem Def8 defines associative ALTCAT_2:def 8 :

definition

let c₁ be non empty AltCatStr ;
redefine attr a₁ is with_units means :: ALTCAT_2:def 9
for b₁ being object of a₁ holds
( <^b₁,b₁^> <> {} & ex b₂ being Morphism of b₁,b₁ st
for b₃ being object of a₁
for b₄ being Morphism of b₃,b₁
for b₅ being Morphism of b₁,b₃ holds
( ( <^b₃,b₁^> <> {} implies b₂ * b₄ = b₄ ) & ( <^b₁,b₃^> <> {} implies b₅ * b₂ = b₅ ) ) );
compatibility

proof end;

end;

:: deftheorem Def9 defines with_units ALTCAT_2:def 9 :

registration

cluster non empty with_units -> non empty reflexive AltCatStr ;
coherence

proof end;

end;

registration

cluster non empty reflexive AltGraph ;
existence

proof end;

end;

registration

cluster non empty reflexive AltCatStr ;
existence

proof end;

end;

Lemma18: for b₁, b₂ being strict AltCatStr st the carrier of b₁ is empty & the carrier of b₂ is empty holds
b₁ = b₂

proof end;

definition

func the_empty_category -> strict AltCatStr means :Def10: :: ALTCAT_2:def 10
the carrier of a₁ is empty;
existence

proof end;

uniqueness by Lemma18;

end;

:: deftheorem Def10 defines the_empty_category ALTCAT_2:def 10 :

registration

cluster the_empty_category -> empty strict ;
coherence

proof end;

end;

registration

cluster empty strict AltCatStr ;
existence

proof end;

end;

theorem Th20: :: ALTCAT_2:20

for b₁ being empty strict AltCatStr holds b₁ = the_empty_category

proof end;

definition

let c₁ be AltCatStr ;
mode SubCatStr of c₁ -> AltCatStr means :Def11: :: ALTCAT_2:def 11
( the carrier of a₂ c= the carrier of a₁ & the Arrows of a₂ cc= the Arrows of a₁ & the Comp of a₂ cc= the Comp of a₁ );
existence ;

end;

:: deftheorem Def11 defines SubCatStr ALTCAT_2:def 11 :

theorem Th21: :: ALTCAT_2:21

for b₁ being AltCatStr holds b₁ is SubCatStr of b₁

proof end;

theorem Th22: :: ALTCAT_2:22

for b₁, b₂, b₃ being AltCatStr st b₁ is SubCatStr of b₂ & b₂ is SubCatStr of b₃ holds
b₁ is SubCatStr of b₃

proof end;

theorem Th23: :: ALTCAT_2:23

for b₁, b₂ being AltCatStr st b₁ is SubCatStr of b₂ & b₂ is SubCatStr of b₁ holds
AltCatStr(# the carrier of b₁,the Arrows of b₁,the Comp of b₁ #) = AltCatStr(# the carrier of b₂,the Arrows of b₂,the Comp of b₂ #)

proof end;

registration

let c₁ be AltCatStr ;
cluster strict SubCatStr of a₁;
existence

proof end;

end;

definition

let c₁ be non empty AltCatStr ;
let c₂ be object of c₁;
func ObCat c₂ -> strict SubCatStr of a₁ means :Def12: :: ALTCAT_2:def 12
( the carrier of a₃ = {a₂} & the Arrows of a₃ = a₂,a₂ :-> <^a₂,a₂^> & the Comp of a₃ = [a₂,a₂,a₂] .--> (the Comp of a₁ . a₂,a₂,a₂) );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def12 defines ObCat ALTCAT_2:def 12 :

theorem Th24: :: ALTCAT_2:24

for b₁ being non empty AltCatStr
for b₂ being object of b₁
for b₃ being object of (ObCat b₂) holds b₃ = b₂

proof end;

registration

let c₁ be non empty AltCatStr ;
let c₂ be object of c₁;
cluster ObCat a₂ -> non empty transitive strict ;
coherence

proof end;

end;

registration

let c₁ be non empty AltCatStr ;
cluster non empty transitive strict SubCatStr of a₁;
existence

proof end;

end;

theorem Th25: :: ALTCAT_2:25

for b₁ being non empty transitive AltCatStr
for b₂, b₃ being non empty transitive SubCatStr of b₁ st the carrier of b₂ c= the carrier of b₃ & the Arrows of b₂ cc= the Arrows of b₃ holds
b₂ is SubCatStr of b₃

proof end;

definition

let c₁ be AltCatStr ;
let c₂ be SubCatStr of c₁;
attr a₂ is full means :Def13: :: ALTCAT_2:def 13
the Arrows of a₂ = the Arrows of a₁ || the carrier of a₂;

end;

:: deftheorem Def13 defines full ALTCAT_2:def 13 :

definition

let c₁ be non empty with_units AltCatStr ;
let c₂ be SubCatStr of c₁;
attr a₂ is id-inheriting means :Def14: :: ALTCAT_2:def 14
for b₁ being object of a₂
for b₂ being object of a₁ st b₁ = b₂ holds
idm b₂ in <^b₁,b₁^> if not a₂ is empty
otherwise verum;
consistency ;

end;

:: deftheorem Def14 defines id-inheriting ALTCAT_2:def 14 :

registration

let c₁ be AltCatStr ;
cluster strict full SubCatStr of a₁;
existence

proof end;

end;

registration

let c₁ be non empty AltCatStr ;
cluster non empty strict full SubCatStr of a₁;
existence

proof end;

end;

registration

let c₁ be category;
let c₂ be object of c₁;
cluster ObCat a₂ -> non empty transitive strict full id-inheriting ;
coherence

proof end;

end;

registration

let c₁ be category;
cluster non empty strict full id-inheriting SubCatStr of a₁;
existence

proof end;

end;

theorem Th26: :: ALTCAT_2:26

for b₁ being non empty transitive AltCatStr
for b₂ being SubCatStr of b₁ st the carrier of b₂ = the carrier of b₁ & the Arrows of b₂ = the Arrows of b₁ holds
AltCatStr(# the carrier of b₂,the Arrows of b₂,the Comp of b₂ #) = AltCatStr(# the carrier of b₁,the Arrows of b₁,the Comp of b₁ #)

proof end;

theorem Th27: :: ALTCAT_2:27

for b₁ being non empty transitive AltCatStr
for b₂, b₃ being non empty transitive SubCatStr of b₁ st the carrier of b₂ = the carrier of b₃ & the Arrows of b₂ = the Arrows of b₃ holds
AltCatStr(# the carrier of b₂,the Arrows of b₂,the Comp of b₂ #) = AltCatStr(# the carrier of b₃,the Arrows of b₃,the Comp of b₃ #)

proof end;

theorem Th28: :: ALTCAT_2:28

for b₁ being non empty transitive AltCatStr
for b₂ being full SubCatStr of b₁ st the carrier of b₂ = the carrier of b₁ holds
AltCatStr(# the carrier of b₂,the Arrows of b₂,the Comp of b₂ #) = AltCatStr(# the carrier of b₁,the Arrows of b₁,the Comp of b₁ #)

proof end;

theorem Th29: :: ALTCAT_2:29

for b₁ being non empty AltCatStr
for b₂ being non empty full SubCatStr of b₁
for b₃, b₄ being object of b₁
for b₅, b₆ being object of b₂ st b₃ = b₅ & b₄ = b₆ holds
<^b₃,b₄^> = <^b₅,b₆^>

proof end;

theorem Th30: :: ALTCAT_2:30

for b₁ being non empty AltCatStr
for b₂ being non empty SubCatStr of b₁
for b₃ being object of b₂ holds b₃ is object of b₁

proof end;

registration

let c₁ be non empty transitive AltCatStr ;
cluster non empty full -> transitive SubCatStr of a₁;
coherence

proof end;

end;

theorem Th31: :: ALTCAT_2:31

for b₁ being non empty transitive AltCatStr
for b₂, b₃ being non empty full SubCatStr of b₁ st the carrier of b₂ = the carrier of b₃ holds
AltCatStr(# the carrier of b₂,the Arrows of b₂,the Comp of b₂ #) = AltCatStr(# the carrier of b₃,the Arrows of b₃,the Comp of b₃ #)

proof end;

theorem Th32: :: ALTCAT_2:32

for b₁ being non empty AltCatStr
for b₂ being non empty SubCatStr of b₁
for b₃, b₄ being object of b₁
for b₅, b₆ being object of b₂ st b₃ = b₅ & b₄ = b₆ holds
<^b₅,b₆^> c= <^b₃,b₄^>

proof end;

theorem Th33: :: ALTCAT_2:33

for b₁ being non empty transitive AltCatStr
for b₂ being non empty transitive SubCatStr of b₁
for b₃, b₄, b₅ being object of b₂ st <^b₃,b₄^> <> {} & <^b₄,b₅^> <> {} holds
for b₆, b₇, b₈ being object of b₁ st b₆ = b₃ & b₇ = b₄ & b₈ = b₅ holds
for b₉ being Morphism of b₆,b₇
for b₁₀ being Morphism of b₇,b₈
for b₁₁ being Morphism of b₃,b₄
for b₁₂ being Morphism of b₄,b₅ st b₉ = b₁₁ & b₁₀ = b₁₂ holds
b₁₀ * b₉ = b₁₂ * b₁₁

proof end;

registration

let c₁ be non empty transitive associative AltCatStr ;
cluster non empty transitive -> non empty associative SubCatStr of a₁;
coherence

proof end;

end;

theorem Th34: :: ALTCAT_2:34

for b₁ being non empty AltCatStr
for b₂ being non empty SubCatStr of b₁
for b₃, b₄ being object of b₁
for b₅, b₆ being object of b₂ st b₃ = b₅ & b₄ = b₆ & <^b₅,b₆^> <> {} holds
for b₇ being Morphism of b₅,b₆ holds b₇ is Morphism of b₃,b₄

proof end;

registration

let c₁ be non empty transitive with_units AltCatStr ;
cluster non empty transitive id-inheriting -> non empty with_units reflexive SubCatStr of a₁;
coherence

proof end;

end;

registration

let c₁ be category;
cluster non empty transitive associative with_units reflexive id-inheriting SubCatStr of a₁;
existence

proof end;

end;

definition

let c₁ be category;
mode subcategory of a₁ is transitive id-inheriting SubCatStr of a₁;

end;

theorem Th35: :: ALTCAT_2:35

for b₁ being category
for b₂ being non empty subcategory of b₁
for b₃ being object of b₂
for b₄ being object of b₁ st b₃ = b₄ holds
idm b₃ = idm b₄

proof end;