(*******************************************************************
The idea in this file is to start with an axiomatized ZFC-type set theory
and develop mathematics from there. The main advantage is that we obtain
an untyped theory---all objects are sets (the exception being that we often
look at things of type E -> E, E-> Prop, E->E->E etc; but even in these cases
there is no dependancy).  At the start we need some tools that essentially
serve to recreate an environment similar to type theory. The first aspect of 
this situation is that typing relations are replaced by properties, for example x:a
is replaced by (inc x a). This allows us to manipulate typing information just as any
other information. The next aspect is definition of functions replacing certain
type-theoretic operations.  For example the operation L with syntax (L a [y:E](f y)) 
means the function with domain set a, whose values are given by the formula f. It 
is an element of a function space (F a [y:E](b y)) whenever 
(y:E)(inc y a) -> (inc (f y) (b y)).  Thus L replaces the lambda operation and 
F replaces the dependent product construction.   We similarly use D for a 
record-type construction with J as the constructor, Z for cutting out subsets,
and Y for a switch.  Also we abbreviate `and' by A, which allows a compact
representation of large conjunctions (this is preferable to the Record construction
because it is "first-class"). All of these constructions will need special tactics;
we start by giving some for A.  For the moment all of these operations are just 
axiomatized as parameters but of course later we will be able to give their 
set-theoretic definitions. 
    With all of this, it turns out to be possible to write mathematical definitions 
and statements, just about as easily as writing in natural language (with the added 
benefit of precision).  On the other hand, the transformation of typing information
into mathematical properties, as well as the re-definition of type-theoretic 
operations in the set-theoretical context, could cause additional difficulties 
in the proofs. We do only a very few proofs at the start, in the current version; 
the rest are "skipped".
    This is part of an ongoing project involving interaction with Marco Maggesi,
Andre Hirschowitz, Laurent Chicli and others. Most of the mathematical content 
presented here comes from discussions with them and from contributions they are 
developing. Also it should be pointed out that the axiomatic set theory approach 
has numerous  antecedents (cf the discussion in "FunctionsInZFC").
    The present version is a preliminary version, subject to potential modifications 
even at the beginning (in particular, statements whose proofs are skipped may well 
be wrong).
    The only concrete claim I make is that it successfully compiles under Coq 7.4. 
    ---Carlos Simpson, Nice, April 17th 2003
******************************************************************************)


Require Export Arith.
Require Export ZArith.

Parameter joker : (P:Prop)P.

Tactic Definition Skip := EApply joker.

Set Implicit Arguments.





Parameter E:Type.
Parameter inc : E -> E -> Prop.
Definition sub := [a,b:E](x:E)(inc x a) -> (inc x b).
Axiom extensionality : (a,b:E)(sub a b)
 -> (sub b a) -> a == b.

Syntactic Definition E1 := E -> E.
Syntactic Definition E2 := E -> E1.
Syntactic Definition E3 := E -> E2.
Syntactic Definition E4 := E -> E3.
Syntactic Definition E5 := E -> E4.
Syntactic Definition E6 := E -> E5.
(** thus for example E3 = E -> E -> E -> E **)


Definition A := and.

Parameter Y : Prop -> E -> E -> E.
(* (Y p x y) means x if p or else y if not *)

Parameter Z : E -> (E -> Prop) -> E.
(* cutting out a subset *)

Module AYZ.
Axiom a1 : (p:Prop; x,y:E)p -> (Y p x y) == x.
Axiom a2 : (p:Prop; x,y:E)(not p) -> (Y p x y) == y.

Axiom em : (p:Prop)p \/ (not p).

(* put in stuff about Z ???*)

End AYZ.

Recursive Tactic Definition Deconj :=
Match Context With
[|- (A ?  ?)] -> Unfold A; Apply conj; [Idtac |Deconj]
|
[|- (and ?  ?)] -> Apply conj; [Idtac |Deconj]
|
[|-  ? /\ ?] -> Apply conj; [Idtac |Deconj]

|
[|- ?]  -> Idtac.

Tactic Definition UnfoldDeconj d := (Unfold d); Deconj.






Recursive Tactic Definition Expand := 
Match Context With 
[id1 : (A ?1 ?2) |- ?] -> (Unfold A in id1); NewInduction id1; Expand
|
[id1 : (and ?1 ?2) |- ?] -> NewInduction id1; Expand
|
[id1 : (?1 /\ ?2) |- ?] -> NewInduction id1; Expand
|
[|- ?] -> Idtac.




Inductive exists [p:E -> Prop]: Prop :=
exists_intro : (x:E)(p x) -> (exists p).
Definition exists_unique := [p:E->Prop]
(A (exists p)
   (x,y:E)(p x) -> (p y) -> x == y
).

Axiom excluded_middle : (P:Prop)(not (not P)) -> P.


Lemma exists_proof : (p:E->Prop)(not (x:E)(not (p x))) -> (exists p).
Proof.
Intros. Unfold not in H. EApply excluded_middle. Unfold not.
Intros. Apply H. Intros. Apply H0. EApply exists_intro with x.
Assumption. Save.

Lemma not_exists_pr : (p:E-> Prop)(not (exists p)) <-> ((x:E)(not (p x))).
Proof.
Intros. Unfold iff. Apply conj. Intros. Unfold not. Unfold not in H.
Intros. Apply H. Apply exists_intro with x. Assumption.
  Intros. Unfold not. Unfold not in H. Intros. NewInduction H0.
Apply H with x. Assumption. Save. 


Inductive nonemptyT [t:Type] : Prop := 
nonemptyT_intro : t -> (nonemptyT t).


Parameter chooseT :(t:Type; p: t-> Prop)(nonemptyT t) -> t.
Axiom chooseT_pr : (t:Type; p: t-> Prop; ne: (nonemptyT t))
(exT ? p)-> (p (chooseT p ne)).

Parameter choose : (E -> Prop) -> E.
Axiom choose_pr : (p:E -> Prop)(exists p) -> (p (choose p)).

Parameter get : E -> E -> E.
Parameter set : E -> E -> E -> E.

Parameter pair : E -> E -> E.
Parameter pr1 : E -> E.
Parameter pr2 : E -> E.
Axiom pr1_pair : (x,y:E)(pr1 (pair x y)) == x.
Axiom pr2_pair : (x,y:E)(pr2 (pair x y)) == y.

Definition is_pair := [u:E](pair (pr1 u) (pr2 u)) == u.

Parameter singleton : E -> E.
Axiom singleton_incl : (x:E)(inc x (singleton x)).
Axiom singleton_uni : (x,y:E)(inc y (singleton x)) -> x == y.


Definition ev := [f,x:E](choose [y:E](inc (pair x y) f)).

Module Image.

Parameter create : (E -> E) -> E -> E.
Axiom incl : (f:E -> E; x,a:E)(inc x a) -> (inc (f x) (create f a)).
Axiom ex : (f:E-> E; x,a:E)(inc x (create f a)) ->
(exists [y:E]((inc y a) /\ (f y) == x)).

End Image.


Parameter cut : (E -> Prop) -> E -> E.
Axiom cut1 : (p:E -> Prop; x,y:E)(inc y (cut p x)) -> (p y).
Axiom cut2 : (p:E -> Prop; x:E)(sub (cut p x) x).
Axiom cut3 : (p:E-> Prop; x,y:E)(inc y x) -> (p y) -> (inc y (cut p x)).

Definition neq := [x,y:E]~(x == y).

Axiom get_set_neq : (x,y,u,a:E)(neq x y) -> (get x (set y u a)) ==
(get x a).
Axiom get_set_eq : (x,y,u,a:E)(x == y) -> (get x (set y u a)) ==
u.
Axiom set_set : (x,y,u,v,a:E)(set x u (set y v a)) == (set y v (set 
x u a)).
Axiom set_set_eq : (x,u,v,a:E)(set x u (set x v a)) == (set x u a).

Parameter next : E -> E.

Definition strict_sub := [a,b:E]
(A (neq a b)
   (sub a b)
).


Axiom sub_trans : (a,b,c:E)(sub a b) -> (sub b c) -> (sub a c).
Axiom strict_sub_trans1 : (a,b,c:E)(strict_sub a b) -> (sub b c) -> 
(strict_sub a c).
Axiom strict_sub_trans2 : (a,b,c:E)(sub a b) -> (strict_sub b c) -> 
(strict_sub a c).

Parameter emptyset : E.
Axiom emptyset_empty : (x:E)~(inc x emptyset).

Definition nat_E : nat -> E.
Intro n.
NewInduction n.
Exact emptyset.
Exact (next IHn).
Defined.



Definition index := [i:nat](nat_E i).


Axiom nat_E_inj : (i,j : nat) (nat_E i) == (nat_E j) -> i == j.
Lemma nat_E_neq : (i,j:nat)~(i==j) -> (neq (nat_E i) (nat_E j)).
Intros. Unfold neq. Unfold not. Intros. Apply H. Apply nat_E_inj.
Assumption. Save.

Axiom get_set_index : (i,j: nat; u,a:E)~(i == j) -> (get (index i) 
(set (index j) u a)) == (get (index i) a).



Parameter powerset : E -> E.
Axiom powerset_ax1 : (x,a:E)(sub x a) -> (inc x (powerset a)).
Axiom powerset_ax2 : (x,a:E)(inc x (powerset a)) -> (sub x a).

Parameter union : E -> E.
Axiom union_ax1 : (x,y,a:E)(inc x y) -> (inc y a) -> (inc x (union a)).
Axiom union_ax2 : (x,a:E)(inc x (union a)) -> (exists [y:E]((inc x y) /\ 
(inc y a))).

Parameter union2 : E -> E -> E.
Axiom union2_ax : (x,y,a:E)(inc a (union2 x y)) <-> ((inc a x) \/ (inc a y)).

Parameter intersection : E -> E.
Axiom intersection_ax : (f,a:E)(exists [x:E](inc x f)) -> 
((inc a (intersection f)) <-> ((y:E)(inc y f) -> (inc a y))).

Parameter intersection2 : E -> E -> E.
Axiom intersection2_ax : (x,y,a:E)(inc a (intersection2 x y)) <-> ((inc a x) /\ (inc a y)).






Module Function.

Definition axioms :=  [f:E] 
(A (x:E)(inc x f) -> (pair (pr1 x) (pr2 x)) == x
   (x,y:E)(inc x f) -> (inc y f) -> (pr1 x) == (pr1  y) -> x == y
).

Definition domain [f:E] := (Image.create pr1 f).
Definition range [f:E] := (Image.create pr2 f).

Definition defined := [f,x:E]
(A (axioms f)
   (inc x (domain f))
).


Lemma sub_axioms : (f,g:E)(axioms g) -> (sub f g) -> (axioms f).
Intros. 
NewInduction H. 
Unfold sub in H0. 
UnfoldDeconj axioms.
Intros. 
Auto. 
Intros. 
Auto.
Save.

Lemma sub_domain : (f,g:E)(sub f g) -> (sub (domain f) (domain g)).
Intros. 
Unfold sub. 
Unfold domain. 
Unfold sub in H.
Intros. 
LetTac K := (Image.ex H0). 
NewInduction K. 
NewInduction H1.
Rewrite <- H2. 
Apply Image.incl. 
Auto.
Save.

Lemma sub_range : (f,g:E)(sub f g) -> (sub (range f) (range g)).
Intros. 
Unfold sub. 
Unfold range. 
Unfold sub in H. 
Intros.
LetTac K:= (Image.ex H0). 
NewInduction K. 
NewInduction H1.
Rewrite <- H2. 
Apply Image.incl. 
Auto.
Save.


Lemma defined_lem : (f,x:E)(axioms f) -> (defined f x) -> 
(inc (pair x (ev f x)) f).
Intros.
Unfold axioms in H.
Unfold defined in H0.
Expand.
Unfold domain in H1.
LetTac K := (Image.ex H1).
NewInduction K.
NewInduction H3.
Assert (exists [y:E](inc (pair x y) f)).
EApply exists_intro with (pr2 x0).
Rewrite <- H4.
Rewrite H.
Assumption.
Assumption.
LetTac K := (choose_pr H5).
Assumption.
Save.

Lemma lem1 : (f,x:E)(axioms f) -> (inc x f) -> x == (pair (pr1 x) (ev f (pr1 x))).
Intros.
Unfold axioms in H.
Expand.
LetTac z := (pr1 x).
Assert (exists [y:E](inc (pair z y) f)).
Apply exists_intro with (pr2 x).
Unfold z.
Rewrite H.
Assumption.
Assumption.
LetTac K := (choose_pr H2).
Assert (inc (pair z (ev f z)) f).
Assumption.
Apply H1.
Assumption.
Assumption.
Rewrite pr1_pair.
Trivial.
Save.


Lemma function_sub : (f,g:E)(axioms f) -> (axioms g) ->
((x:E)(defined f x) -> (defined g x)) ->
((x:E)(defined f x) -> (ev f x) == (ev g x)) ->
(sub f g).
Intros.
Unfold sub.
Intros.
LetTac K := (lem1 H H3).
Assert (defined f (pr1 x)).
UnfoldDeconj defined.
Assumption.
Unfold domain.
Apply Image.incl.
Assumption.
Assert (ev f (pr1 x)) == (ev g (pr1 x)).
Apply H2.
Assumption.
Rewrite K.
Assert (defined g (pr1 x)).
Apply H1.
Assumption.
Unfold defined in H6.
Expand.
Unfold domain in H7.
LetTac K1 := (Image.ex H7).
NewInduction K1.
NewInduction H8.
Unfold axioms in H0.
LetTac K1 := (lem1 H6 H8).
Rewrite H9 in K1.
Rewrite H5.
Rewrite <- K1.
Assumption.
Save.


Lemma extensionality : (f,g:E)(axioms f) -> (axioms g) ->
((x:E)(defined f x) -> (defined g x)) ->
((x:E)(defined g x) -> (defined f x)) ->
((x:E)(defined f x) -> (ev f x) == (ev g x)) ->
f == g.
Intros.
Apply extensionality.
Apply function_sub; Auto.
Apply function_sub; Auto.
Intros.
Symmetry.
Apply H3.
Apply H2.
Assumption.
Save.


Definition inverse_image := [f,a:E](domain (cut [x:E](inc (pr2 x) a) 
f)).

Lemma inverse_image_domain : (f,a:E)(sub (inverse_image f a) (domain 
f)).
Skip. Save.

Definition create [x:E;p:E -> E] := (Image.create [y:E](pair y (p y)) 
x).

Lemma create_axioms : (p:E-> E; x:E)(axioms (create x p)).
Skip. Save.

Lemma create_domain : (p:E -> E; x:E)(domain (create x p)) == x.
Skip. Save.

Lemma create_range : (p:E-> E; x:E)(range (create x p)) ==
(Image.create p x).
Skip. Save.

Lemma create_redo : (f:E)(axioms f) -> (create (domain f) [x:E](ev f x)) 
== f.
Skip. Save.

Definition compose [f,g:E] := (create (domain g) [y:E](ev f (ev g 
y))).

Lemma compose_axioms : (f,g:E)(axioms (compose f g)).
Skip. Save.

Lemma compose_domain : (f,g:E)(domain (compose f g)) ==
(inverse_image g (domain f)).
Skip. Save.

Lemma compose_ev : (x,f,g:E)(inc x (domain (compose f g))) ->
(ev (compose f g) x) == (ev f (ev g x)).
Skip. Save.

Definition identity [x:E] := (create x [y:E]y).

Lemma identity_domain : (x:E)(domain (identity x)) == x.
Skip.  Save.

Lemma identity_ev : (x,a:E)(inc x a) -> (ev (identity a) x) == x.
Skip. Save.

(*
Lemma create_univ : (univ, a:E; f:E -> E)(Universe.axioms univ) -> (inc 
a univ) ->
((x:E)(inc x a) -> (inc (f x) univ)) -> (inc (Function.create a f) 
univ).
Skip. Save.
*)

End Function.

Module Transformation.


Definition covers := [a,b:E; f:E -> E](x:E)(inc x b) -> (exists 
[y:E]((inc y a)/\(f y) == x)).
Definition injects := [a:E; f:E-> E](x,y:E)(inc x a) -> (inc y a) -> 
(f x) == (f y) -> x == y.


Definition inverse := [a:E; f:E -> E;y:E](choose [x:E]((inc x a)/\(f 
x) == y)).


Definition axioms := [a,b:E; f:E -> E](x:E)(inc x a) -> (inc (f x) b).

Lemma compose_axioms : (a,b,c:E;f,g: E->E)(axioms b c f) -> (axioms a b 
g) ->
(axioms a c [x:E](f (g x))).
Skip. Save.

Lemma identity_axioms : (a:E)(axioms a a [x:E]x).
Skip. Save.

Record surjective [a,b:E;f: E->E]:Prop :={
s1 : (axioms a b f);
s2 : (covers a b f)
}.

Record injective [a,b:E;f:E->E]:Prop := {
i1 : (axioms a b f);
i2 : (injects a f)
}.

Record bijective [a,b:E;f:E-> E]: Prop := {
bij_maps : (axioms a b f);
bij_surj : (surjective a b f);
bij_inj : (injective a b f)
}.


End Transformation.


Module Map.

Record axioms [a,b,f:E] : Prop := {
a1 : (Function.axioms f);
a2 : (Function.domain f) == a;
a3 : (sub (Function.range f) b)
}.

Lemma compose_axioms : (a,b,c,f,g: E)(axioms b c f) -> (axioms a b g) -> 

(axioms a c (Function.compose f g)).
Skip. Save.

Lemma identity_axioms : (a:E)(axioms a a (Function.identity a)).
Skip. Save.

Record surjective [a,b,f: E]:Prop :={
s1 : (axioms a b f);
s2 : (Transformation.covers a b (ev f))
}.

Record injective [a,b,f:E]:Prop := {
i1 : (axioms a b f);
i2 : (Transformation.injects a (ev f))
}.

Record bijective [a,b,f:E]: Prop := {
bij_maps : (axioms a b f);
bij_surj : (surjective a b f);
bij_inj : (injective a b f)
}.


End Map.



(*** the above stuff is old, it should be replaced with more of the 
following type notation ***)





Parameter C : Prop -> E.
(* currification *)

Parameter D : E -> (E -> E) -> E.
(* dependent record *)

Parameter J : E -> E -> E.
(* conjugation for obtaining an element of D *)

Parameter P : E -> E.
(* first projection for D *)

Parameter Q : E -> E.
(* second projection for D *)

Fixpoint Qr [n:nat] : E -> E :=
Cases n of
O => [x:E]x |
(S m) => [x:E](Q (Qr m x))
end.

Definition Pr := [n:nat; x: E](P (Qr n x)).

Parameter F : E -> (E -> E) -> E.
(* dependent function type *)

Parameter L : E -> (E -> E) -> E.
(* lambda for creating elements of F *)

Parameter V : E -> E -> E.
(* evaluation of functions *)



Module DJPC.

Axiom a1 : (u,a:E; b:E -> E)(inc u (D a b)) <->
(inc (P u) a) /\ (inc (Q u) (b (P u))) /\ (J (P u) (Q u)) == u.

Axiom a2 : (x,y:E)(P (J x y)) == x.

Axiom a3 : (x,y:E)(Q (J x y)) == y.

Axiom a4 : (x:E; p:Prop)(inc x (C p)) -> x ==  emptyset.
Axiom a5 : (p:Prop)p <-> (inc emptyset (C p)).

Axiom a6 : (x,y,z,w:E)x == z -> y == w -> (J x y) == (J z 
w).

Definition facts :=
(u,a:E; b:E -> E)(inc u (D a b)) -> (inc (P u) a) /\
(u,a:E; b:E -> E)(inc u (D a b)) -> (inc (Q u) (b (P u))) /\
(u,a:E; b:E -> E)(inc u (D a b)) -> (J (P u) (Q u)) == u /\
(x,y,a: E; b: E -> E)(inc x a) -> (inc y (b x)) -> (inc (J x y) (D a 
b))/\
(x:E; p:Prop)(inc x (C p)) -> p /\
(x:E; p:Prop)(inc x (C p)) -> x == emptyset/\
(x:E; p:Prop)p ->  (inc emptyset (C p)).


Lemma theory : facts.
Skip. Save.

End DJPC.

Recursive Tactic Definition CompareRecords :=
Match Context With
[|- (J ?1 ?2) == (J ?3 ?4)] ->
Apply DJPC.a6; [Idtac | CompareRecords]
|
[|- ? ] -> Idtac.

Recursive Tactic Definition Projector :=
Try (Unfold Pr);
Try (Unfold Qr);
First [Rewrite DJPC.a3 ; Projector | Rewrite DJPC.a2 | Idtac].

Module FLV.

Axiom a1 : (f,a:E; b: E -> E)(inc f (F a b)) <->
((x:E)(inc x a) -> (inc (V f x) (b x))) /\ (L a (V f)) == f.

Axiom a2 : (x,a:E; u:E -> E)(inc x a) -> (V (L a u) x) == (u x).

Axiom a3 : (a,b:E; u,v: E -> E) (a == b) -> ((x:E)(inc x a) -> (u x) 
== (v x)) ->
(L a u) == (L b v).

Definition facts :=
(f,a:E; b: E -> E)(inc f (F a b)) -> (L a (V f)) == f /\
(x,f,a:E; b: E -> E)(inc f (F a b)) ->(inc x a) -> (inc (V f x) (b x)) 
/\
(a:E; u,b: E -> E)((x:E)(inc x a) -> (inc (u x) (b x))) -> (inc (L a u) 
(F a b)).

Lemma theory : facts.
Skip. Save.

End FLV.





Module Quotient.

Parameter quotient : E -> (E -> E -> Prop) -> E.

(* (create a r) is the set of equivalence classes for a wrt the =
equivalence
relation on a generated by r. In particular the class of an element is 
determined
by choosing an element of (quotient a r) which contains that element *)

Parameter class : E -> E -> E.
(* syntax: (class x q) means the class of x in the quotient q, obtained
by looking for an element of q which contains x *)

Parameter rep : E -> E.
(* chooses a representative for the equivalence class, actually just a 
choice function *)

(**** we need to do the axioms for these ****)


Definition eq_reln := [a:E; r:E -> E -> Prop]
(A (x:E)(inc x a) -> (r x x)
(A (x,y:E)(inc x a) -> (inc y a) -> (r x y) -> (r y x)
   (x,y,z:E)(inc x a) -> (inc y a) -> (inc z a) -> (r x y) -> (r y z) -> (r x z)
)).

Definition equivalent := [a:E; r:E -> E -> Prop; x,y:E]
(A (inc x a)
(A (inc y a)
   (class x (quotient a r)) == (class y (quotient a r))
)).

Axiom lem1 : (a:E; r:E -> E -> Prop; x,y:E)(r x y) -> (equivalent a r x y).

Lemma lem2 : (a:E; r:E -> E -> Prop; x,y:E)(eq_reln a r) ->(equivalent a r x y) -> (r x y).
Skip. Save.


End Quotient.



Module Bounded.

Definition axioms := [p:E -> Prop](exists [x:E]((y:E)(p y) <-> (inc y 
x))).

Definition create := [p:E->Prop] (choose [x:E]((y:E)(p y) <-> (inc y 
x))).

Lemma lem1 : (p:E-> Prop; y:E)(axioms p) -> (inc y (create p)) -> (p y).
Skip. Save.

Lemma lem2 : (p:E -> Prop; y:E)(axioms p) -> (p y) -> (inc y (create 
p)).
Skip. Save.

End Bounded.

Module Cartesian.

Definition in_product := [a,b,u:E]
(A (is_pair u)
(A (inc (pr1 u) a)
   (inc (pr2 u) b)
)).

Definition create := [a,b:E](Bounded.create (in_product a b)).

Lemma bounded : (a,b:E)(Bounded.axioms (in_product a b)).
Skip. Save.

Lemma lem1 : (a,b,u:E)(inc u (create a b)) <-> (in_product a b u).
Skip. Save.

End Cartesian.


Module Order.

Definition less_than := [a,x,y:E](inc (pair x y) a).
Definition create := [u:E; lt : E -> E -> Prop](Z (Cartesian.create u u) [x:E](lt (pr1 x) (pr2 x))).
Definition like := [u,o:E](create u (less_than o)) == o.

Lemma lem_1 : (u:E; lt: E -> E -> Prop; x,y:E)(inc x u) -> (inc y u) ->
((less_than (create u lt) x y) <-> (lt x y)).
Skip. Save.

Definition property := [u:E; lt:E -> E -> Prop]
(A (x:E)(inc x u) -> (lt x x) -> False
(A (x,y,z:E)(inc x u) -> (inc y u) -> (inc z u) -> (lt x y) -> (lt y z) 
-> (lt x z)
True)).



Lemma lem1 : (u,v:E; lt: E -> E -> Prop)(sub v u) -> (property u lt) -> (property v lt).
Skip. Save.



Definition linear := [u:E; lt:E -> E-> Prop]
(x,y:E)(inc x u) -> (inc y u) -> ((lt x y) \/ (lt y x) \/ (x == y)).

Definition leq := [lt : E -> E -> Prop; x,y:E](lt x y)\/(x == y).

Lemma lem2_1 : (u:E; lt:E ->E-> Prop; x,y:E)(property u lt) -> (linear u 
lt) ->
(inc x u) -> (inc y u) -> (lt x y) \/ (leq lt y x).
Skip. Save.

Lemma lem2_2 : (u,v:E; lt: E -> E -> Prop)(sub v u) -> (linear u lt) -> (linear v lt).
Skip. Save.

Definition bounds_above := [u,v:E; lt : E -> E -> Prop; x:E]
(A (inc x u)
   (y:E)(inc y v) -> (leq lt y x)
).
Definition upper_bound := [u,v:E; lt: E -> E -> Prop](choose [x:E](bounds_above u v lt x)).
Definition admits_upper_bound := [u,v:E; lt : E -> E -> Prop](bounds_above u v lt (upper_bound u v lt)).

Definition is_maximal := [u:E; lt : E -> E -> Prop; x:E]
(A (inc x u)
   (y:E)(inc y u) -> (leq lt x y) -> x == y
).

Definition bounds_below := [u,v:E; lt : E -> E -> Prop; x:E]
(A (inc x u)
   (y:E)(inc y v) -> (leq lt x y)
).
Definition lower_bound := [u,v:E; lt: E -> E -> Prop](choose [x:E](bounds_below u v lt x)).
Definition admits_lower_bound := [u,v:E; lt : E -> E -> Prop](bounds_below u v lt (lower_bound u v lt)).

Definition is_minimal := [u:E; lt : E -> E -> Prop; x:E]
(A (inc x u)
   (y:E)(inc y u) -> (leq lt y x) -> x == y
).



Definition well_ordered := [u:E; lt : E -> E-> Prop]
(A (Order.property u lt)
(A (Order.linear u lt)
 (v:E)(sub v u) -> (admits_lower_bound v v lt)
)).




Module Zorn.

Definition hypothesis := [u:E; lt: E -> E -> Prop]
(A (Order.property u lt)
   (v:E)(sub v u) -> (Order.linear v lt) ->(admits_upper_bound u v lt)
).

Definition succ_pr := [u,v:E; lt: E -> E -> Prop; x:E]
(A (bounds_above u v lt x)
   (not (inc x v))
).


Definition succ := [u,v:E; lt: E -> E -> Prop](choose [x:E](succ_pr u v lt x)).
Definition is_succ := [u,v:E; lt: E -> E -> Prop; x:E](A (succ_pr u v lt x) (succ u v lt) == x).

Definition admissible_chain := [u,v:E; lt: E -> E -> Prop]
(A (Order.property u lt)
(A (sub v u)
(A (well_ordered v lt)
   (x:E)(inc x v) -> (is_succ u (Z v [y:E](lt y x)) lt x)
))).

Lemma  comparison : (u,v,w:E; lt: E -> E -> Prop)(admissible_chain u v lt) ->
(admissible_chain u w lt) -> ((sub v w) \/ (sub w v)).
Skip. Save.

Definition the_chain := [u:E; lt : E -> E -> Prop]
(Z u [x:E](exists [v:E](A (inc x v) (admissible_chain u v lt)))).

Lemma the_chain_admissible : (u:E; lt : E -> E -> Prop)
((v:E)(sub v u) -> (Order.linear v lt) -> (exists [x:E](succ_pr u v lt x))) ->
(admissible_chain u (the_chain u lt) lt).
Skip. Save. 
     
Lemma zorn's_lemma : (u:E; lt : E -> E -> Prop)(hypothesis u lt) -> (exists [x:E](is_maximal u lt x)).
Skip. Save.
     
Lemma wo_exists : (u:E)(exists [o:E](A (like u o) (well_ordered u (less_than o)))).
Skip. Save.

Definition well_ordering := [u:E](choose [o:E](A (like u o) (well_ordered u (less_than o)))).

Lemma lem2 : (u:E)(well_ordered u (less_than (well_ordering u))).
Skip. Save.


End Zorn.


End Order.

Module Ordinal.

Definition axioms := [u:E]
(A (x:E)(inc x u) -> (sub x u)
   (Order.well_ordered u [x,y:E](inc x y))
).



End Ordinal.

Module Natural.

Parameter set : E.

Axiom a1 : (Ordinal.axioms set).

Parameter create : nat -> E.
Axiom a2 : (i:nat)(inc (create i) set).
Axiom a3 : (i,j:nat)(Peano.lt i j) -> (inc (create i) (create j)).
Axiom a4 : (i,j:nat)(create i) == (create j) -> i == j.
Axiom a5 : (x:E)(inc x set) -> (exT ? [i:nat](create i)== x).
Axiom a6 : (i,j:nat)(inc (create i) (create j)) -> (Peano.lt i j).

Definition le := [x,y:E](A (sub x y) (A (inc x set) (inc y set))).
Definition lt := [x,y:E](A (inc x y) (A (inc x set) (inc y set))).

Lemma lem1 : (Order.property set lt).
Skip. Save.

Lemma lem2 : (x,y:E)(inc x set)-> (inc y set) -> 
(lt x y) \/ (lt y x) \/ x == y.
Skip. Save.

(*** ??? le is not quite the same as (Order.leq lt) because the latter includes any
two pairs of equal sets ??? ***)

Parameter plus : E -> E -> E.
Parameter minus : E -> E -> E.
Parameter times : E -> E -> E.

Definition zero := (create O).

Axiom p1 : (i,j:nat)(plus (create i) (create j)) == (create (Peano.plus i j)).
(*** ??? look for the minus and times operations ???
Axiom m1 : (i,j:nat)(minus (create i) (create j)) == (create (Peano.minus i j)).
Axiom t1 : (i,j:nat)(times (create i) (create j)) == (create (Peano.times i j)).
*****)

(*** other things for these ???? ****)

End Natural.

Module List.

Definition domain := [n:E](Z Natural.set [i:E](Natural.lt i n)).

Lemma lem1 : (n,i:E)(inc i (domain n)) -> (inc n Natural.set).
Skip. Save.

Definition set := [n,a:E](Z (F (domain n) [i:E]a) [l:E](inc n Natural.set)).
(** note that the above means that List.set is nonempty iff n is in Natural.set ****)

Definition create := [n:E; f:E -> E](L (domain n) f).

Lemma lem2 : (n,a:E; f:E -> E)((i:E)(inc i (domain n)) -> (inc (f i) a)) -> (inc (create n f) (set n a)).
Skip. Save.

Lemma lem3 : (n,i:E; f:E -> E)(inc i (domain n)) -> (V (create n f) i) == (f i).
Skip. Save.

(**** ??? do head and tail removes, also cons's or maybe singleton lists, empty list, concatenation
etc ****)

Definition map := [f:E -> E; l:E](L (Function.domain l) [x:E](f (V l x))).

End List.

Module Integer.


Definition axioms := [i:E]
(inc i Natural.set) \/
(A (is_pair i)
(A (pr2 i) == Natural.set
(A (inc (pr1 i) Natural.set)
   (not (pr1 i) == (Natural.zero))
))).

Definition set := (Bounded.create axioms).

Lemma natural_sub : (sub Natural.set Integer.set).
Skip. Save.


Syntactic Definition Zar := Coq.ZArith.fast_integer.Z.
Parameter of_Z : Zar -> E.
Definition zero := Natural.zero.

(** the following dont work, we need to find the function which
corresponds to lt in Coq.ZArith.fast_integer ****
Definition lt := [i,j:E]
(A (axioms i)
(A (axioms j)
   (exists [k:Zar](exists [l:Zar]
   (A (of_Z k) == i
   (A (of_Z l) == j
      (ZArith.lt k l)
   ))))
)). 

Definition le := [i,j:E]
(A (axioms i)
(A (axioms j)
   (exists [k:ZArith.Z](exists [l:ZArith.Z]
   (A (of_Z k) == i
   (A (of_Z l) == j
      (ZArith.le k l)
   ))))
)). 
****)
Import Coq.ZArith.fast_integer.

Parameter plus : E -> E -> E.
Parameter minus : E -> E -> E.
Parameter times : E -> E -> E.



Axiom plus_Z : (i,j:Zar)(plus (of_Z i) (of_Z j)) == (of_Z (Zplus i j)).
Axiom minus_Z : (i,j:Zar)(minus (of_Z i) (of_Z j)) == (of_Z (Zminus i j)).
Axiom times_Z : (i,j:Zar)(times (of_Z i) (of_Z j)) == (of_Z (Zmult i j)).

Definition one := (of_Z `1`).

Definition succ := [x:E](plus x one).

End Integer.



Module Categorical.

Section I.
Variables ob : E -> Prop; mor : E -> Prop; source,target : E->E; comp : E->E -> E; id : E->E.

Definition composable := [u,v:E]
(A (mor u)
(A (mor v)
   (source u) == (target v)
)).

Definition hom := [a,b,f:E]
(A (mor f)
(A (source f) == a
   (target f) == b
)).

Definition axioms := 
(A (u:E)(mor u) -> (ob (source u))
(A (u:E)(mor u) -> (ob (target u))
(A (x:E)(ob x) -> (mor (id x))
(A (x:E)(ob x) -> (source (id x)) == x
(A (x:E)(ob x) -> (target (id x)) == x
(A (u,v:E)(composable u v) -> (hom (source v) (target u) (comp u v))
(A (u:E)(mor u) -> (comp (id (target u)) u) == u
(A (u:E)(mor u) -> (comp u (id (target u))) == u
   (u,v,w:E)(composable u v) -> (composable v w) ->
     (comp (comp u v) w) == (comp u (comp v w))
)))))))).

Definition are_inverses := [f,g:E]
(A axioms
(A (mor f)
(A (mor g)
(A (source f) == (target g)
(A (target f) == (source g)
(A (comp f g) == (id (target f))
   (comp g f) == (id (target g))
)))))).

Definition inverse := [f:E]
(choose (are_inverses f)).

Lemma lem1 : (f:E)(exists [g:E](are_inverses f g)) -> (are_inverses f (inverse f)).
Skip. Save. 


Definition isom := [a,b,f:E]
(A axioms
(A (hom a b f)
   (are_inverses f (inverse f))
)).

Definition monomorphism := [f:E]
(A axioms
(A (mor f)
   (x,g,h:E)(hom x (source f) g) -> (hom x (source f) h) -> (comp f g) == (comp f h) -> g == h
)). 

Definition epimorphism := [f:E]
(A axioms
(A (mor f)
   (x,g,h:E)(hom (target f) x g) -> (hom (target f) x h) -> (comp g f) == (comp h f) -> g == h
)).

Definition is_initial := [a:E]
(A axioms
(A (ob a)
   (b:E)(ob b) -> (exists_unique [f:E](hom a b f))
)).

Definition is_coinitial := [b:E]
(A axioms
(A (ob b)
   (a:E)(ob a) -> (exists_unique [f:E](hom a b f))
)).

Definition init := (choose (is_initial)).

(*** we choose coinit to be equal to init if possible ***)
Definition coinit := (choose [b:E]
(A (is_coinitial b)
   (is_coinitial init) -> b == init
)).

Definition has_initial := (exists [a:E](is_initial a)).
Definition has_coinitial := (exists [a:E](is_coinitial a)).

Lemma init_lem1 : has_initial -> (is_initial init).
Skip. Save.
Lemma coinit_lem1 : has_coinitial -> (is_coinitial coinit).
Skip. Save.

Definition pointed := (exists [a:E](A (is_initial a) (is_coinitial a))).

Lemma pointed_lem1 : pointed -> 
(A (is_initial init) 
(A (is_coinitial coinit)
   init == coinit
)).
Skip. Save.

Definition init_mor := [x:E](choose [f:E](hom init x f)).
Definition coinit_mor := [x:E](choose [f:E](hom x coinit f)).

Definition zero := [x,y:E](comp (init_mor y) (coinit_mor x)).
Lemma lem4 : (x,y:E)pointed -> (hom x y (zero x y)).
Skip. Save.


Definition is_product := [a,b,u,v:E]
(A axioms
(A (mor u)
(A (mor v)
(A (target u) == a
(A (target v) == b
(A (source u) == (source v)
   (y,z:E)(source y) == (source z) -> (target y) == a ->(target z) == b ->
      (exists_unique [w:E]
      (A (source w) == (source y)
      (A (target w) == (source u)
      (A (comp u w) == y
         (comp v w) == z))))
)))))).

Definition pr1 := [a,b:E](choose [u:E](exists [v:E](is_product a b u v))).
Definition pr2 := [a,b:E](choose [v:E](is_product a b (pr1 a b) v)).
Definition product := [a,b:E](source (pr1 a b)).
Definition product_exists := [a,b:E](exists [u:E](exists [v:E](is_product a b u v))).
Definition product_univ := [y,z:E](choose [w:E]
(A (hom (source y) (product (target y) (target z)) w)
(A (comp (pr1 (target y) (target z)) w) == y
   (comp (pr2 (target y) (target z)) w) == z
))).

Lemma lem2 : (a,b:E)(product_exists a b) -> 
(A (is_product a b (pr1 a b) (pr2 a b))
(A (hom (product a b) a (pr1 a b))
(A (hom (product a b) b (pr2 a b))
(A (c,y,z:E)(hom c a y) -> (hom c b z) ->  
   (A (hom c (product a b) (product_univ y z))
   (A (comp (pr1 a b) (product_univ y z)) == y
      (comp (pr2 a b) (product_univ y z)) == z
   ))
  (c,w:E)(hom c (product a b) w) -> (product_univ (comp (pr1 a b) w) (comp (pr2 a b) w)) == w
)))). 
Skip. Save.



Definition prod_comm := [a,b:E]
(product_univ (pr2 a b) (pr1 a b)).

Lemma product_comm : (a,b:E)(ob a) -> (ob b) -> (product_exists a b) ->
(A (product_exists b a)
(A (isom (product a b) (product b a) (prod_comm a b))
   (are_inverses (prod_comm a b) (prod_comm b a))
)).
Skip. Save.

(*** prod_assoc1 goes from (a x b) x c to a x (b x c) ****)
Definition prod_assoc1 := [a,b,c:E]
(product_univ (comp (pr1 a b) (pr1 (product a b) c))
(product_univ (comp (pr2 a b) (pr1 (product a b) c))
              (pr2 (product a b) c)
)).

(*** prod_assoc2 goes from a x (b x c) to (a x b) x c ****)
Definition prod_assoc2 := [a,b,c:E]
(product_univ 
  (product_univ (pr1 a (product b c))
                (comp (pr1 b c) (pr2 a (product b c)))
  )
  (comp (pr2 b c) (pr2 a (product b c)))
).

Lemma product_assoc : (a,b,c:E)(ob a) -> (ob b) -> (ob c) ->
(product_exists a b) -> (product_exists b c) -> (product_exists a (product b c)) ->
(product_exists (product a b) c) ->
(A (isom (product (product a b) c) (product a (product b c)) (prod_assoc1 a b c))
(A (isom (product a (product b c)) (product (product a b) c) (prod_assoc2 a b c))
   (are_inverses (prod_assoc1 a b c) (prod_assoc2 a b c))
)).
Skip. Save.


Definition is_coproduct := [a,b,u,v:E]
(A axioms
(A (mor u)
(A (mor v)
(A (source u) == a
(A (source v) == b
(A (target u) == (target v)
   (y,z:E)(target y) == (target z) -> (source y) == a ->(source z) == b ->
      (exists_unique [w:E]
      (A (target w) == (target y)
      (A (source w) == (target u)
      (A (comp w u) == y
         (comp w v) == z))))
)))))).

Definition copr1 := [a,b:E](choose [u:E](exists [v:E](is_coproduct a b u v))).
Definition copr2 := [a,b:E](choose [v:E](is_coproduct a b (copr1 a b) v)).
Definition coproduct := [a,b:E](target (pr1 a b)).
Definition coproduct_exists := [a,b:E](exists [u:E](exists [v:E]
(is_coproduct a b u v))).
Definition coproduct_univ := [y,z:E](choose [w:E]
(A (hom (coproduct (source y) (source z)) (target y) w)
(A (comp w (copr1 (target y) (target z))) == y
   (comp w (copr2 (target y) (target z))) == z
))).

Lemma lem3 : (a,b:E)(coproduct_exists a b) -> 
(A (is_coproduct a b (copr1 a b) (copr2 a b))
(A (hom a (coproduct a b) (copr1 a b))
(A (hom b (coproduct a b) (copr2 a b))
(A (c,y,z:E)(hom a c y) -> (hom b c z) ->  
   (A (hom (coproduct a b) c (coproduct_univ y z))
   (A (comp (coproduct_univ y z) (copr1 a b)) == y
      (comp (coproduct_univ y z) (copr2 a b)) == z
   ))
  (c,w:E)(hom (coproduct a b) c w) -> (coproduct_univ (comp w (copr1 a b)) (comp w (copr2 a b))) == w
)))). 
Skip. Save.



Definition coprod_comm := [a,b:E]
(coproduct_univ (copr2 a b) (copr1 a b)).

Lemma coproduct_comm : (a,b:E)(ob a) -> (ob b) -> (coproduct_exists a b) ->
(A (coproduct_exists b a)
(A (isom (coproduct a b) (coproduct b a) (coprod_comm a b))
   (are_inverses (coprod_comm a b) (coprod_comm b a))
)).
Skip. Save.

Definition coprod_assoc1 := [a,b,c:E]
(coproduct_univ (comp  (copr1 (coproduct a b) c) (copr1 a b))
(coproduct_univ (comp  (copr1 (coproduct a b) c) (copr2 a b))
              (copr2 (coproduct a b) c)
)).

Definition coprod_assoc2 := [a,b,c:E]
(coproduct_univ 
  (coproduct_univ (copr1 a (coproduct b c))
                (comp (copr2 a (coproduct b c)) (copr1 b c))
  )
  (comp (copr2 a (coproduct b c)) (copr2 b c))
).

(*** the following may be somewhat wrong---just copied product_assoc and changed some things ****)
Lemma coproduct_assoc : (a,b,c:E)(ob a) -> (ob b) -> (ob c) ->
(coproduct_exists a b) -> (coproduct_exists b c) -> (coproduct_exists a (coproduct b c)) ->
(coproduct_exists (coproduct a b) c) ->
(A (isom (coproduct (coproduct a b) c) (coproduct a (coproduct b c)) (coprod_assoc1 a b c))
(A (isom (coproduct a (coproduct b c)) (coproduct (coproduct a b) c) (coprod_assoc2 a b c))
   (are_inverses (coprod_assoc1 a b c) (coprod_assoc2 a b c))
)).
Skip. Save.


(*** next we do stuff in the pointed case ***)

Lemma lem3_1_1 : (a,b,c,f:E)pointed -> (ob a) -> (hom b c f) -> 
(comp f (zero a b)) == (zero a c).
Skip. Save.
Lemma lem3_1_2 : (a,b,c,f:E)pointed -> (ob c) -> (hom a b f) -> 
(comp (zero b c) f) == (zero a c).
Skip. Save.


Definition ia1 := [a,b:E](coproduct_univ (id a) (zero a b)).
Definition ia2 := [a,b:E](coproduct_univ (zero b a) (id b)).

Lemma lem3_1 : (a,b:E)pointed -> (product_exists a b) -> 
(A (hom a (product a b) (ia1 a b))
   (hom b (product a b) (ia2 a b))
).
Skip. Save.

Definition coproduct_to_product := [a,b:E]
(coproduct_univ (ia1 a b) (ia2 a b)).

Definition coproduct_to_product_2 := [a,b:E]
(product_univ (coproduct_univ (id a) (zero a b)) (coproduct_univ (zero b a) (id b))).

Lemma lem3_2 : (a,b:E)(product_exists a b) -> (coproduct_exists a b) -> 
(coproduct_to_product a b) == (coproduct_to_product_2 a b).
(** because the maps a to a, a to b, b to a and b to b are the same in both cases ***)
Skip. Save.

Definition semiadditive := 
(A axioms
(A pointed
   (a,b:E)(ob a) -> (ob b) -> 
   (A (product_exists a b)
   (A (coproduct_exists a b)
      (isom (coproduct a b) (product a b) (coproduct_to_product a b)
   )))
)).

Definition product_to_coproduct := [a,b:E](inverse (coproduct_to_product a b)).
Lemma lem4_0 : (a,b:E)semiadditive -> (ob a) -> (ob b) ->
(A (hom (product a b) (coproduct a b) (product_to_coproduct a b))
(A (comp (product_to_coproduct a b) (coproduct_to_product a b)) == (id (coproduct a b))
   (comp (coproduct_to_product a b) (product_to_coproduct a b)) == (id (product a b))
)).
Skip. Save.

Lemma lem4_1 : (a,b,c,f,g:E)semiadditive -> (ob a) -> (ob b) ->
(hom (product a b) c f) -> (hom (product a b) c g) ->
(comp f (ia1 a b)) == (comp g (ia1 a b)) ->
(comp f (ia2 a b)) == (comp g (ia2 a b)) ->
f == g.
Skip. Save.

Definition diagonal := [a:E](product_univ (id a) (id a)).
Definition codiagonal := [a:E](comp (product_to_coproduct a a) (coproduct_univ (id a) (id a))).

Lemma diagonals : (a:E)semiadditive -> 
(A (hom a (product a a) (diagonal a))
(A (hom (product a a) a (codiagonal a))
(A (comp (codiagonal a) (ia1 a a)) == (id a)
(A (comp (codiagonal a) (ia2 a a)) == (id a)
(A (comp (pr1 a a) (diagonal a)) == (id a)
   (comp (pr2 a a) (diagonal a)) == (id a)
))))).
Skip. Save.

Definition plus := [f,g:E](comp (codiagonal (target f)) (product_univ f g)).

Lemma lem5 : (a,b,f,g:E)semiadditive -> (hom a b f) -> (hom a b g) -> (hom a b (plus f g)).
Skip. Save.

Lemma lem6_1 : (a,b,f,g,h:E)semiadditive -> (hom a b f) -> (hom a b g) -> (source h) == b ->
(comp h (plus f g)) == (plus (comp h f) (comp h g)).
Skip. Save.

Lemma lem6_2 : (a,b,f,g,h:E)semiadditive -> (hom a b f) -> (hom a b g) -> (target h) == a ->
(comp (plus f g) h) == (plus (comp f h) (comp g h)).
Skip. Save.

Lemma lem6_3 : (a,b,f:E)semiadditive -> (hom a b f) -> (plus f (zero a b)) == f.
Skip. Save.

Lemma lem6_4 : (a,b,f,g:E)semiadditive -> (hom a b f) -> (hom a b g) -> (plus f g) == (plus g f).
Skip. Save.

Lemma lem6_5_1 : (a,b,f,g,h:E)semiadditive -> (hom a b f) -> (hom a b g) -> (hom a b h) ->
(plus (plus f g) h) == 
(comp (codiagonal b)
(comp (product_univ (codiagonal b) (id b))
      (product_univ (product_univ f g) h)
)).
Skip. Save.

Lemma lem6_5_2 : (a,b,f,g,h:E)semiadditive -> (hom a b f) -> (hom a b g) -> (hom a b h) ->
(plus f (plus g h)) == 
(comp (codiagonal b)
(comp (product_univ (id b) (codiagonal b))
      (product_univ f (product_univ g h))
)).
Skip. Save. 

Lemma lem6_5_3 : (a,b,f,g,h:E)semiadditive -> (hom a b f) -> (hom a b g) -> (hom a b h) ->
(comp (prod_assoc1 b b b) (product_univ (product_univ f g) h)) == (product_univ f (product_univ g h)).
Skip. Save.

Lemma lem6_5_4 : (b:E)semiadditive -> (ob b) ->
(comp (codiagonal b)
(comp (product_univ (id b) (codiagonal b))
      (prod_assoc1 b b b)
)) ==
(comp (codiagonal b)
      (product_univ (codiagonal b) (id b))
).
(*** use the criterion of lem4_1 (twice) for comparing maps (b x b) x b to b ***)
Skip. Save.

Lemma lem6_5_5 : (a,b,f,g,h:E)semiadditive -> (hom a b f) -> (hom a b g) -> (hom a b h) ->
(plus (plus f g) h) == (plus f (plus g h)).
Skip. Save.

(*********** now we have obtained an operation which is associative, commutative and unitary.
However it is not necessarily a group; example: the category of free N-modules (N=the naturals)
i.e. with objects N^k where the set of maps from N^k to N^l is the space of k x l matrices with
positive integer coefficients. This forms a semiadditive category but plus doesn't admit an inverse.
It is also an example of a category in which monomorphism + epimorphism doesn't necessarily imply 
isomorphism.  However it doesn't seem to be the case that this last condition would guarantee 
additivity (i.e. existence of an inverse for plus). **********************************)

Definition additive := 
(A semiadditive
   (a,b,f:E)(hom a b f) -> (exists [g:E](A (hom a b g) (plus f g) == (zero a b)))
).

Definition neg := [f:E](choose [g:E]
(A (source g) == (source f)
(A (target g) == (target f)
   (plus f g) == (zero (source f) (target f))
))).

Definition minus := [f,g:E](plus f (neg g)).

(****************** end of additive stuff ******************)

(****************** kernels and cokernels ******************)

Definition is_kernel := [f,g:E]
(A pointed 
(A (composable f g)
(A (monomorphism g)
(A (comp f g) == (zero (source g) (target f))
   (h:E)(composable f h) -> (comp f h) == (zero (source h) (target f)) ->
   (exists [u:E]
   (A (hom (source h) (source g) u)
      (comp g u) == h 
   ))
)))).

Definition kernel_mor := [f:E](choose [g:E]
(A (is_kernel f g)
   (is_initial (source g)) -> (source g) == init
)).
(*** the latter condition is put so that we can more easily speak of the case when the kernel is zero **)

Definition kernel := [f:E](source (kernel_mor f)). 
Definition kernel_exists := [f:E](is_kernel f (kernel_mor f)).
Definition has_kernels := (f:E)(mor f) -> (kernel_exists f).
Definition kernel_fact := [f,h:E](choose [u:E]
  (A (hom (source h) (kernel f) u)
     (comp (kernel_mor f) u) == h
  )).



Lemma lem7_1 : (f:E)(exists [g:E](is_kernel f g)) -> (kernel_exists f).
Skip. Save.

Lemma lem7_2 : (f:E)(kernel_exists f) -> ((kernel f) == init <-> (monomorphism f)).
Skip. Save. 

Lemma lem7_3 : (f,h:E)(kernel_exists f) -> (composable f h) -> (comp f h) == (zero (source h) (target f)) ->
(A (hom (source h) (kernel f) (kernel_fact f h))
(A (comp (kernel_mor f) (kernel_fact f h)) == h
   (u:E)(hom (source h) (kernel f) u) -> (comp (kernel_mor f) u) == h -> u == (kernel_fact f h)
)).
Skip. Save.





Definition is_cokernel := [f,g:E]
(A pointed
(A (composable g f)
(A (epimorphism g)
(A (comp g f) == (zero (source f) (target g))
   (h:E)(composable h f) -> (comp h f) == (zero (source f) (target h)) ->
   (exists [u:E]
   (A (hom (target g) (target h) u)
      (comp u g) == h 
   ))
)))).

Definition cokernel_mor := [f:E](choose [g:E]
(A (is_cokernel f g)
   (is_coinitial (target g)) -> (target g) == init
)).


Definition cokernel := [f:E](target (cokernel_mor f)).
Definition cokernel_exists := [f:E](is_cokernel f (cokernel_mor f)).
Definition has_cokernels := (f:E)(mor f) -> (cokernel_exists f).
Definition cokernel_fact := [f,h:E](choose [u:E]
  (A (hom (cokernel f) (target h) u)
     (comp u (cokernel_mor f)) == h
  )).


Lemma lem8_1 : (f:E)(exists [g:E](is_cokernel f g)) -> (cokernel_exists f).
Skip. Save.

Lemma lem8_2 : (f:E)(cokernel_exists f) -> ((cokernel f) == coinit <-> (epimorphism f)).
Skip. Save. 

Lemma lem8_3 : (f,h:E)(cokernel_exists f) -> (composable h f) -> (comp h f) == (zero (source f) (target h)) ->
(A (hom (cokernel f) (target h) (cokernel_fact f h))
(A (comp (cokernel_fact f h) (cokernel_mor f)) == h
   (u:E)(hom (cokernel f) (target h) u) -> (comp u (cokernel_mor f)) == h -> u == (cokernel_fact f h)
)).
Skip. Save.



Definition image_mor := [f:E](kernel_mor (cokernel_mor f)).
Definition image := [f:E](source (image_mor f)).
Definition image_comor := [f:E](kernel_fact (cokernel_mor f) f).


Lemma lem9_1 : (f:E)(cokernel_exists f) -> (kernel_exists (cokernel_mor f)) -> 
(A (hom (image f) (target f) (image_mor f))
(A (hom (source f) (image f) (image_comor f))
(A (comp (image_mor f) (image_comor f)) == f
   (monomorphism (image_mor f))
))).
Skip. Save.

Definition coimage_mor := [f:E](cokernel_mor (kernel_mor f)).
Definition coimage := [f:E](target (coimage_mor f)).
Definition coimage_comor := [f:E](cokernel_fact (kernel_mor f) f).


Lemma lem9_2 : (f:E)(kernel_exists f) -> (cokernel_exists (kernel_mor f)) -> 
(A (hom (source f) (image f) (coimage_mor f))
(A (hom (image f) (target f) (coimage_comor f))
(A (comp (coimage_comor f) (coimage_mor f)) == f
   (epimorphism (image_mor f))
))).
Skip. Save.

Definition coimage_to_image := [f:E](cokernel_fact (kernel_mor f) (image_comor f)).
Definition coimage_to_image_2 := [f:E](kernel_fact (cokernel_mor f) (coimage_comor f)).

Lemma lem9_3 :  (f:E)(kernel_exists f) -> (cokernel_exists (kernel_mor f)) -> 
(cokernel_exists f) -> (kernel_exists (cokernel_mor f)) -> 
(A (hom (coimage f) (image f) (coimage_to_image f))
   (coimage_to_image_2 f) == (coimage_to_image f)
).
Skip. Save.

Definition abelian := 
(A additive
(A has_kernels
(A has_cokernels
   (f:E)(isom (coimage f) (image f) (coimage_to_image f))
))).

Definition exact_at := [f,g:E]
(A abelian
(A (composable f g)
(A (comp f g) == (zero (source g) (target f))
   (is_kernel f (image_mor g))
))).

Lemma lem10_1 : (f,g:E)(exact_at f g) -> 
(A (is_kernel f (coimage_comor g))
(A (is_cokernel g (image_comor f))
   (is_cokernel g (coimage_mor f))
)).
Skip. Save.

Definition left_exact := [f,g:E]
(A (exact_at f g)
   (kernel g) == init
).

Definition right_exact := [f,g:E]
(A (exact_at f g)
   (cokernel g) == coinit
).

Definition short_exact := [f,g:E]
(A (left_exact f g)
   (right_exact f g)
).

(**** next do resolutions, long exact sequences etc; concentrate on the case of injective resolutions first ***)

Definition is_complex := [a:E]
(A abelian
(A a == (L Integer.set [i:E](V a i))
(A (i:E)(inc i Integer.set) -> (mor (V a i))
(A (i:E)(inc i Integer.set) -> (composable (V a (Integer.succ i)) (V a i))
   (i:E)(inc i Integer.set) -> 
   (comp (V a (Integer.succ i)) (V a i)) == (zero (source (V a i)) (target (V a (Integer.succ i))))
)))).





End I.

End Categorical.


Module Morphism.

(* here morphisms are just functions between the sets *)

Definition Source := (index (11)).
Definition Target := (index (12)).
Definition Funct := (index (13)).

Definition source := [f:E](get Source f).
Definition target := [f:E](get Target f).
Definition ev := [f,x:E](V (get Funct f) x).


Definition axioms := [f:E] 
(Transformation.axioms (source f) (target f) (ev f)).

Definition create := [a,b:E; f:E -> E]
(set Source a
(set Target b
(set Funct (L a [x:E](f x))
emptyset))).

Definition strong_axioms := [f:E]
(A (axioms f)
   (create (source f) (target f) (ev f)) == f
).

Definition collection := [a,b:E]
(Bounded.create [u:E]
(A (strong_axioms u)
(A (source u) == a
   (target u) == b
))).

Definition comp := [u,v:E](create (source v) (target u) [x:E](ev u (ev v x))).
Definition id := [x:E](create x x [y:E]y).

Definition composable := (Categorical.composable axioms source target).


Lemma categorical : (Categorical.axioms [x:E]True axioms source target comp id).
Skip. Save.


End Morphism.

Definition Underlying := (index (1)).
Definition U := [x:E](get Underlying x).
Definition underlying := U.


Module Umorphism.

(* here the morphisms are functions between the underlying sets *)

Definition Source := (index (11)).
Definition Target := (index (12)).
Definition Funct := (index (13)).

Definition source := [f:E](get Source f).
Definition target := [f:E](get Target f).
Definition ev := [f,x:E](V (get Funct f) x).


Definition axioms := [f:E] 
(Transformation.axioms (U (source f)) (U (target f)) (ev f)).

Definition create := [a,b:E; f: E -> E]
(set Source a
(set Target b
(set Funct (L (U a) [x:E](f x))
emptyset))).

Definition strong_axioms := [f:E]
(A (axioms f)
   (create (source f) (target f) (ev f)) == f
).

Definition collection := [a,b:E]
(Bounded.create [u:E]
(A (strong_axioms u)
(A (source u) == a
   (target u) == b
))).

Definition comp := [u,v:E](create (source v) (target u) [x:E](ev u (ev v x))).
Definition id := [x:E](create x x [y:E]y).

Definition composable := (Categorical.composable axioms source target).

Lemma categorical : (Categorical.axioms [x:E]True axioms source target comp id).
Skip. Save.



End Umorphism.

Module Structure.

Definition source := Umorphism.source.
Definition target := Umorphism.target.
Definition comp := Umorphism.comp.
Definition id := Umorphism.id.

Definition composable := [mor : E -> Prop](Categorical.composable mor source target).

Definition axioms := [ob : E -> Prop; mor : E -> Prop]
(A (u:E)(mor u) -> (Umorphism.strong_axioms u)
   (Categorical.axioms ob mor source target comp id)
).



End Structure.


Module Magma.


Definition property := [a:E; op:E2]
(x,y:E)(inc x a) -> (inc y a) -> (inc (op x y) a).



Definition is_associative := [a:E; op:E2]
(x,y,z:E)(inc x a) -> (inc y a) -> (inc z a) -> 
(op (op x y) z) == (op x (op y z)).

Definition is_commutative := [a:E; op:E2]
(x,y:E)(inc x a) -> (inc y a) -> 
(op x y) == (op y x).

Definition is_left_unit := [a:E; op:E2; u:E]
(A (inc u a)
   (x:E)(inc x a) -> (op u x) == x
).

Definition is_right_unit := [a:E; op:E2; u:E]
(A (inc u a)
   (x:E)(inc x a) -> (op x u) == x
).

Definition is_unit := [a;op:E2; u:E](A (is_left_unit a op u) (is_right_unit a op u)).

Definition unit := [a:E; op:E2](choose (is_unit a op)).

Definition has_unit := [a:E;op:E2]
(A (property a op)
   (is_unit a op (unit a op))
).


Definition are_inverse :=[a:E; op:E2; x,y:E]
(A (inc x a)
(A (inc y a)
   (is_unit a op (op x y))
)).

Lemma inverse_comm : (a:E; op:E2; x,y:E)(are_inverse a op x y) -> (are_inverse a op y x).
Skip. Save.

Definition inverse := [a:E; op:E2; x:E](choose [y:E](are_inverse a op x y)).

Definition has_inverses := [a:E;op : E2]
(A (has_unit a op)
   (x:E)(inc x a) -> (are_inverse a op x (inverse a op x))
).

Definition is_monoid :=[a:E;op:E2]
(A (property a op)
(A (is_associative a op)
   (has_unit a op)
)).

Definition is_group := [a:E;op:E2]
(A (is_monoid a op)
   (has_inverses a op)
).

Definition is_abelian_monoid := [a:E;op:E2]
(A (is_monoid a op)
   (is_commutative a op)
).

Definition is_abelian_group := [a:E;op:E2]
(A (is_group a op)
   (is_commutative a op)
).

Definition compatible := [a:E; oa: E2; b:E;ob:E2; f:E -> E]
(A (property a oa)
(A (property b ob)
(A (x:E)(inc x a) -> (inc (f x) b)
   (x,y:E)(inc x a) -> (inc y a) -> (f (oa x y)) == (ob (f x) (f y))
))).

Lemma compatible_id : (a:E; oa : E2)(property a oa) -> (compatible a oa a oa [x:E]x).
Skip. Save.

Lemma compatible_comp : (a:E; oa: E2; b:E;ob:E2; c: E; oc: E2; f,g:E -> E)
(compatible a oa b ob f) -> (compatible b ob c oc g) -> (compatible a oa c oc [x:E](g (f x))).
Skip. Save.

Definition ucompatible := [a:E; oa : E2; b:E; ob : E2; f:E -> E]
(A (has_unit a oa) 
(A (has_unit b ob)
(A (compatible a oa b ob f)
   (f (unit a oa)) == (unit b ob)
))).

Lemma ucompatible_id : (a:E; oa: E2)(has_unit a oa) -> (ucompatible a oa a oa [x:E]x).
Skip. Save.

Lemma ucompatible_comp : (a:E; oa: E2; b:E;ob:E2; c: E; oc: E2; f,g:E -> E)
(ucompatible a oa b ob f) -> (ucompatible b ob c oc g) -> (ucompatible a oa c oc [x:E](g (f x))).
Skip. Save.



End Magma.

Definition Plus := (index (31)).
Definition Times := (index (32)).
Definition Mult := (index (33)).

Module Ring.

(***** make the convention that we speak of crings here; later if we want to do noncomm rings 
we can just recopy this part and erase commutativity *******************************************)

Definition plus := [r,x,y:E](V (V (get Plus r) x) y).
Definition times := [r,x,y:E](V (V (get Times r) x) y).

Definition zero := [r:E](Magma.unit (U r) (plus r)).
Definition one := [r:E](Magma.unit (U r) (times r)).
Definition neg := [r,x:E](Magma.inverse (U r) (plus r) x).

Definition minus := [r,x,y:E](plus r x (neg r y)).

Definition create := [a:E; p,t : E2]
(set Underlying a
(set Plus (L a [x:E](L a [y:E](p x y)))
(set Times (L a [x:E](L a [y:E](t x y)))
emptyset))).

Definition like := [r:E](create (U r) (plus r) (times r)) == r.

Definition property := [a:E; p,t:E2]
(A (Magma.is_abelian_group a p)
(A (Magma.is_abelian_monoid a t)
(A (x,y,z:E)(inc x a) -> (inc y a) -> (inc z a) -> (t x (p y z)) == (p (t x y) (t x z))
   (x,y,z:E)(inc x a) -> (inc y a) -> (inc z a) -> (t (p x y) z) == (p (t x z) (t y z))
))).

Definition axioms := [r:E](property (U r) (plus r) (times r)).
Definition strong_axioms := [r:E](A (like r) (axioms r)).

   
Lemma lem1 : (a:E; p,t:E2)(property a p t) -> 
(A (strong_axioms (create a p t))
(A (x,y:E)(inc x a) -> (inc y a) -> (plus (create a p t) x y) == (p x y)
   (x,y:E)(inc x a) -> (inc y a) -> (times (create a p t) x y) == (t x y)
)).
Skip. Save.


Definition source := Umorphism.source.
Definition target := Umorphism.target.
Definition ev := Umorphism.ev.

Definition mor := [m:E]
(A (Umorphism.axioms m)
(A (axioms (source m))
(A (axioms (target m))
(A (Magma.ucompatible (U (source m)) (plus (source m))  (U (target m)) (plus (target m)) (ev m))
   (Magma.ucompatible (U (source m)) (times (source m)) (U (target m)) (times (target m)) (ev m))
)))).

Definition comp := Umorphism.comp.
Definition id := Umorphism.id.

Definition composable := (Structure.composable mor).

Lemma lem1_0 : (Structure.axioms axioms mor).
Skip. Save.


End Ring.

Module Module.

Definition plus := [q,x,y:E](V (V (get Plus q) x) y).
Definition mult := [q,x,y:E](V (V (get Mult q) x) y).

Definition zero := [q:E](Magma.unit (U q) (plus q)).
Definition neg := [q,x:E](Magma.inverse (U q) (plus q) x).

Definition minus := [r,x,y:E](plus r x (neg r y)).



Definition create := [r,a:E; p,m : E2]
(set Underlying a
(set Plus (L a [x:E](L a [y:E](p x y)))
(set Mult (L (U r) [x:E](L a [y:E](m x y)))
emptyset))).

Definition like := [r,q:E](create r (U q) (plus q) (mult q)) == q.

Definition property := [r,a:E; p,m:E2]
(A (Ring.axioms r)
(A (Magma.is_abelian_group a p)
(A (x,y,z:E)(inc x (U r)) -> (inc y (U r)) -> (inc z a) -> 
     (m (Ring.times r x y) z) == (m x (m y z))
(A (x:E)(inc x a) -> (m (Ring.one r) x) == x
(A (x,y,z:E)(inc x (U r)) -> (inc y a) -> (inc z a) -> 
     (m x (p y z)) == (p (m x y) (m x z))
   (x,y,z:E)(inc x (U r)) -> (inc y (U r)) -> (inc z a) -> 
     (m (Ring.plus r x y) z) == (p (m x z) (m y z))
))))).

Definition axioms := [r,q:E](property r (U q) (plus q) (mult q)).
Definition strong_axioms := [r,q:E](A (like r q) (axioms r q)).

   
Lemma lem1 : (r,a:E; p,m:E2)(property r a p m) -> 
(A (strong_axioms r (create r a p m))
(A (x,y:E)(inc x a) -> (inc y a) -> (plus (create r a p m) x y) == (p x y)
   (x,y:E)(inc x (U r)) -> (inc y a) -> (mult (create r a p m) x y) == (m x y)
)).
Skip. Save.


Definition source := Umorphism.source.
Definition target := Umorphism.target.
Definition ev := Umorphism.ev.

Definition mor := [r,m:E]
(A (Umorphism.axioms m)
(A (axioms r (source m))
(A (axioms r (target m))
(A (Magma.ucompatible (U (source m)) (plus (source m))  (U (target m)) (plus (target m)) (ev m))
   (x,y:E)(inc x (U r)) -> (inc y (U (source m))) -> (ev m (mult (source m) x y)) == (mult (target m) x (ev m y))
)))).

Definition comp := Umorphism.comp.
Definition id := Umorphism.id.

Definition composable := [r:E](Structure.composable (mor r)).

Lemma lem1_0 : (r:E)(Ring.axioms r) -> (Structure.axioms (axioms r) (mor r)).
Skip. Save.

Definition rel_mor := [t,m:E]
(A (Ring.mor t)
(A (Umorphism.axioms m)
(A (axioms (source t) (source m))
(A (axioms (target t) (target m))
(A (Magma.ucompatible (U (source m)) (plus (source m))  
     (U (target m)) (plus (target m)) (ev m))
   (x,y:E)(inc x (U (source t))) -> (inc y (U (source m))) -> 
     (ev m (mult (source m) x y)) == (mult (target m) (Ring.ev t x) (ev m y))
))))).

(*** have to put here the analogue of the categorical stuff for rel_mor, by hand ***)


End Module.

Module Ideal.
Export Ring.
Definition axioms := [r,i:E]
(A (Ring.axioms r)
(A (sub i (U r))
(A (x,y:E)(inc x i) -> (inc y i) -> (inc (plus r x y) i)
   (x,y:E)(inc x (U r)) -> (inc y i) -> (inc (times r x y) i)
))).

Definition set := [r:E](Z (powerset r) [i:E](axioms r i)).
Lemma lem0_1 : (r,i:E)(axioms r i) <-> (inc i (set r)).
Skip. Save.

Definition as_module := [r,i:E](Module.create r i (plus r) (times r)).

Lemma lem1 : (r,i:E)(axioms r i) -> 
(A (Module.property r i (plus r) (times r))
   (Module.strong_axioms r (as_module r i))
).
Skip. Save. 

Definition reln := [r,i,x,y:E](inc (Ring.minus r x y) i).

Lemma lem2 : (r,i:E)(axioms r i) -> (Quotient.eq_reln (U r) (reln r i)).
Skip. Save.

Definition quotient_set := [r,i:E](Quotient.quotient (U r) (reln r i)).
Definition class_mod := [r,i,x:E](Quotient.class (quotient_set r i) x).
Definition rep := [r,i,x:E](Quotient.rep (class_mod r i x)).

Lemma lem3_1 : (r,i:E)(axioms r i) -> 
(A (x:E)(inc x (U r)) -> (inc (class_mod r i x) (quotient_set r i))
(A (x:E)(inc x (quotient_set r i)) -> (class_mod r i (Quotient.rep x)) == x
(A (x,y:E)(inc x (U r)) -> (inc y (U r)) -> 
     (class_mod r i x) == (class_mod r i y) -> (inc (Ring.minus r x y) i)
(A (x,y:E)(inc x (U r)) -> (inc y (U r)) -> (inc (Ring.minus r x y) i) -> 
     (class_mod r i x) == (class_mod r i y)
   (x:E)(inc x (U r)) -> (inc (Ring.minus r x (rep r i x)) i)
)))).
Skip. Save.

Lemma lem3_2 : (r,i:E)(axioms r i) ->
(A (x,y:E)(inc x (U r)) -> (inc y (U r)) -> (class_mod r i (Ring.plus r x y)) ==
    (class_mod r i (Ring.plus r (rep r i x) (rep r i y))) 
(A (x,y:E)(inc x (U r)) -> (inc y (U r)) -> (class_mod r i (Ring.times r x y)) ==
    (class_mod r i (Ring.times r (rep r i x) (rep r i y))) 
   (x:E)(inc x (U r)) -> (class_mod r i (Ring.neg r x)) ==
    (class_mod r i (Ring.neg r (rep r i x))) 
)).
Skip. Save.


Definition quotient_ring := [r,i:E](Ring.create 
(quotient_set r i) 
[x,y:E](Quotient.class (quotient_set r i) (Ring.plus r (Quotient.rep x) (Quotient.rep y)))
[x,y:E](Quotient.class (quotient_set r i) (Ring.times r (Quotient.rep x) (Quotient.rep y)))
).

Lemma lem3_3 : (r,i:E)(axioms r i) -> (Ring.property 
(quotient_set r i) 
[x,y:E](Quotient.class (quotient_set r i) (Ring.plus r (Quotient.rep x) (Quotient.rep y)))
[x,y:E](Quotient.class (quotient_set r i) (Ring.times r (Quotient.rep x) (Quotient.rep y)))
).
Skip. Save.

Lemma lem3_3_1 : (r,i:E)(axioms r i) -> (Ring.axioms (quotient_ring r i)).
Skip. Save.

Definition unit_ideal := [r:E](U r).
Definition zero_ideal := [r:E](singleton (Ring.zero r)).

Lemma lem3_4 : (r,i:E)(Ring.axioms r) -> 
(A (axioms r (unit_ideal r))
   (axioms r (zero_ideal r))
).
Skip. Save.


Definition is_prime := [r,i:E]
(A (axioms r i)
   (x,y:E)(inc x (U r)) -> (inc y (U r)) -> (inc (Ring.times r x y) i) -> 
     ((inc x i) \/ (inc y i))
). 

Definition is_maximal := [r,i:E]
(A (axioms r i)
(A (strict_sub i (U r))
   (j:E)(axioms r j) -> (sub i j) -> (strict_sub j (U r)) ->  i == j
)).

Definition nonunit_ideals := [r:E](Z (Ideal.set r) [i:E](strict_sub i (U r))).

Lemma acc : (r:E)(Ring.axioms r) -> 
(Order.Zorn.hypothesis (nonunit_ideals r) [i,j:E](strict_sub i j)).
Skip. Save.

Lemma maximal_exists : (r:E)(Ring.axioms r) -> (not (Ring.one r) == (Ring.zero r)) ->
(exists [i:E](is_maximal r i)).
Skip. Save.

End Ideal.

Module LocalRing.

Definition axioms := [r:E]
(A (Ring.axioms r)
   (i,j:E)(Ideal.is_maximal r i) -> (Ideal.is_maximal r j) -> i == j
). 

End LocalRing.

Module Algebra.

Definition plus := Ring.plus.
Definition times := Ring.times.
Definition mult := Module.mult.


Definition zero := Ring.zero.
Definition neg := Ring.neg.
Definition one := Ring.one.

Lemma rm : 
(A plus == Module.plus
(A zero == Module.zero
   neg == Module.neg
)).
Skip. Save.



Definition create := [k,a:E; p,t,m : E2]
(set Underlying a
(set Plus (L a [x:E](L a [y:E](p x y)))
(set Times (L a [x:E](L a [y:E](p x y)))
(set Mult (L (U k) [x:E](L a [y:E](m x y)))
emptyset)))).

Definition like := [k,q:E](create k (U q) (plus q) (times q) (mult q)) == q.

Definition property := [k,a:E; p,t,m:E2]
(A (Ring.axioms k)
(A (Ring.property a p t)
(A (Module.property k a p m)
   (x,y,z:E)(inc x (U k)) -> (inc y a) -> (inc z a) -> (m x (t y z)) == (t (m x y) z)
))).

Definition axioms := [k,q:E](property k (U q) (plus q) (times q) (mult q)).
Definition strong_axioms := [k,q:E](A (like k q) (axioms k q)).

   
Lemma lem1 : (k,a:E; p,t,m:E2)(property k a p t m) -> 
(A (strong_axioms k (create k a p t m))
(A (x,y:E)(inc x a) -> (inc y a) -> (plus (create k a p t m) x y) == (p x y)
(A (x,y:E)(inc x a) -> (inc y a) -> (times (create k a p t m) x y) == (t x y)
   (x,y:E)(inc x (U k)) -> (inc y a) -> (mult (create k a p t m) x y) == (m x y)
))).
Skip. Save.

Lemma alg_mod : (k,a:E)(Algebra.axioms k a) -> (Module.axioms k a).
Skip. Save.

Lemma alg_ring : (k,a:E)(Algebra.axioms k a) -> (Ring.axioms a).
Skip. Save.


Definition source := Umorphism.source.
Definition target := Umorphism.target.
Definition ev := Umorphism.ev.

Definition mor := [k,m:E]
(A (Umorphism.axioms m)
(A (axioms k (source m))
(A (axioms k (target m))
(A (Magma.ucompatible (U (source m)) (plus (source m))  (U (target m)) (plus (target m)) (ev m))
(A (Magma.ucompatible (U (source m)) (times (source m))  (U (target m)) (times (target m)) (ev m))
   (x,y:E)(inc x (U k)) -> (inc y (U (source m))) -> (ev m (mult (source m) x y)) == (mult (target m) x (ev m y))
))))).

Definition comp := Umorphism.comp.
Definition id := Umorphism.id.

Definition composable := [k:E](Structure.composable (mor k)).

Lemma lem2 : (k:E)(Ring.axioms k) -> (Structure.axioms (axioms k) (mor k)).
Skip. Save.

Lemma lem3 : (k,m:E)(Algebra.mor k m) <-> (A (Ring.mor m) (Module.mor k m)).
Skip. Save.

End Algebra.


Module Rational.

Definition is_fraction := [a:E]
(A (is_pair a)
(A (inc (pr1 a) Integer.set)
(A (inc (pr2 a) Integer.set)
   (not (pr2 a) == Integer.zero)
))).

Definition fractions := (Bounded.create is_fraction).
Definition num := pr1.
Definition denom := pr2.

Definition integer_fraction := [i:E](pair i Integer.one).

Definition fraction_rel := [a,b:E](Integer.times (num a) (denom b)) == (Integer.times (num b) (denom a)).

Lemma fraction_eq_reln : (Quotient.eq_reln fractions fraction_rel).
Skip. Save.

Definition frationals := (Quotient.quotient fractions fraction_rel).


Definition axioms := [a:E]
(inc a Integer.set) \/
(A (inc a frationals)
   (i:E)(not (A (inc i Integer.set) 
(Quotient.class (integer_fraction i) frationals) == a))
).

Definition set := (Bounded.create axioms).

Lemma integer_sub : (sub Integer.set Rational.set).
Skip. Save.

Parameter plus : E -> E -> E.
Parameter minus : E -> E -> E.
Parameter times : E -> E -> E.
Parameter divide : E -> E -> E.

Parameter lt : E -> E -> Prop.
Parameter le : E -> E -> Prop.





End Rational.


Module Real.

Definition is_dedekind := [x:E]
(A (sub x Rational.set)
(A (y,z:E)(inc y x) -> (Rational.le y z) -> (inc z x)
(A (y:E)(inc y x) -> (exists [z:E](A (inc z x) (Rational.lt z y)))
   (exists [z:E](A (inc z Rational.set) (not (inc z x))))
))).

Definition dedekinds := (Bounded.create is_dedekind).

Definition rational_dedekind := [a:E](Z Rational.set [y:E](Rational.lt a y)).
Lemma lem1 : (a:E)(inc a Rational.set) -> (inc (rational_dedekind a) dedekinds).
Skip. Save.

Definition axioms := [a:E]
(inc a Rational.set) \/
(A (inc a dedekinds) 
(x:E)(not (A (inc x Rational.set) (rational_dedekind x) == a))
).

Definition set := (Bounded.create axioms).

Lemma rational_sub : (sub Rational.set Real.set).
Skip. Save.
Parameter plus : E -> E -> E.
Parameter minus : E -> E -> E.
Parameter times : E -> E -> E.
Parameter divide : E -> E -> E.

Parameter lt : E -> E -> Prop.
Parameter le : E -> E -> Prop.





End Real.

Module Topology.

Definition space := union.

Definition axioms := [u:E]
(A (x:E)(inc x u) -> (sub x (space u))
(A (inc (space u) u)
(A (inc emptyset u)
(A (f:E)(sub f u) -> (inc (union f) u)
   (x,y:E)(inc x u) -> (inc y u) -> (inc (intersection2 x y) u)
)))).


Definition mor_create := [u,v:E; f:E -> E]
(J u
(J v
(J (L (space u) f)
emptyset))).

Definition source := (Pr (0)).
Definition target := (Pr (1)).
Definition ev := [m,x:E](V (Pr (2) m) x).
Definition pullback := [m,y:E](Z (space (source m)) [a:E](inc (ev m a) y)).


Definition mor := [m:E]
(A (axioms (source m))
(A (axioms (target m))
(A (mor_create (source m) (target m) (ev m)) == m
(A (Transformation.axioms (space (source m)) (space (target m)) (ev m))
   (u:E)(inc u (target m)) -> (inc (pullback m u) (source m))
)))).

Definition id := [u:E](mor_create u u [y:E]y).
Definition comp := [m,n:E](mor_create (source n) (target m) [y:E](ev m (ev n y))).
Definition composable := (Structure.composable mor).

Lemma lem1 : (Structure.axioms axioms mor).
Skip. Save.



Definition open_subspace := [y,u:E](Z u [a:E](sub a y)).

Lemma lem6 : (y,u:E)(axioms u) -> (inc y u) -> (axioms (open_subspace y u)).
Skip. Save.

Definition open_inclusion := [y,u:E](mor_create (open_subspace y u) u [a:E]a).

Lemma lem7 : (u,y:E)(axioms u) -> (inc y u) -> (mor (open_inclusion y u)).
Skip. Save.



Definition included := [t,v,u:E]
(A (Topology.axioms t)
(A (inc u t)
(A (inc v t)
   (sub v u)
))). 




End Topology.

Module Presheaf.

Export Topology.

Definition Topo := (index (25)).
Definition Val := (index (26)).
Definition Res := (index (27)).
Definition Str := (index (28)).

Definition topo := (get Topo).
Definition val := [f,u:E](V (get Val f) u).
Definition str := [f,u:E](V (get Str f) u).
Definition res := [f,u,v,a:E](V (V (V (get Res f) u) v) a).

Definition create := [t:E; va : E -> E; re : E-> E -> E -> E; st: E -> E]
(set Topo t
(set Val (L t va)
(set Res (L t [u:E](L (open_subspace u t) [v:E](L (va u) (re u v))))
(set Str (L t st)
emptyset)))).

Definition like := [f:E](create (topo f) (val f) (res f) (str f)) == f.

Definition property := [t:E; va : E -> E; re : E-> E -> E -> E]
(A (Topology.axioms t)
(A (u,v,a:E)(included t v u) -> (inc a (va u)) -> (inc (re u v a) (va v))
(A (u,a:E)(inc u t) -> (inc a (va u)) -> (re u u a) == a
   (u,v,w,a:E)(included t w v) -> (included t v u) -> (inc a (va u)) -> (re v w (re u v a)) == (re u w a)
))).

Definition axioms := [t,f:E]
(A (topo f) == t
   (property (topo f) (val f) (res f))
).
Definition strong_axioms := [t,f:E](A (like f) (axioms t f)).

Lemma lem1 : (t:E; va : E -> E; re : E-> E -> E -> E; st : E -> E)
(property t va re) -> (strong_axioms t (create t va re st)).
Skip. Save.
Lemma lem2 : (t:E; va : E -> E; re : E-> E -> E -> E; st: E -> E; u:E)
(property t va re) -> (inc u t) -> (val (create t va re st) u) == (va u).
Skip. Save.
Lemma lem3 : (t:E; va : E -> E; re : E-> E -> E -> E; st: E -> E; u,v,a:E)
(property t va re) -> (included t v u) -> (inc a (va u)) ->
(res (create t va re st) u v a) == (re u v a).
Skip. Save.

Definition mor_create := [f,g:E; mv:E -> E -> E]
(J f
(J g 
(J (L (topo f) [u:E](L (val f u) [a:E](mv u a)))
emptyset))).

Definition source := (Pr (0)).
Definition target := (Pr (1)).
Definition mval := [m,u,a:E](V (V (Pr (2) m) u) a).

Definition mor := [t,m:E]
(A (axioms t (source m))
(A (axioms t (target m))
(A (mor_create (source m) (target m) (mval m)) == m
(A (u,a:E)(inc u (topo (source m))) -> (inc a (val (source m) u)) -> (inc (mval m u a) (val (target m) u))
   (u,v,a:E)(included (topo (source m)) v u) -> (inc a (val (source m) u)) ->
            (mval m v (res (source m) u v a)) == (res (target m) u v (mval m u a))
)))). 

Definition hom := [t,f,g,m:E]
(A (mor t m)
(A (source m) == f
   (target m) == g
)).

Definition homs := [t,f,g:E](Bounded.create (hom t f g)).

Lemma homs1 : (t, f,g,m:E)(hom t f g m) <-> (inc m (homs t f g)).
Skip. Save.
 
Definition id := [f:E](mor_create f f [u,y:E]y).
Definition comp := [m,n:E](mor_create (source n) (target m) [u,a:E](mval m u (mval n u a))). 
Definition composable := [t:E](Categorical.composable (mor t) source target).

Lemma categorical : (t:E)(Topology.axioms t) ->
(Categorical.axioms (axioms t) (mor t) source target comp id).
Skip. Save.
(** now we define the set of sections of a presheaf f over a subset (sub r (topo f)) **)

Definition local_sections := [f,r:E](Z (F r [u:E](val f u)) [s:E]
(A (axioms (topo f) f)
(A (sub r (topo f))
   (u,v:E)(inc u r) -> (inc v r) -> 
          (res f u (intersection2 u v) (V s u)) == (res f v (intersection2 u v) (V s v))
))).

Lemma lem4 : (t,f,r,a:E)(axioms t f) -> (sub r t) -> (inc a (val f (union r))) ->
(inc (L r [u:E](res f (union r) u a)) (local_sections f r)).
Skip. Save.

Definition constant := [t,a:E](create t [u:E]a [u,v,x:E]x [u:E]a).
Definition uconstant := [t,a:E](create t [u:E](U a) [u,v,x:E]x [u:E]a).

Lemma constant_presheaf : (t,a:E)(Topology.axioms t) -> (axioms t (constant t a)).
Skip. Save.

Lemma uconstant_presheaf : (t,a:E)(Topology.axioms t) -> (axioms t (uconstant t a)).
Skip. Save.

Definition restriction := [f,u:E](create 
(Topology.open_subspace u (topo f))  
[v:E](val f v)
[v,w,a:E](res f v w a)
[v:E](str f v)).

Lemma restriction_presheaf : (t,f,u:E)(axioms t f) -> (inc u t) -> 
(axioms (Topology.open_subspace u t) (restriction f u)).
Skip. Save.

Lemma restriction_comp : (t,f,u,v:E)(axioms t f) -> (included t v u) ->
(restriction (restriction f u) v) == (restriction f v).
Skip. Save.

Lemma restriction_id : (t,f:E)(axioms t f) -> (restriction f (space t)) == f.
Skip. Save.

Definition ihom := [t,f,g:E](create 
t 
[u:E](homs (Topology.open_subspace u t) (restriction f u) (restriction g u))
[u,v,m:E](mor_create (restriction f v) (restriction g v) [w,a:E](mval m w a))
[u:E]u
).

Lemma ihom_axioms : (t,f,g:E)(axioms t f) -> (axioms t g) ->
(axioms t (ihom t f g)).
Skip. Save.

Definition str_res := [f,u,v:E](Umorphism.create (str f u) (str f v) (res f u v)).
Definition str_mval := [m,u:E](Umorphism.create (str (source m) u) (str (target m) u) (mval m u)).

Definition structured := [t,f:E]
(A (axioms t f)
   (u:E)(inc u t) -> (U (str f u)) == (val f u)
).


Module OfMagmas.

Definition axioms := [f:E; o: E -> E -> E -> E]
(A (Presheaf.axioms (topo f) f)
(A (u:E)(inc u (topo f))->(Magma.property (val f u) (o u))
   (u,v:E)(included (topo f) v u) -> (Magma.compatible (val f u) (o u) (val f v) (o v) (res f u v))
)).

Definition is_associative := [f:E; o:E3]
(A (axioms f o)
   (u:E)(inc u (topo f)) ->(Magma.is_associative (val f u) (o u))
).

Definition is_commutative := [f:E; o:E3]
(A (axioms f o)
   (u:E)(inc u (topo f)) ->(Magma.is_commutative (val f u) (o u))
).

Definition has_unit := [f:E; o:E3]
(A (axioms f o)
(A (u:E)(inc u (topo f)) ->(Magma.has_unit (val f u) (o u))
   (u,v:E)(included (topo f) v u) -> 
     (res f u v (Magma.unit (val f u) (o u))) == (Magma.unit (val f v) (o v))
)).

Definition has_inverses := [f:E; o:E3]
(A (has_unit f o)
   (u:E)(inc u (topo f)) -> (Magma.has_inverses (val f u) (o u))
).

Lemma lem1 : (f:E; o:E3; u,v,x:E)(has_inverses f o) -> (included (topo f) v u) -> (inc x (val f u)) ->
(res f u v (Magma.inverse (val f u) (o u) x)) == (Magma.inverse (val f v) (o v) (res f u v x)).
Skip. Save.

Definition is_monoid :=[f:E;o:E3]
(A (axioms f o)
(A (is_associative f o)
   (has_unit f o)
)).

Definition is_group := [f:E;o:E3]
(A (is_monoid f o)
   (has_inverses f o)
).

Definition is_abelian_monoid := [f:E;o:E3]
(A (is_monoid f o)
   (is_commutative f o)
).

Definition is_abelian_group := [f:E;o:E3]
(A (is_group f o)
   (is_commutative f o)
).


(*** do morphisms too ... ***)

Definition compatible := [t:E; osource,otarget : E3; m:E]
(A (Presheaf.mor t m)
(A (axioms (source m) osource)
(A (axioms (target m) otarget)
   (u:E)(inc u t) -> (Magma.compatible (val (source m) u) (osource u) (val (target m) u) (otarget u) (mval m u))
))).

Definition ucompatible := [t:E; osource,otarget : E3; m:E]
(A (Presheaf.mor t m)
(A (axioms (source m) osource)
(A (axioms (target m) otarget)
   (u:E)(inc u t) -> (Magma.ucompatible (val (source m) u) (osource u) (val (target m) u) (otarget u) (mval m u))
))).




End OfMagmas.


Definition plus := [f,u,x,y:E](V (V (get Plus (str f u)) x) y).
Definition times := [f,u,x,y:E](V (V (get Times (str f u)) x) y).
Definition mult := [f,u,x,y:E](V (V (get Mult (str f u)) x) y).
Definition zero := [f,u:E](Magma.unit (val f u) (plus f u)).
Definition one := [f,u:E](Magma.unit (val f u) (times f u)).
Definition neg := [f,u,x:E](Magma.inverse (val f u) (plus f u) x).


Module OfRings.

Definition axioms := [t,f:E]
(A (structured t f)
(A (u:E)(inc u t) -> (Ring.axioms (str f u))
   (u,v:E)(included t v u) -> (Ring.mor (str_res f u v))
)).

Definition create := [t:E; va: E -> E; re : E -> E -> E -> E; pl,ti: E -> E -> E -> E]
(Presheaf.create t va re [u:E](Ring.create (va u) (pl u) (ti u))).

Definition property := [t:E; va: E -> E; re : E -> E -> E -> E; pl,ti: E -> E -> E -> E]
(A (Topology.axioms t)
(A (Presheaf.property t va re)
(A (u:E)(inc u t) -> (Ring.property (va u) (pl u) (ti u))
(A (u,v,x,y:E)(included t v u) -> (inc x (va u)) -> (inc y (va u)) ->
    (re u v (pl u x y)) == (pl v (re u v x) (re u v y))
(A (u,v,x,y:E)(included t v u) -> (inc x (va u)) -> (inc y (va u)) ->
    (re u v (ti u x y)) == (ti v (re u v x) (re u v y))
   (u,v:E)(included t v u) -> (re u v (Magma.unit (va u) (ti u))) == (Magma.unit (va v) (ti v))
))))).

Lemma create_axioms : (t:E; va: E -> E; re : E -> E -> E -> E; pl,ti: E -> E -> E -> E; f:E)
(property t va re pl ti) -> f == (create t va re pl ti) ->
(A (OfRings.axioms t f)
(A (u:E)(inc u t) -> (val f u) == (va u)
(A (u,v,x:E)(included t v u) -> (inc x (va u)) -> (res f u v x) == (re u v x)
(A (u,x,y:E)(inc u t) -> (inc x (va u)) -> (inc y (va u)) -> (plus f u x y) == (pl u x y)
(A (u,x,y:E)(inc u t) -> (inc x (va u)) -> (inc y (va u)) -> (times f u x y) == (ti u x y)
(A (u,x:E)(inc u t) -> (inc x (va u)) -> (neg f u x) == (Magma.inverse (va u) (pl u) x)
(A (u:E)(inc u t) -> (zero f u) == (Magma.unit (va u) (pl u))
   (u:E)(inc u t) -> (one f u) == (Magma.unit (va u) (ti u))
))))))).
Skip. Save.
 

Lemma lem1 : (t,f,u:E)(OfRings.axioms t f) -> (inc u t) -> 
(A (Ring.property (val f u) (plus f u) (times f u))
(A (x,y:E)(inc x (val f u)) -> (inc y (val f u)) -> (Ring.plus (str f u) x y) == (plus f u x y)
(A (x,y:E)(inc x (val f u)) -> (inc y (val f u)) -> (Ring.times (str f u) x y) == (times f u x y)
(A (x:E)(inc x (val f u)) -> (Ring.neg (str f u) x) == (neg f u x)
(A (Ring.zero (str f u)) == (zero f u)
   (Ring.one (str f u)) == (one f u)
))))).
Skip. Save.

Lemma lem2 : (t,f,u,v:E)(OfRings.axioms t f) -> (included t v u) ->
(A (x,y:E)(inc x (val f u)) -> (inc y (val f u)) -> 
     (plus f v (res f u v x) (res f u v y)) == (res f u v (plus f u x y))
(A (x,y:E)(inc x (val f u)) -> (inc y (val f u)) -> 
     (times f v (res f u v x) (res f u v y)) == (res f u v (times f u x y))
(A (x:E)(inc x (val f u)) -> (neg f v (res f u v x)) == (res f u v (neg f u x))
(A (res f u v (zero f u)) == (zero f v)
   (res f u v (one f u)) == (one f v)
)))).
Skip. Save.

Definition mor := [t,m:E]
(A (OfRings.axioms t (source m))
(A (OfRings.axioms t (target m))
(A (Presheaf.mor t m)
   (u:E)(inc u t) -> (Ring.mor (str_mval m u))
))).

Definition composable := [t:E](Categorical.composable (mor t) source target).

Lemma categorical : (t:E)(Topology.axioms t) -> 
(Categorical.axioms (OfRings.axioms t) (OfRings.mor t) source target comp id).
Skip. Save.

Lemma lem3 : (t,m:E)(OfRings.mor t m) ->
(A (u,x,y:E)(inc u t) -> (inc x (val (source m) u)) -> (inc y (val (source m) u)) ->
     (plus (target m) u (mval m u x) (mval m u y)) == (mval m u (plus (source m) u x y))
(A (u,x,y:E)(inc u t) -> (inc x (val (source m) u)) -> (inc y (val (source m) u)) ->
     (times (target m) u (mval m u x) (mval m u y)) == (mval m u (times (source m) u x y))
(A (u,x:E)(inc u t) -> (inc x (val (source m) u)) -> 
     (neg (target m) u (mval m u x)) == (mval m u (neg (source m) u x))
(A (u:E)(inc u t) ->  (zero (target m) u) == (mval m u (zero (source m) u))
   (u:E)(inc u t) ->  (one (target m) u) == (mval m u (one (source m) u))
)))).
Skip. Save. 




End OfRings.

Module OfModules.

Definition axioms := [r,f:E]
(A (OfRings.axioms (topo r) r)
(A (structured (topo r) f)
(A (u:E)(inc u (topo r)) -> (Module.axioms (str r u) (str f u))
   (u,v:E)(included (topo r) v u) -> (Module.rel_mor (str_res r u v) (str_res f u v))
))).


Definition create := [r:E; va: E -> E; re : E -> E -> E -> E; pl,mu: E -> E -> E -> E]
(Presheaf.create (topo r) va re [u:E](Module.create (str r u) (va u) (pl u) (mu u))).

Definition property := [r:E; va: E -> E; re : E -> E -> E -> E; pl,mu: E -> E -> E -> E]
(A (Topology.axioms (topo r))
(A (Presheaf.property (topo r) va re)
(A (u:E)(inc u (topo r)) -> (Module.property (str r u) (va u) (pl u) (mu u))
(A (u,v,x,y:E)(included (topo r) v u) -> (inc x (va u)) -> (inc y (va u)) ->
    (re u v (pl u x y)) == (pl v (re u v x) (re u v y))
   (u,v,x,y:E)(included (topo r) v u) -> (inc x (val r u)) -> (inc y (va u)) ->
    (re u v (mu u x y)) == (mu v (re u v x) (re u v y))
)))).

Lemma create_axioms : (r:E; va: E -> E; re : E -> E -> E -> E; pl,mu: E -> E -> E -> E; f:E)
(property r va re pl mu) -> f == (create r va re pl mu) ->
(A (OfModules.axioms r f)
(A (u:E)(inc u (topo r)) -> (val f u) == (va u)
(A (u,v,x:E)(included (topo r) v u) -> (inc x (va u)) -> (res f u v x) == (re u v x)
(A (u,x,y:E)(inc u (topo r)) -> (inc x (va u)) -> (inc y (va u)) -> (plus f u x y) == (pl u x y)
(A (u,x,y:E)(inc u (topo r)) -> (inc x (va u)) -> (inc y (va u)) -> (mult f u x y) == (mu u x y)
(A (u,x:E)(inc u (topo r)) -> (inc x (va u)) -> 
     (neg f u x) == (Magma.inverse (va u) (pl u) x)
   (u:E)(inc u (topo r)) -> (zero f u) == (Magma.unit (va u) (pl u))
)))))).
Skip. Save.
 

Lemma lem1 : (r,f,u:E)(OfModules.axioms r f) -> (inc u (topo r)) -> 
(A (Module.property (str r u) (val f u) (plus f u) (times f u))
(A (x,y:E)(inc x (val f u)) -> (inc y (val f u)) -> (Module.plus (str f u) x y) == (plus f u x y)
(A (x,y:E)(inc x (val r u)) -> (inc y (val f u)) -> (Module.mult (str f u) x y) == (mult f u x y)
(A (x:E)(inc x (val f u)) -> (Module.neg (str f u) x) == (neg f u x)
   (Ring.zero (str f u)) == (zero f u)
)))).
Skip. Save.

Lemma lem2 : (r,f,u,v:E)(OfModules.axioms r f) -> (included (topo r) v u) ->
(A (x,y:E)(inc x (val f u)) -> (inc y (val f u)) -> 
     (plus f v (res f u v x) (res f u v y)) == (res f u v (plus f u x y))
(A (x,y:E)(inc x (val r u)) -> (inc y (val f u)) -> 
     (mult f v (res f u v x) (res f u v y)) == (res f u v (mult f u x y))
(A (x:E)(inc x (val f u)) -> (neg f v (res f u v x)) == (res f u v (neg f u x))
   (res f u v (zero f u)) == (zero f v)
))).
Skip. Save.

Definition mor := [r,m:E]
(A (OfModules.axioms r (source m))
(A (OfModules.axioms r (target m))
(A (Presheaf.mor (topo r) m)
   (u:E)(inc u (topo r)) -> (Module.mor (str r u) (str_mval m u))
))).

Definition composable := [t:E](Categorical.composable (mor t) source target).

Lemma categorical : (r:E)(OfRings.axioms (topo r) r) -> 
(Categorical.axioms (OfModules.axioms r) (OfModules.mor r) source target comp id).
Skip. Save.

Lemma lem3 : (r,m:E)(OfModules.mor r m) ->
(A (u,x,y:E)(inc u (topo r)) -> (inc x (val (source m) u)) -> (inc y (val (source m) u)) ->
     (plus (target m) u (mval m u x) (mval m u y)) == (mval m u (plus (source m) u x y))
(A (u,x,y:E)(inc u (topo r)) -> (inc x (val r u)) -> (inc y (val (source m) u)) ->
     (mult (target m) u (mval m u x) (mval m u y)) == (mval m u (mult (source m) u x y))
(A (u,x:E)(inc u (topo r)) -> (inc x (val (source m) u)) -> 
     (neg (target m) u (mval m u x)) == (mval m u (neg (source m) u x))
   (u:E)(inc u (topo r)) ->  (zero (target m) u) == (mval m u (zero (source m) u))
))).
Skip. Save. 

End OfModules.

Module OfAlgebras.

(**** here we look at presheaves of algebras over a fixed ring k;
if we wanted to do algebras over a sheaf of rings r we would have to redo it
(it would look more like OfModules) ****)

Definition axioms := [k,t,f:E]
(A (Ring.axioms k)
(A (structured t f)
(A (u:E)(inc u t) -> (Algebra.axioms k (str f u))
   (u,v:E)(included t v u) -> (Algebra.mor k (str_res f u v))
))).

Lemma of_rings : (k,t,f:E)(axioms k t f) -> (OfRings.axioms t f).
Skip. Save.

Definition create := [k,t:E; va: E -> E; re : E -> E -> E -> E; pl,ti,mu: E -> E -> E -> E]
(Presheaf.create t va re [u:E](Algebra.create k (va u) (pl u) (ti u) (mu u))).

Definition property := [k,t:E; va: E -> E; re : E -> E -> E -> E; pl,ti, mu: E -> E -> E -> E]
(A (Ring.axioms k)
(A (Topology.axioms t)
(A (Presheaf.property t va re)
(A (u:E)(inc u t) -> (Algebra.property k (va u) (pl u) (ti u) (mu u))
(A (u,v,x,y:E)(included t v u) -> (inc x (va u)) -> (inc y (va u)) ->
    (re u v (pl u x y)) == (pl v (re u v x) (re u v y))
(A (u,v,x,y:E)(included t v u) -> (inc x (va u)) -> (inc y (va u)) ->
    (re u v (ti u x y)) == (ti v (re u v x) (re u v y))
(A (u,v,x,y:E)(included t v u) -> (inc x (U k)) -> (inc y (va u)) ->
    (re u v (mu u x y)) == (mu v (re u v x) (re u v y))
   (u,v:E)(included t v u) -> (re u v (Magma.unit (va u) (ti u))) == (Magma.unit (va v) (ti v))
))))))).

Lemma create_axioms : (k,t:E; va: E -> E; re : E -> E -> E -> E; pl,ti,mu: E -> E -> E -> E; f:E)
(property k t va re pl ti mu) -> f == (create k t va re pl ti mu) ->
(A (OfAlgebras.axioms k t f)
(A (u:E)(inc u t) -> (val f u) == (va u)
(A (u,v,x:E)(included t v u) -> (inc x (va u)) -> (res f u v x) == (re u v x)
(A (u,x,y:E)(inc u t) -> (inc x (va u)) -> (inc y (va u)) -> (plus f u x y) == (pl u x y)
(A (u,x,y:E)(inc u t) -> (inc x (va u)) -> (inc y (va u)) -> (times f u x y) == (ti u x y)
(A (u,x,y:E)(inc u t) -> (inc x (U k)) -> (inc y (va u)) -> (mult f u x y) == (mu u x y)
(A (u,x:E)(inc u t) -> (inc x (va u)) -> (neg f u x) == (Magma.inverse (va u) (pl u) x)
(A (u:E)(inc u t) -> (zero f u) == (Magma.unit (va u) (pl u))
   (u:E)(inc u t) -> (one f u) == (Magma.unit (va u) (ti u))
)))))))).
Skip. Save.
 

Lemma lem1 : (k,t,f,u:E)(OfAlgebras.axioms k t f) -> (inc u t) -> 
(A (Algebra.property k (val f u) (plus f u) (times f u) (mult f u))
(A (x,y:E)(inc x (val f u)) -> (inc y (val f u)) -> (Algebra.plus (str f u) x y) == (plus f u x y)
(A (x,y:E)(inc x (val f u)) -> (inc y (val f u)) -> (Algebra.times (str f u) x y) == (times f u x y)
(A (x,y:E)(inc x (U k)) -> (inc y (val f u)) -> (Algebra.mult (str f u) x y) == (mult f u x y)
(A (x:E)(inc x (val f u)) -> (Algebra.neg (str f u) x) == (neg f u x)
(A (Algebra.zero (str f u)) == (zero f u)
   (Algebra.one (str f u)) == (one f u)
)))))).
Skip. Save.

Lemma lem2 : (k, t,f,u,v:E)(OfAlgebras.axioms k t f) -> (included t v u) ->
(A (x,y:E)(inc x (val f u)) -> (inc y (val f u)) -> 
     (plus f v (res f u v x) (res f u v y)) == (res f u v (plus f u x y))
(A (x,y:E)(inc x (val f u)) -> (inc y (val f u)) -> 
     (times f v (res f u v x) (res f u v y)) == (res f u v (times f u x y))
(A (x,y:E)(inc x (U k)) -> (inc y (val f u)) -> 
     (mult f v x (res f u v y)) == (res f u v (mult f u x y))
(A (x:E)(inc x (val f u)) -> (neg f v (res f u v x)) == (res f u v (neg f u x))
(A (res f u v (zero f u)) == (zero f v)
   (res f u v (one f u)) == (one f v)
))))).
Skip. Save.

Definition mor := [k,t,m:E]
(A (OfAlgebras.axioms k t (source m))
(A (OfAlgebras.axioms k t (target m))
(A (Presheaf.mor t m)
   (u:E)(inc u t) -> (Algebra.mor k (str_mval m u))
))).

Definition composable := [k,t:E](Categorical.composable (mor k t) source target).

Lemma categorical : (k,t:E)(Topology.axioms t) -> (Ring.axioms k) ->
(Categorical.axioms (OfAlgebras.axioms k t) (OfAlgebras.mor k t) source target comp id).
Skip. Save.

Lemma lem3 : (k,t,m:E)(OfAlgebras.mor k t m) ->
(A (u,x,y:E)(inc u t) -> (inc x (val (source m) u)) -> (inc y (val (source m) u)) ->
     (plus (target m) u (mval m u x) (mval m u y)) == (mval m u (plus (source m) u x y))
(A (u,x,y:E)(inc u t) -> (inc x (val (source m) u)) -> (inc y (val (source m) u)) ->
     (times (target m) u (mval m u x) (mval m u y)) == (mval m u (times (source m) u x y))
(A (u,x,y:E)(inc u t) -> (inc x (U k)) -> (inc y (val (source m) u)) ->
     (mult (target m) u x (mval m u y)) == (mval m u (mult (source m) u x y))
(A (u,x:E)(inc u t) -> (inc x (val (source m) u)) -> 
     (neg (target m) u (mval m u x)) == (mval m u (neg (source m) u x))
(A (u:E)(inc u t) ->  (zero (target m) u) == (mval m u (zero (source m) u))
   (u:E)(inc u t) ->  (one (target m) u) == (mval m u (one (source m) u))
))))).
Skip. Save.

End OfAlgebras.



(*** give the set of local sections, structures of rings or modules ****)

End Presheaf.

Module Stalk.

Export Presheaf.


Definition carrier := [f,x:E](Z (D (Z (topo f) [u:E](inc x u)) [u:E](val f u)) [a:E]
(A (Presheaf.axioms (topo f) f)
   (inc x (space (topo f)))
)).

Definition openset := (Pr (0)).
Definition section := (Pr (1)).

Lemma lem1 : (f,x,a:E)(inc a (carrier f x)) <->
(A (Presheaf.axioms (topo f) f)
(A (J (openset a) (section a)) == a
(A (inc (openset a) (topo f))
(A (inc x (openset a))
   (inc (section a) (val f (openset a)))
)))).
Skip. Save.

Definition neighborhood := [t,x,u:E]
(A (Topology.axioms t)
(A (inc u t)
   (inc x u)
)).
Definition subneighborhood := [t,x,u,v:E]
(A (neighborhood t x u) 
(A (neighborhood t x v)
   (sub u v)
)).

Definition reln := [f,x,a,b:E](exists [u:E]
(A (subneighborhood (topo f) x u (openset a))
(A (subneighborhood (topo f) x u (openset b))
   (res f (openset a) u (section a)) == (res f (openset b) u (section b))
))).

Lemma lem2 : (f,x:E)(Presheaf.axioms (topo f) f)  -> (inc x (space (topo f))) ->
(Quotient.eq_reln (carrier f x) (reln f x)).
Skip. Save.

Definition create := [f,x:E](Quotient.quotient (carrier f x) (reln f x)).

Definition germ := [f,x,u,a:E](Quotient.class (J u a) (create f x)).
Definition rep := Quotient.rep.

Definition  able := [f,x,u,a:E]
(A (Presheaf.axioms (topo f) f)
(A (neighborhood (topo f) x u)
   (inc a (val f u)
))).

Lemma lem3 : (f,x,u,a:E)(able f x u a) -> (inc (germ f x u a) (create f x)).
Skip. Save.

Lemma lem4 : (f,x,a:E)(inc a (create f x)) -> (able f x (openset (rep a)) (section (rep a))).
Skip. Save.


Definition relates := [f,x,u,a,v,b,w:E]
(A (Presheaf.axioms (topo f) f)
(A (subneighborhood (topo f) x w u)
(A (subneighborhood (topo f) x w v)
(A (inc a (val f u))
(A (inc b (val f v))
   (res f u w a) == (res f v w b)
))))).

Definition relater := [f,x,u,a,v,b:E](choose (relates f x u a v b)).

Lemma lem5 : (f,x,u,a,v:E)(able f x u a) -> (subneighborhood (topo f) x v u) ->
(relates f x u a v (res f u v a) v).
Skip. Save.

Lemma lem6 : (f,x,u,a,v,b,w,y:E)(relates f x u a v b w) -> (subneighborhood (topo f) x y w) ->
(relates f x u a v b y).
Skip. Save.

Lemma lem7 : (f,x,u,a,v,b,w:E)(relates f x u a v b w) -> (germ f x u a) == (germ f x v b).
Skip. Save.

Lemma lem8 : (f,x,u,a,v,b:E)(able f x u a) -> (able f x v b) ->
(germ f x u a) == (germ f x v b) -> (relates f x u a v b (relater f x u a v b)).
Skip. Save.

Lemma lem9 : (f,x,u,a:E)(able f x u a) ->
(germ f x u a) == (germ f x (openset (rep (germ f x u a))) (section (rep (germ f x u a)))).
Skip. Save.

(**** morphisms of presheaves give morphisms of stalks ***)

Definition map := [m,x,a:E](germ (target m) x (openset (rep a)) (mval m (openset (rep a)) (section (rep a)))).

Lemma lem10 : (t,m,x,a:E)(Presheaf.mor t m) -> (inc x t) -> (inc a (create (source m) x)) ->
(inc (map m x a) (create (target m) x)).
Skip. Save.

Lemma lem11 : (t,m,x,u,a:E)(Presheaf.mor t m) -> (able (source m) x u a) -> (map m x (germ (source m) x u a))
== (germ (target m) x u (mval m u a)).
Skip. Save.
 




Module AsMagma.
Definition common_open := [a,b:E]
(intersection2 (openset (rep a)) (openset (rep b))).

Definition op := [f,x:E; o:E3; a,b:E](o (common_open a b)
(res f (openset (rep a)) (common_open a b) (section (rep a)))
(res f (openset (rep b)) (common_open a b) (section (rep b)))
).

Lemma lem1 : (f,x:E; o:E3;u,a,v,b,w:E)(OfMagmas.axioms f o) -> (inc x (topo f)) ->
(able f x u a) -> (able f x v b) -> 
(subneighborhood (topo f) x w u) -> (subneighborhood (topo f) x w v) ->
(op f x o (germ f x u a) (germ f x v b)) == (germ f x w (o w (res f u w a) (res f v w b))).
Skip. Save.

Lemma lem2 : (f,x:E; o:E3)(OfMagmas.axioms f o) -> (inc x (topo f)) ->
(Magma.property (create f x) (op f x o)).
Skip. Save.

(*** ???? do all of the various possible properties ****)

Lemma lem3 : (m,x:E; osource,otarget : E3)(Presheaf.mor (topo (source m)) m) -> 
(OfMagmas.compatible (topo (source m)) osource otarget m) -> (inc x (topo (source m))) ->
(Magma.compatible 
(create (source m) x) (op (source m) x osource) 
(create (target m) x) (op (target m) x otarget)
(map m x)
).
Skip. Save.

Lemma lem4 : (m,x:E; osource,otarget : E3)(Presheaf.mor (topo (source m)) m) -> 
(OfMagmas.ucompatible (topo (source m)) osource otarget m) -> 
(inc x (topo (source m))) ->
(Magma.ucompatible 
(create (source m) x) (op (source m) x osource) 
(create (target m) x) (op (target m) x otarget)
(map m x)
).
Skip. Save.



End AsMagma.
(*** rings, modules, algebras ***)

Module AsRing.

End AsRing.

Module AsModule.

End AsModule.

Module AsAlgebra.

End AsAlgebra.

End Stalk.


Module Sheaf.

Export Presheaf.

Definition axiom1 := [f:E]
(r,a,b:E)(sub r (topo f)) -> 
(inc a (val f (union r))) ->
(inc b (val f (union r))) ->
((u:E)(inc u r) -> (res f (union r) u a) == (res f (union r) u b)) ->
a==b.

Definition axiom2 := [f:E]
(r,a:E)(sub r (topo f)) -> (inc a (local_sections f r)) ->
(exists [b:E]
(A (inc b (val f (union r)))
   (u:E)(inc u r) -> (res f (union r) u b) == (V a u)
)). 

Definition axioms := [f:E]
(A (Presheaf.axioms (topo f) f)
(A (axiom1 f)
   (axiom2 f)
)).

Definition is_association := [m:E]
(A (Presheaf.mor (topo (source m)) m)
(A (Sheaf.axioms (Presheaf.target m))
   (n:E)(Presheaf.mor (topo (source n)) n) -> 
(Presheaf.source n) == (Presheaf.source m) 
   -> (Sheaf.axioms (Presheaf.target n)) -> (exists_unique [p:E]
        (A (Presheaf.composable (topo (source m)) p m) (Presheaf.comp p m) == n))
)).

Theorem thm1 : (f:E)(Presheaf.axioms (topo f) f) -> 
(exists [m:E](A (is_association m) (Presheaf.source m) == f)).
Skip. Save.

Definition association := [f:E](choose [m:E](A (is_association m) (Presheaf.source m) == f)).

Lemma cor1 : (f:E)(Presheaf.axioms (topo f) f) -> (is_association (association f)).
Skip. Save.

Definition associated := [f:E](Presheaf.target (association f)).

Lemma ihom_sheaf : (f,g:E)(Presheaf.axioms (topo f) f) -> 
(axioms g) -> (topo f) == (topo g) ->
(axioms (Presheaf.ihom (topo f) f g)).
Skip. Save.

End Sheaf.