(*** file notation9.v, version of november 10, 2003---Carlos Simpson ***)


Set Implicit Arguments.

Require Arith.
Require groundwork7.




Module Notation_gen.

Module preregions.



Definition add_translates := [phi : E1; x:E]
(union2 x (IM [a:x](phi (R a)))). 


Lemma add_translates_sub :(phi : E1; x:E)
(sub x (add_translates phi x)). 
ir; uf add_translates; uf sub; ir. ap union2_first; am. 
Save.

Lemma add_translates_new : (phi : E1; x,y:E)
(inc y x) -> (inc (phi y) (add_translates phi x)).
ir; uf add_translates; ir. ap union2_second. 
ap  IM_inc. sh '(B H). 
rw B_eq. tv. 
Save.

Definition im_pr := [x:E](union2 (add_translates pr1 x) (add_translates pr2 x)).

Lemma im_pr_sub: (x:E)(sub x (im_pr x)).
ir. uf sub; ir. uf im_pr. ap union2_first. ap add_translates_sub. am.
Save.

Lemma im_pr_pr1 :(x,a:E)(inc a x) -> (inc (pr1 a) (im_pr x)).
ir. uf im_pr. ap union2_first. ap add_translates_new. am.
Save.

Lemma im_pr_pr2 :(x,a:E)(inc a x) -> (inc (pr2 a) (im_pr x)).
ir. uf im_pr. ap union2_second. ap add_translates_new. am.
Save.


Definition add_pairs := [x:E](union2 (im_pr x) (product x x)).

Lemma add_pairs_sub : (x:E)(sub x (add_pairs x)).
ir; uf add_pairs. uf sub. ir. ap union2_first. ap im_pr_sub. am.
Save.

Lemma add_pairs_pairs : (x,a,b:E)(inc a x) -> (inc b x) 
-> (inc (J a b) (add_pairs x)). 
ir. uf add_pairs. 
ap union2_second. ap product_pair_inc; am. 
Save. 

Lemma add_pairs_pr : (x,a:E)(inc a x) ->
(A (inc (pr1 a) (add_pairs x)) (inc (pr2 a) (add_pairs x))).
ir. dj. uf add_pairs. ap union2_first. ap im_pr_pr1. am. uf add_pairs.
ap union2_first. ap im_pr_pr2. am.
Save. 


Definition add_elements := [x:E](union2 x (union x)).

Lemma add_elements_sub : (x:E)(sub x (add_elements x)). 
ir; uf add_elements; uf sub; ir. ap union2_first; am. 
Save. 


Lemma add_elements_elts : (x,y,z:E)(inc y x) -> (inc z y) ->
(inc z (add_elements x)).
ir; uf add_elements; ap union2_second. 
Apply union_inc with y; am. 
Save. 

Definition add_values := (add_translates [x:E](V (pr1 x) (pr2 x))).

Lemma add_values_sub : (x:E)(sub x (add_values x)).
ir; uf add_values; ap add_translates_sub.
Save. 

Lemma add_values_values : (x,y:E)(inc y x) -> (inc (V (pr1 y) (pr2 y)) (add_values x)).
ir.
Exact (add_translates_new [z:E](V (pr1 z) (pr2 z)) H).
Save. 

Definition add_all := [phi : E1; x:E]
(add_values (add_elements (add_translates phi (add_pairs x)))).

Lemma add_all_sub : (phi:E1; x:E)(sub x (add_all phi x)).
uf add_all; uf sub; ir. 
ap add_values_sub.
ap add_elements_sub. ap add_translates_sub.
ap add_pairs_sub. am.
Save.

Lemma add_all_pair : (phi:E1; x,a,b:E)(inc a x) -> (inc b x)
-> (inc (pair a b) (add_all phi x)).
ir; uf add_all. ap add_values_sub. ap add_elements_sub. ap add_translates_sub.
ap add_pairs_pairs; am. 
Save. 

Lemma add_all_pr : (phi:E1; x,a:E)(inc a x) -> 
(A (inc (pr1 a) (add_all phi x)) (inc (pr2 a) (add_all phi x))).
ir. dj. uf add_all. ap add_values_sub.
ap add_elements_sub. ap add_translates_sub.
Remind '(add_pairs_pr H). xd. Remind '(add_pairs_pr H).
uf add_all. ap add_values_sub. ap add_elements_sub. ap add_translates_sub. xd.
Save. 


Lemma add_all_translate : (phi:E1; x,a:E)(inc a x)->
(inc (phi a) (add_all phi x)).
ir; uf add_all; 
ap add_values_sub;
ap add_elements_sub. ap add_translates_new.
ap add_pairs_sub; am. 
Save. 

Lemma add_all_elt : (phi:E1; x,y,z:E)(inc y x) -> (inc z y)
-> (inc z (add_all phi x)).
ir; uf add_all. ap add_values_sub. Apply add_elements_elts with y. 
ap add_translates_sub; ap add_pairs_sub; am. am.
Save. 

Lemma add_all_values : (phi:E1; x,y:E)(inc y x) -> (inc (V (pr1 y) (pr2 y)) (add_all phi x)).
ir.
uf add_all. ap add_values_values. ap add_elements_sub. ap add_translates_sub. ap add_pairs_sub. am.
Save. 

Definition add_all_rec : (n:nat; phi : E1; x:E)E.
Intro n; nin n.
ir; am. ir. Exact (add_all phi (IHn phi x)). 
Defined. 

Definition pool := [phi:E1; x:E](IM [n:nat](add_all_rec n phi x)). 

Lemma aar_in_pool : (n:nat; phi : E1; x:E)
(inc (add_all_rec n phi x) (pool phi x)). 
ir. uf pool; ap IM_inc. sh n. tv. 
Save.

Lemma pool_from_aar :(phi:E1; x,y:E)(inc y (pool phi x)) ->
(exT ? [n:nat]y==(add_all_rec n phi x)). 
ir. ufi pool H. Pose (IM_exists H). nin e.
sh x0. sy; am.
Save. 

Lemma pool_add_all : (phi:E1; x,y,z:E)(inc y (pool phi x)) ->
(inc z (add_all phi y)) -> 
(exists [w:E](A (inc w (pool phi x)) (inc z w))).
ir. Pose (pool_from_aar H). nin e. 
sh '(add_all_rec (S x0) phi x). ee. 
ap aar_in_pool. 
Change (inc z (add_all phi (add_all_rec x0 phi x))). 
wr H1. am. 
Save. 


Lemma nat_family_sub : (f:nat -> E; hyp : (n:nat)(sub
(f n) (f (S n))); n,m:nat)(lt n m) -> (sub (f n) (f m)).
ir. nin H. ap hyp. Apply sub_trans with (f m); au.  
Save. 

Lemma aar_S_sub : (n:nat; phi : E1; x:E)(sub (add_all_rec 
n phi x) (add_all_rec (S n) phi x)).
ir. LetTac K:= (add_all_rec n phi x). 
Change (sub K (add_all phi K)). ap add_all_sub. 
Save. 

Lemma aar_lt_sub : (n,m:nat; phi : E1; x:E)
(lt n m) -> (sub (add_all_rec n phi x) (add_all_rec m phi x)). 
ir. Pose (nat_family_sub 1![i:nat](add_all_rec i phi x)). 
Pose (s [n:nat](aar_S_sub 1!n 2!phi 3!x)). ap s0; ir; am. 
Save.

Lemma strub_exists : (m,n:nat)(exT ? [p:nat](A (lt m p)
(lt n p))). 
ir. Pose (Coq.Arith.Compare_dec.lt_eq_lt_dec m n). 
nin s. nin a. sh '(S n). xd. sh '(S n). xd. 
rw b; au. sh '(S m); xd. 
Save. 


Definition zoom := [phi : E1; x:E](union (pool phi x)). 


Lemma zoom_pr : (phi : E1; x,a,b:E)(inc a (zoom phi x)) ->
(inc b (zoom phi x)) -> 
(exists [z:E]
(A (inc a z) 
(A (inc b z) 
   (sub (add_all phi z) (zoom phi x))
))). 
ir. ufi zoom H; ufi zoom H0. Pose (union_exists H);
Pose (union_exists H0). nin e; nin e0. ee. 
nin '(pool_from_aar H4). nin '(pool_from_aar H3). 
nin '(strub_exists x2 x3). ee. 
Pose (aar_lt_sub 3!phi 4!x H7). 
Pose (aar_lt_sub 3!phi 4!x H8).
sh '(add_all_rec x4 phi x). xd. ap s;
wr H5; am. ap s0; wr H6; am. 
uf sub; ir; uf zoom. 
Apply union_inc with (add_all_rec (S x4) phi x). 
Exact H9. ap aar_in_pool. 
Save.

Lemma zoom_sub : (phi : E1; x:E)(sub x (zoom phi x)). 
uf sub; ir. uf zoom.
Apply union_inc with (add_all_rec (0) phi x). 
Exact H. ap aar_in_pool. 
Save. 

Lemma zoom_translate : (phi : E1; x,y:E)
(inc y (zoom phi x)) -> (inc (phi y) (zoom phi x)). 
ir. nin '(zoom_pr H H); ee. ap H2. ap 
add_all_translate. am. 
Save. 

Lemma zoom_pair : (phi:E1; x,a,b:E)
(inc a (zoom phi x)) -> (inc b (zoom phi x)) ->
(inc (J a b) (zoom phi x)). 
ir. nin '(zoom_pr H H0). ee. ap H3. 
ap add_all_pair; am. 
Save. 

Lemma zoom_projections : (phi : E1; x,a:E)(inc a (zoom phi x)) ->
(A (inc (pr1 a) (zoom phi x)) (inc (pr2 a) (zoom phi x))).
ir. Pose (zoom_pr H H). nin e. ee; Pose (add_all_pr phi H0); xd. 
Save.

Lemma zoom_elt : (phi : E1; x,y,z:E)
(inc y (zoom phi x)) -> (inc z y) -> 
(inc z (zoom phi x)). 
ir. nin '(zoom_pr H H); ee. 
ap H3. Apply add_all_elt with y; am. 
Save. 

Lemma zoom_values : (phi : E1; x,y:E)(inc y (zoom phi x)) ->
(inc (V (pr1 y) (pr2 y)) (zoom phi x)).
ir. 
nin '(zoom_pr H H); ee. ap H2. ap add_all_values. am.
Save. 

End preregions.



Definition arity_type : nat -> Type.
ir. nin H. Exact E. Exact E->IHnat.
Defined. 

Fixpoint arex [n:nat]: (E->E) -> (arity_type n):=
<[n:nat](E->E)-> (arity_type n)>
Cases n of
O => [u:E->E](u emptyset) |
(S m) => [u:E->E; x:E](arex m [y:E](u (J x y)))
end. 

Lemma arex_S_rw : (n:nat; u:E->E)(arex (S n) u) == [x:E](arex n [y:E](u (J x y))).
ir; tv. 
Save. 

Fixpoint arsimilar [reg : E; n:nat]:
(arity_type n) -> (arity_type n) -> Prop :=
<[n:nat](arity_type n) -> (arity_type n)-> Prop>
Cases n of
O => [x,y:E]x==y |
(S m) => [u,v:E -> (arity_type m)](x:E)(inc x reg) -> 
(arsimilar reg (u x) (v x))
end. 

Lemma arsimilar_O : (reg:E; f,g:(arity_type (0)))(arsimilar reg 2!(0) f g) -> f==g.
ir; am.
Save.

Lemma arsimilar_S : (reg:E; n:nat; f,g:(arity_type (S n)))(arsimilar reg 2!(S n) f g) ->
((x:E)(inc x reg)->(arsimilar reg 2!n (f x) (g x))).
Intros reg n f g H. am.
Save. 

Lemma arsimilarS : (reg:E; n:nat; f,g:(arity_type (S n)))
((x:E)(inc x reg)->(arsimilar reg 2!n (f x) (g x))) -> (arsimilar reg 2!(S n) f g).
Intros reg n f g H. am.
Save. 

Lemma E1_nonempty : (nonemptyT E1). 
Apply nonemptyT_intro. ir; am. 
Save. 


Fixpoint arex_inv [n:nat]:(arity_type n) -> E -> E :=
<[n:nat](arity_type n) -> E -> E>Cases n of
O => [a,b:E]a |
(S m) => [f:(arity_type (S m)); x:E]
(arex_inv 1!m (f (pr1 x)) (pr2 x))
end. 


Lemma arex_inv_pr : (n:nat; f: (arity_type n))
(arex n (arex_inv f)) == f. 
Intro n; nin n; ir. tv. 
Change ([x:E](arex n [y:E](arex_inv f (J x y))) )== f. 
Apply arrow_extensionality. ir. 
Assert ([y:E](arex_inv f (J a y))) == (arex_inv (f a)). 
Apply arrow_extensionality. ir. 
Transitivity
(arex_inv 1!n (f (pr1 (pair a a0))) (pr2 (pair a a0))); tv.
rw pr1_pair. rw pr2_pair. tv. 
rw H. rw IHn. tv. 
Save.  



Definition approximates := [reg:E; f:E1; u:E]
(y:E)(inc y reg) -> (V y u) == (f y).

Lemma L_approx : (reg:E; f: E1)
(approximates reg f (L reg f)). 
ir. uf approximates; ir. Apply Function.create_V_rewrite. 
am. 
Save. 

Lemma arsimilar_arex : (reg:E; n:nat; u,v:E1)
(inc emptyset reg) -> ((a,b:E)(inc a reg) -> (inc b reg) -> (inc (J a b) reg)) -> 
(arsimilar reg 2!(1) u v) -> (arsimilar reg 2!n (arex n u) (arex n v)).
Intros reg n; nin n; ir. Change (u emptyset)==(v emptyset). Remind '(arsimilar_S H1).
ap H2. am. ap arsimilarS. ir. rw arex_S_rw. rw arex_S_rw. ap IHn; au.
ap arsimilarS. ir. Change (u (pair x x0))==(v (pair x x0)). ap H1. ap H0; am.
Save. 

Lemma arsimilar_f_arex : 
(reg:E; n:nat; f:(arity_type n); u:E1)
(inc emptyset reg) -> ((a,b:E)(inc a reg) -> (inc b reg) -> (inc (J a b) reg)) -> 
((x:E)(inc x reg)-> (arex_inv f x) == (u x))  -> (arsimilar reg 2!n f (arex n u)).
ir. Assert f==(arex n (arex_inv f)). sy. ap arex_inv_pr. rw H2.
ap arsimilar_arex. am. am. am.
Save. 


Definition object := [t:E; k:t->nat](a:t)(arity_type (k a)).


Definition obex : (t:E; k:t->nat)(E->E) -> (object k):=
[t:E; k:t->nat; f:E->E; a:t]
(arex (k a) [x:E](f (J (R a) x))).

Definition obex_inv :(t:E; k:t->nat)(object k) -> E -> E :=
[t:E; k:t->nat; o:(object k); x:E]
(choose [y:E](hyp : (inc (pr1 x) t))y==(arex_inv (o (B hyp)) (pr2 x))).

Definition obex_pr := [t:E; k:t->nat; o:(object k); x,y:E]
(hyp : (inc (pr1 x) t))y==(arex_inv (o (B hyp)) (pr2 x)).

Lemma obex_pr_rw : (t:E; k:t->nat; o:(object k); x:E)
(obex_inv o x) == (choose (obex_pr o x)).
ir; tv.
Save. 


Lemma obex_inv_rw : (t:E; k:t->nat; o:(object k); a:t; x:E)
(obex_inv o (J (R a) x)) == (arex_inv (o a) x).
ir.
uf obex_inv.
Assert
 (exists
   [y:E]
     (hyp:(inc (pr1 (J (R a) x)) t))
       y==(arex_inv (o (B hyp)) (pr2 (J (R a) x)))).
Apply exists_intro with (arex_inv (o a) x).
ir.
Assert (B hyp)==a.
ap R_inj; rw B_eq; tv.
ap pr1_pair.

rw H.
rw pr2_pair.
tv.

Pose (choose_pr H).
Assert (inc (pr1 (pair (R a) x)) t).
rw pr1_pair.
ap R_inc.

Pose (e H0).
rw e0.
Assert (B H0)==a.
ap R_inj; rw B_eq; tv.
ap pr1_pair.

rw H1.
rw pr2_pair; tv.
Save. 

Lemma obex_inv_pr : (t:E; k:t->nat; o:(object k))
(obex k (obex_inv o)) == o.
ir.
uf obex.
Assert (a:t)(arex (k a) [x:E](obex_inv o (J (R a) x)))==(o a).
ir.
Assert ([x:E](obex_inv o (J (R a) x)))==(arex_inv (o a)).
ap arrow_extensionality.
ir.
ap obex_inv_rw.

rw H.
ap arex_inv_pr.

Exact (prod_extensionality 1!t 2![a:t](arity_type (k a))
3!([a:t](arex (k a) [x:E](obex_inv o (pair (R a) x))))
4!o 
H).
Save. 

Definition preregion := [t:E; k:t->nat; o:(object k)]
(preregions.zoom (obex_inv o) (union2 t (singleton emptyset))).



Fixpoint preserves [reg:E; n:nat]:(arity_type n)-> Prop :=
<[n:nat](arity_type n)-> Prop>
Cases n of
O => [f:E](inc f reg) |
(S m) => [f:E-> (arity_type m)](x:E)(inc x reg) -> 
(preserves reg 2!m (f x))
end. 


Lemma preserves_S : (reg:E; n:nat; f:(arity_type (S n)))
(preserves reg f) == ((x:E)(inc x reg) -> (preserves reg 2!n (f x))).
ir. ap iff_eq. Intro H; am. Intro H; am.
Save. 

Lemma preserves_criterion : (reg:E; n:nat; f:(arity_type n))
((a,b:E)(inc a reg) -> (inc b reg) -> (inc (J a b) reg)) ->
((a:E)(inc a reg) -> (inc (arex_inv f a) reg)) ->
(nonempty reg) -> 
(preserves reg f).
Intros reg n; nin n. ir. Change (inc f reg). 
nin H1. Exact (H0 y H1). 
ir. Change (x:E)(inc x reg) -> (preserves reg 2!n (f x)). 
ir. ap IHn. am. 
ir. Assert (arex_inv 1!n (f x) a) ==
(arex_inv 1!(S n) f (J x a)). 
Transitivity (arex_inv 1!n (f (pr1 (J x a))) (pr2 (J x a))). 
rw pr1_pair; rw pr2_pair; tv. tv. rw H4. ap H0. ap H; am. 
am. 
Save. 

Lemma preregion_stability : (t:E; k:t->nat; o:(object k))
(A (sub t (preregion o))
(A (a,b:E)(inc a (preregion o)) -> (inc b (preregion o)) -> 
(inc (J a b) (preregion o))
(A (x,y:E)(inc x (preregion o)) -> (inc y x) -> (inc y (preregion o))
(A (a:t)(preserves (preregion o) (o a))
(A (inc emptyset (preregion o))
(A  (x:E)(inc x (preregion o)) -> (A (inc (pr1 x) (preregion o)) (inc (pr2 x) (preregion o)))
   (x,y:E)(inc x (preregion o)) -> (inc y (preregion o)) -> (inc (V x y) (preregion o))
)))))). 
ir. dj. uf preregion.  Apply sub_trans with (union2 t (singleton emptyset)).
uf sub; ir. ap union2_first. am.
ap preregions.zoom_sub. 
uf preregion; ap preregions.zoom_pair; am. 
uf preregion; Apply preregions.zoom_elt with x; am. 
ap preserves_criterion. am.
uf preregion. ir. 
Assert (arex_inv 1!(k a) (o a) a0) ==
(obex_inv o (J (R a) a0)). sy. ap obex_inv_rw. 
rw H3. ap preregions.zoom_translate. ap preregions.zoom_pair. 
ap H. ap R_inc. am. Apply nonempty_intro with (R a).
ap H. ap R_inc. 
Assert (sub (union2 t (singleton emptyset)) (preregion o)).
uf preregion. ap preregions.zoom_sub. ap H3. ap union2_second. ap singleton_inc.
ufi preregion H4. Pose (preregions.zoom_projections H4). xd.
ufi preregion H4. Pose (preregions.zoom_projections H4). xd.

Assert (inc (J x y) (preregion o)). ap H0; am. LetTac z:=(pair x y).
Assert (V x y)==(V (pr1 z) (pr2 z)). uf z. rw pr1_pair. rw pr2_pair. tv.
rw H8. Remind '(preregions.zoom_values H7). Exact H9.
Save. 

Definition stability_condition := [t:E; k:t->nat; o:(object k);reg:E]
(A (sub t reg)
(A (a,b:E)(inc a reg) -> (inc b reg) -> (inc (J a b) reg)
(A (x,y:E)(inc x reg) -> (inc y x) -> (inc y reg)
(A (a:t)(preserves reg (o a))
(A (inc emptyset reg)
(A (x:E)(inc x reg) -> (A (inc (pr1 x) reg) (inc (pr2 x) reg))
   (x,y:E)(inc x reg) -> (inc y reg) -> (inc (V x y) reg)
)))))). 

Lemma preregion_cond : (t:E; k:t->nat; o:(object k))(stability_condition o (preregion o)).
ir. Exact (preregion_stability o). 
Save.

Lemma preserves_intersection : (n:nat; f:(arity_type n); regint : E)((r:E)(inc r regint) -> (preserves r f)) ->
(nonempty regint) -> (preserves (intersection regint) f).
Intro n; nin n; ir.
Change (inc f (intersection regint)).
ap intersection_inc; am.
Change (x:E)(inc x (intersection regint)) ->(preserves (intersection regint) 2!n (f x)).
ir. ap IHn. ir. Remind '(H r H2). Assert (inc x r).
Apply intersection_forall with regint; am.
Apply (H3 x H4). am.
Save. 

Lemma stability_condition_intersection : (t:E; k:t->nat; o:(object k); regint : E)((r:E)(inc r regint) ->
(stability_condition o r)) -> (nonempty regint) -> (stability_condition o (intersection regint)).
ir. uf stability_condition; xd. uf sub; ir. ap intersection_inc. am.
ir. Remind '(H y H2). ufi stability_condition H3. xd.
ir. Remind '(intersection_use_inc H1). Remind '(intersection_use_inc H2).
ap intersection_inc. am.
ir. Assert (inc a y). Apply H3; am. Assert (inc b y). ap H4; am.
Remind '(H y H5). ufi stability_condition H8. xd.
ir. Remind '(intersection_use_inc H1). ap intersection_inc. am.
ir. Remind '(H y0 H4). ufi stability_condition H5. xd. Apply H7 with x.
ap H3; am. am. ir. ap preserves_intersection. ir.
ufi stability_condition H; Remind '(H r H1); xd. am.
ap intersection_inc. am. ir. Remind '(H y H1). ufi stability_condition H2; xd.

ir.
xd.
ap intersection_inc.
am.

ir.
Remind '(H y H2).
ufi stability_condition H3; xd.
Remind '(intersection_use_inc H1).
Remind '(H10 y H2).
Remind '(H8 x H11).
xd.

ap intersection_inc. am.
ir.
Remind '(H y H2).
ufi stability_condition H3; xd.
Remind '(intersection_use_inc H1).
Remind '(H10 y H2).
Remind '(H8 x H11).
xd.

ir.
ap intersection_inc.
am.

ir.
Remind '(H ? H3).
uh H4; ee.
ap H10.
ap '(intersection_use_inc H1).
am.

ap '(intersection_use_inc H2).
am.
Save.

Lemma stability_condition_intersection2 : (t:E; k:t->nat; o:(object k); r1,r2:E)(stability_condition o r1) ->
(stability_condition o r2) -> (stability_condition o (intersection2 r1 r2)).
ir. uf intersection2. ap stability_condition_intersection. ir.
Remind '(doubleton_or H1). nin H2. rw H2; am. rw H2; am. sh r1. ap doubleton_first.
Save. 

Definition region_intersecters := [t:E; k:t->nat; o:(object k)](Z (powerset (preregion o)) [r:E](stability_condition o r)).

Definition region := [t:E; k:t->nat; o:(object k)](intersection (region_intersecters o)).

Lemma region_stability : (t:E; k:t->nat; o:(object k))(stability_condition o (region o)).
ir. uf region. ap stability_condition_intersection. ir. ufi region_intersecters H. Ztac. 
sh '(preregion o). uf region_intersecters. Ztac. ap powerset_inc; uf sub; ir; am. ap preregion_cond.
Save.

Lemma region_smallest : (t:E; k:t->nat; o:(object k); r:E)(stability_condition o r) -> (sub (region o) r).
ir. Pose s:=(preregion o). Assert (stability_condition o s). uf s; ap preregion_cond.
Pose u:=(intersection2 r s). Assert (stability_condition o u). uf u; ap stability_condition_intersection2; am.
uf region. Assert (inc u (region_intersecters o)). uf region_intersecters; Ztac. ap powerset_inc.
Change (sub u s). uf u. uf sub; ir. Apply intersection2_second with r. am.
Apply sub_trans with u. Apply intersection_sub. am. uf u; uf sub; ir. Apply intersection2_first with s. am.
Save. 


Definition similar := [reg,t:E; k:t->nat; o,p:(object k)]
(a:t)(arsimilar reg (o a) (p a)).


Lemma arsimilar_symm : (n:nat; f,g:(arity_type n); r:E)(arsimilar r f g) ->(arsimilar r g f).
Intro n; nin n; ir. Change g==f. sy. am. ap arsimilarS. ir. ap IHn. ap H. am.
Save. 

Lemma arsimilar_sub :(n:nat; f,g:(arity_type n); r1,r2:E)(sub r1 r2) -> (arsimilar r2 f g) -> 
(arsimilar r1 f g).
Intro n; nin n; ir. am. ap arsimilarS. Remind '(arsimilar_S H0). ir. Apply IHn with r2.
am. ap H1. ap H; am.
Save.

Lemma similar_symm : (t:E; k:t->nat; o,p:(object k); r:E)(similar r o p) -> (similar r p o).
uf similar; ir. ap arsimilar_symm; ap H.
Save.

Lemma similar_sub :(t:E; k:t->nat; o,p:(object k);r1,r2:E)(sub r1 r2) -> (similar r2 o p) ->
(similar r1 o p).
uf similar; ir. Apply arsimilar_sub with r2. am. ap H0.
Save. 

Lemma arsimilar_preserves : (n:nat; f,g:(arity_type n);r:E)(preserves r f) ->
(arsimilar r f g) -> (preserves r g).
Intro n; nin n; ir.  Change (inc g r). Remind '(arsimilar_O H0). wr H1; am. rw preserves_S.
ir. rwi preserves_S H. Remind '(arsimilar_S H0). Apply IHn with (f x). ap H; am. ap H2; am.
Save. 

Lemma similar_stab : (t:E; k:t->nat; o,p:(object k); r:E)(stability_condition o r) ->
(similar r o p) -> (stability_condition p r).
uf stability_condition; ir; xd. ufi similar H0. ir. Apply arsimilar_preserves with (o a). ap H3. ap H0.
Save. 


Lemma similar_same_region1 : (t:E; k:t->nat; o,p:(object k); r:E)(stability_condition o r) ->
(similar r o p) -> (region o) == (region p).
ir. ap extensionality. ap region_smallest. Apply similar_stab with p. ap region_stability.
Apply similar_sub with r. ap region_smallest. Apply similar_stab with o; am. ap similar_symm. am.
ap region_smallest. Apply similar_stab with o. ap region_stability. Apply similar_sub with r.
ap region_smallest. am. am.
Save. 

Lemma similar_same_region : (t:E; k:t->nat; o,p:(object k))
(similar (region o) o p) -> (region o) == (region p).
ir. Apply similar_same_region1 with (region o). ap region_stability. am.
Save. 




Definition createN := [t:E; k:t->nat; o:(object k)]
(L (region o) (obex_inv o)).

Definition extract := [t:E; k:t->nat; u:E](obex k [x:E](V x u)).


Lemma extract_create_similar : (t:E; k:t->nat; o:(object k))
(similar (region o) o (extract k (createN o))).
ir. uf similar; ir. uf extract. uf obex. Assert (stability_condition o (region o)).
ap region_stability. ap arsimilar_f_arex. ufi stability_condition H; xd. ir.
ufi stability_condition H. xd. ir. uf createN. rw Function.create_V_rewrite.
rw obex_inv_rw. tv. ufi stability_condition H. xd. ap H1. ap H. ap R_inc. am.
Save. 

Lemma stability_pr1 : (t:E; k:t->nat; o:(object k);r,x:E)(stability_condition o r)
->(inc x r) -> (inc (pr1 x) r).
ir. ufi stability_condition H. xd. Pose (H5 x H0). xd.
Save.

Lemma stability_pr2 : (t:E; k:t->nat; o:(object k);r,x:E)(stability_condition o r)
->(inc x r) -> (inc (pr2 x) r).
ir. ufi stability_condition H. xd. Pose (H5 x H0). xd.
Save.

Lemma arsimilar_arex_inv : (reg:E; n:nat; f,g:(arity_type n); x:E)(inc x reg) ->
((x:E)(inc x reg) -> (A (inc (pr1 x) reg) (inc (pr2 x) reg))) ->
(arsimilar reg f g) -> (arex_inv f x) == (arex_inv g x).
Intros reg n; nin n; ir. Change f==g. am.
Change (arex_inv (f (pr1 x)) (pr2 x))==(arex_inv (g (pr1 x)) (pr2 x)).
Remind '(H0 x H); ee. ap IHn. am. am. Remind '(arsimilar_S H1). ap H4; am.
Save. 


Lemma similar_obex_imp : (t:E; k:t->nat; o,p:(object k);r,x,y:E)(similar r o p) ->
(stability_condition o r) -> (inc x r) -> (obex_pr o x y) -> (obex_pr p x y).
ir.
ufi stability_condition H0; xd.
Remind '(H7 x H1).
xd.
uf obex_pr.
ir.
ufi obex_pr H2.
Remind '(H2 hyp).
ufi similar H.
Remind '(H (B hyp)).
rw H11.
Apply arsimilar_arex_inv with r; am.
Save. 

Lemma similar_obex_inv : (t:E; k:t->nat; o,p:(object k);r:E)(similar r o p) ->
(stability_condition o r) -> (stability_condition p r)
-> ((x:E)(inc x r) -> (obex_inv o x) == (obex_inv p x)).
ir.
rw obex_pr_rw.
rw obex_pr_rw.
Assert (obex_pr o x)==(obex_pr p x).
ap arrow_extensionality.
ir.
ap iff_eq.
ir.
Apply similar_obex_imp with o r; am.

ir.
Apply similar_obex_imp with p r.
ap similar_symm; am. am. am. am.

rw H3. tv.
Save.

Lemma similar_create_eq1 : (t:E; k:t->nat; o,p:(object k); r:E)
(similar r o p) -> (stability_condition o r) -> (stability_condition p r)
-> (createN o) == (createN p).
ir.
uf createN.
ap Function.create_extensionality.
Apply similar_same_region1 with r; am.

ir.
Assert (similar (region o) o p).
Apply similar_sub with r.
ap region_smallest; am.

am.

Apply similar_obex_inv with (region o).
am.

ap region_stability.

Assert (region o)==(region p).
Apply similar_same_region.
am.

rw H5.
ap region_stability.

am.
Save. 

Lemma similar_create_eq : (t:E; k:t->nat; o,p:(object k))
(similar (region o) o p) -> (createN o) == (createN p).
ir.
Apply similar_create_eq1 with (region o).
am.

ap region_stability.

Assert (region o)==(region p).
ap similar_same_region; am.

rw H0.
ap region_stability.
Save. 


Lemma create_extract_create : (t:E; k:t->nat; o,p:(object k))
(createN (extract k (createN o))) == (createN o).
ir. sy. ap similar_create_eq. ap extract_create_similar.
Save. 



Lemma region_preserves : (t:E; k:t->nat; o:(object k); a:t)
(preserves (region o) (o a)). 
ir. Remind '(region_stability o). ufi stability_condition H. 
xd.
Save. 

Lemma region_preserves_sub : (t:E; k:t->nat; o:(object k);x:E)
(inc x (region o)) -> (sub x (region o)).
ir. Assert (stability_condition o (region o)). 
ap region_stability. uf sub; ir. ufi stability_condition H0; xd.
Apply H3 with x; am. Save. 


Lemma region_value : (t:E; k:t->nat; o:(object k); x:E; a:t)
(inc x (region o)) -> (inc (V (J (R a) emptyset) x) (region o)).
ir.
Assert (stability_condition o (region o)). ap region_stability. 
uh H0. ee. ap H6. ap H1. ap H0. ap R_inc. ap H4. am.
Save. 



Definition default_arity : (n:nat)(arity_type n). 
Intro n; nin n. Exact emptyset. Exact [x:E]IHn. 
Defined. 


Definition related := [t:E; k:t->nat; o:(object k); a:E]
(inc a (region o)).

Tactic Definition sub_relate a :=
Match Context With
[|-(related ?1 ?)]-> uf related; ap '(region_preserves_sub
(region_preserves ?1 a)).


Lemma related_value : (t:E; k:t->nat; o:(object k); x:E; a:t)
(related o x) -> (related o (V (J (R a) emptyset) x)).
ir.
uf related. ap region_value. am.
Save. 


Lemma arsimilar_arity0 : (t:E; k:t->nat; o:(object k); f,g:E)
(arsimilar (region o) 2!(0) f g) ->f==g.
ir. Exact H. Save. 


Lemma arsimilar_arity1 : (t:E; k:t->nat; o:(object k); f,g:E1)
(arsimilar (region o) 2!(1) f g) ->
((a:E)(related o a)-> (f a) == (g a)).
ir. Remind '(arsimilar_S H H0). 
Exact H1. 
Save.

Lemma arsimilar_arity2 : (t:E; k:t->nat; o:(object k); f,g:E2)
(arsimilar (region o) 2!(2) f g) ->
((a,b:E)
(related o a)->
(related o b) -> 
(f a b) == (g a b)).
ir. 
Pose K1:= (arsimilar_S H H0). 
Exact (arsimilar_S K1 H1). 
Save.

Lemma arsimilar_arity3 : (t:E; k:t->nat; o:(object k); f,g:E3)
(arsimilar (region o) 2!(3) f g) ->
((a,b,c:E)
(related o a)->
(related o b) ->
(related o c)-> 
(f a b c) == (g a b c)).
ir. 
Pose K1:= (arsimilar_S H H0). 
Pose K2 :=(arsimilar_S K1 H1). 
Exact (arsimilar_S K2 H2). 
Save.



Lemma arsimilar_arity4 : (t:E; k:t->nat; o:(object k); f,g:E4)
(arsimilar (region o) 2!(4) f g) ->
((a,b,c,d:E)
(related o a)->
(related o b) ->
(related o c)-> 
(related o d) ->
(f a b c d) == (g a b c d)).
ir. 
Pose K1:= (arsimilar_S H H0). 
Pose K2 :=(arsimilar_S K1 H1).
Pose K3 :=(arsimilar_S K2 H2). 
Exact (arsimilar_S K3 H3). 
Save.

Lemma arsimilar_arity5 : (t:E; k:t->nat; o:(object k); f,g:E5)
(arsimilar (region o) 2!(5) f g) ->
((a,b,c,d,e:E)
(related o a)->
(related o b) ->
(related o c)-> 
(related o d) ->
(related o e)->
(f a b c d e) == (g a b c d e)).
ir. 
Pose K1:= (arsimilar_S H H0). 
Pose K2 :=(arsimilar_S K1 H1).
Pose K3 :=(arsimilar_S K2 H2). 
Pose K4 :=(arsimilar_S K3 H3). 
Exact (arsimilar_S K4 H4). 
Save.





Tactic Definition notatac1 := 
Match Context With 
[|- (extract ?1 (createN ?2) ?3) == ? ] ->
Transitivity (?2 ?3); [sy; 
Apply (arsimilar_arity0 (extract_create_similar ?2 ?3))
| tv]
|
[|- (extract ?1 (createN ?2) ?3 ?4) ==(? ?4)] ->
Transitivity (?2 ?3 ?4); [sy; 
Apply (arsimilar_arity1 (extract_create_similar ?2 ?3))
| tv]
|
[|- (extract ?1 (createN ?2) ?3 ?4 ?5) ==(? ?4 ?5)] ->
Transitivity (?2 ?3 ?4 ?5); [sy; 
Apply (arsimilar_arity2 (extract_create_similar ?2 ?3))
| tv]
|
[|- (extract ?1 (createN ?2) ?3 ?4 ?5 ?6) ==(? ?4 ?5 ?6)] ->
Transitivity (?2 ?3 ?4 ?5 ?6); [sy; 
Apply (arsimilar_arity3 (extract_create_similar ?2 ?3))
| tv]
|
[|- (extract ?1 (createN ?2) ?3 ?4 ?5 ?6 ?7) ==(? ?4 ?5 ?6 ?7)] ->
Transitivity (?2 ?3 ?4 ?5 ?6 ?7); [sy; 
Apply (arsimilar_arity4 (extract_create_similar ?2 ?3))
| tv]
|
[|- (extract ?1 (createN ?2) ?3 ?4 ?5 ?6 ?7 ?8) ==(? ?4 ?5 ?6 ?7 ?8)] ->
Transitivity (?2 ?3 ?4 ?5 ?6 ?7 ?8); [sy; 
Apply (arsimilar_arity5 (extract_create_similar ?2 ?3))
| tv]
|
_->Fail. 




End Notation_gen.



Module Notation.

Module Basic.
Export Notation_gen.

(**** the following definition allows us to literally SPELL OUT elements of nota; the
dot i notation at the end lets us specify the arity *********************************)

Inductive nota : E := 
A_ : nota -> nota | H_ : nota -> nota | O_ : nota -> nota | U_ : nota -> nota | 
B_ : nota -> nota | I_ : nota -> nota | P_ : nota -> nota | V_ : nota -> nota | 
C_ : nota -> nota | J_ : nota -> nota | Q_ : nota -> nota | W_ : nota -> nota | 
D_ : nota -> nota | K_ : nota -> nota | R_ : nota -> nota | X_ : nota -> nota | 
E_ : nota -> nota | L_ : nota -> nota | S_ : nota -> nota | Y_ : nota -> nota | 
F_ : nota -> nota | M_ : nota -> nota | T_ : nota -> nota | Z_ : nota -> nota | 
G_ : nota -> nota | N_ : nota -> nota | 
dot : nat -> nota.

Fixpoint arity [k:nota] : nat := 
<[k:nota]nat>
Cases k of
(dot i) => i |
(A_ m) => (arity m) | 
(B_ m) => (arity m) | 
(C_ m) => (arity m) | 
(D_ m) => (arity m) | 
(E_ m) => (arity m) | 
(F_ m) => (arity m) | 
(G_ m) => (arity m) | 
(H_ m) => (arity m) | 
(I_ m) => (arity m) | 
(J_ m) => (arity m) | 
(K_ m) => (arity m) | 
(L_ m) => (arity m) | 
(M_ m) => (arity m) | 
(N_ m) => (arity m) | 
(O_ m) => (arity m) | 
(P_ m) => (arity m) | 
(Q_ m) => (arity m) | 
(R_ m) => (arity m) | 
(S_ m) => (arity m) | 
(T_ m) => (arity m) | 
(U_ m) => (arity m) | 
(V_ m) => (arity m) | 
(W_ m) => (arity m) | 
(X_ m) => (arity m) | 
(Y_ m) => (arity m) | 
(Z_ m) => (arity m) 
end.


Definition da := [op :nota](default_arity (arity op)). 

Syntactic Definition obj := (Notation_gen.object arity). 
Syntactic Definition extra := (extract arity). 


Definition mask : Prop -> E -> E := [P:Prop; x:E](Y P x emptyset).

Lemma mask_in : (P:Prop; x:E)P->(mask P x) == x. 
ir. uf mask. ap Y_if. am. tv. 
Save. 

Lemma mask_out : (P:Prop; x:E)(~P) -> (mask P x) == emptyset.
ir. uf mask. ap Y_if_not. am. tv.  
Save. 


(*** our first example is the basic notational element corresponding to the underlying
set of most common mathematical objects; having everybody share the same notation for
underlying set allows us to fix the general notion of Umorphism as a morphism between objects
which acts as a function on the underlying set (see the module Umorphism below) ****)

Syntactic Definition Underlying := (U_ (N_ (D_ (E_ (R_ (L_ (Y_ (I_ (N_ (G_ (dot (0)))))))))))).

Definition U := [x:E](extra x Underlying).

Lemma U_formula : (x:E)(U x) == (V (J (R Underlying) emptyset) x). 
ir. tv. 
Save.

Lemma related_U : (o:obj; x:E)(related o x) ->(related o (U x)).
ir.
uhg. rw U_formula. ap region_value. am.
Save.



End Basic. 


Module Algebraic.
Export Basic.


Syntactic Definition Plus := (P_ (L_ (U_ (S_ (dot (2)))))). 
Syntactic Definition Times := (T_ (I_ (M_ (E_ (S_ (dot (2))))))).
Syntactic Definition Mult := (M_ (U_ (L_ (T_ (dot (2)))))).
Syntactic Definition Scalars := (S_ (C_ (A_ (L_ (A_ (R_ (S_ (dot (0))))))))).
Syntactic Definition Index := (I_ (N_ (D_ (E_ (X_ (dot (0))))))).
Syntactic Definition Degree := (D_ (E_ (G_ (R_ (E_ (E_ (dot (2)))))))).


Definition plus' := [x,a,b:E](extra x Plus a b).
Definition times' := [x,a,b:E](extra x Times a b).
Definition mult' := [x,a,b:E](extra x Mult a b).
Definition scalars := [x:E](extra x Scalars). 
Definition index := [x:E](extra x Index).
Definition degree' := [x,a,b:E](extra x Degree a b).


Definition times := [a,x,y:E](mask (A (inc x (U a)) (inc y (U a))) (times' a x y)).

Definition plus := [a,x,y:E](mask (A (inc x (U a)) (inc y (U a))) (plus' a x y)).

Definition mult := [a,x,y:E](mask (A (inc x (U (scalars a))) (inc y (U a))) (mult' a x y)).

Definition degree := [a,i,x:E]
(A (inc i (U (index a)))
(A (inc x (U a))
   (nonempty (degree' a i x))
)).

Lemma times_prime : (a,x,y:E)(inc x (U a)) -> (inc y (U a)) -> (times a x y) == (times' a x y).
ir. uf times. ap mask_in. ee; am.
Save.

Lemma plus_prime :(a,x,y:E)(inc x (U a)) -> (inc y (U a)) -> (plus a x y) == (plus' a x y).
ir. uf plus. ap mask_in. ee; am.
Save.

Lemma mult_prime : (a,x,y:E)(inc x (U (scalars a))) -> (inc y (U a)) -> (mult a x y) == (mult' a x y).
ir. uf mult. ap mask_in. ee; am.
Save.

Lemma degree_prime : (a,i,x:E)(inc i (U (index a))) -> (inc x (U a)) -> (degree a i x) == (nonempty (degree' a i x)).
ir. uf degree. ap iff_eq; ir; ee; am.
Save. 


Lemma times_eq : (a,b:E)(U a) == (U b) -> ((x,y:E)(inc x (U a)) -> (inc y (U a)) -> (times a x y) == (times b x y))
-> (times a) == (times b).
ir.
ap arrow_extensionality; Intro x. ap arrow_extensionality; Intro y. Apply by_cases with (inc x (U a)).
ir. Apply by_cases with (inc y (U a)). ir. ap H0; am. ir. uf times.
rw mask_out. rw mask_out. tv. uf not; ir. ap H2. ee. rw H; am. uf not; ir.
ap H2. ee; am. ir. uf times. rw mask_out. rw mask_out. tv. uf not; ir.
ap H1. rw H; ee; am. uf not; ir. ap H1. ee; am.
Save.

Lemma plus_eq : (a,b:E)(U a) == (U b) -> ((x,y:E)(inc x (U a)) -> (inc y (U a)) -> (plus a x y) == (plus b x y))
-> (plus a) == (plus b).
ir.
ap arrow_extensionality; Intro x. ap arrow_extensionality; Intro y. Apply by_cases with (inc x (U a)).
ir. Apply by_cases with (inc y (U a)). ir. ap H0; am. ir. uf plus.
rw mask_out. rw mask_out. tv. uf not; ir. ap H2. ee. rw H; am. uf not; ir.
ap H2. ee; am. ir. uf plus. rw mask_out. rw mask_out. tv. uf not; ir.
ap H1. rw H; ee; am. uf not; ir. ap H1. ee; am.
Save.

Lemma mult_eq : (a,b:E)(U a) == (U b) -> (scalars a) == (scalars b) 
-> ((x,y:E)(inc x (U (scalars a))) -> (inc y (U a)) -> (mult a x y) == (mult b x y))
-> (mult a) == (mult b).
ir.
ap arrow_extensionality; Intro x. ap arrow_extensionality; Intro y. Apply by_cases with (inc x (U (scalars a))).
ir. Apply by_cases with (inc y (U a)). ir.  ap H1; am. ir. uf mult. rw mask_out.
rw mask_out; tv. uf not; ir. ap H3. rw H; ee; am. uf not; ir. ap H3.
ee; am. ir. uf mult. rw mask_out. rw mask_out; tv. uf not; ir. ap H2; rw H0; ee; am.
uf not; ir. ap H2; ee; am.
Save.

Lemma degree_eq : (a,b:E)(U a) ==(U b) -> (index a) == (index b) -> 
((i,x:E)(inc i (U (index a))) -> (inc x (U a)) -> (degree a i x) == (degree b i x)) ->
(degree a) == (degree b).
ir.
ap arrow_extensionality; Intro i. ap arrow_extensionality; Intro x.
Apply by_cases with (inc i (U (index a))). ir. Apply by_cases with (inc x (U a)).
ir. ap H1; am. ir. ap iff_eq. ir. uh H4; ee. Assert False.
ap H3. am. Elim H7. ir. Assert False. uh H4; ee. ap H3. rw H. am.
Elim H5. ir. ap iff_eq; ir. Assert False. ap H2. uh H3; ee; am.
Elim H4. Assert False. ap H2. rw H0. uh H3; ee; am. Elim H4.
Save. 

Lemma degree_addl : (a,i,x:E)(degree a i x) == 
(A (inc i (U (index a))) 
(A (inc x (U a))
   (degree a i x)
)).
ir.
ap iff_eq; ir. dj. uh H; ee; am. uh H; ee; am. am. ee; am.
Save. 

Section def. 
Variables x, v_scalars, v_index:E.
Variables v_plus, v_times, v_mult: E2.
Variable v_degree : E->E->Prop. 


Definition create_obj  :=[op :nota]
<[op :nota](arity_type (arity op))>Cases op of
(U_ (N_ (D_ (E_ (R_ (L_ (Y_ (I_ (N_ (G_ (dot (0)))))))))))) => x |
(S_ (C_ (A_ (L_ (A_ (R_ (S_ (dot (0))))))))) => v_scalars |
(I_ (N_ (D_ (E_ (X_ (dot (0))))))) => v_index |
(P_ (L_ (U_ (S_ (dot (2)))))) => v_plus |
(T_ (I_ (M_ (E_ (S_ (dot (2))))))) => v_times |
(M_ (U_ (L_ (T_ (dot (2)))))) => v_mult |
(D_ (E_ (G_ (R_ (E_ (E_ (dot (2)))))))) => v_degree |
u => (da u)
end. 

Definition create_ens := 
(createN create_obj).

Lemma related_obj : (a:E)(inc a x) -> (related create_obj a).
ir. sub_relate 'Underlying. am. 
Save. 

Lemma scalars_related_obj : (a:E)(inc a (U v_scalars)) -> 
(related create_obj a).
ir.
Remind '(region_preserves create_obj Scalars).
Assert (related create_obj (U v_scalars)). ap related_U. am.
uh H1. uhg.  ap '(region_preserves_sub H1). am.
Save. 

Lemma index_related_obj : (a:E)(inc a (U v_index)) -> 
(related create_obj a).
ir.
Remind '(region_preserves create_obj Index).
Assert (related create_obj (U v_index)). ap related_U. am.
uh H1. uhg.  ap '(region_preserves_sub H1). am.
Save. 

Lemma U_rw : (U create_ens) == x.
ir; uf U; uf create_ens. notatac1; am. 
Save. 

Lemma scalars_rw : (scalars create_ens) == v_scalars.
ir; uf scalars; uf create_ens. notatac1; am. 
Save. 

Lemma index_rw : (index create_ens) == v_index.
ir; uf index; uf create_ens. notatac1; am. 
Save. 

Lemma times_rw : (a,b:E)(inc a x)->(inc b x) ->
(times create_ens a b) == (v_times a b).
ir.
rw times_prime. uf times'; uf create_ens. notatac1; ap related_obj; am.
rw U_rw. am. rw U_rw. am.
Save.

Lemma plus_rw : (a,b:E)(inc a x)->(inc b x) ->
(plus create_ens a b) == (v_plus a b).
ir.
rw plus_prime. uf plus'; uf create_ens. notatac1; ap related_obj; am.
rw U_rw. am. rw U_rw. am.
Save.


Lemma mult_rw : (a,b:E)(inc a (U v_scalars)) -> (inc b x) ->
(mult create_ens a b) == (v_mult a b). 
ir.
rw mult_prime. uf mult'; uf create_ens. notatac1. ap scalars_related_obj.
am. ap related_obj. am. rw scalars_rw. am. rw U_rw. am.
Save.

Lemma degree_rw : (i,a:E)(inc i (U v_index)) -> (inc a x) ->
(degree create_ens i a) == (v_degree i a). 
ir.
rw degree_prime. uf degree'; uf create_ens.
Assert (extract arity (createN create_obj) Degree i a)==(v_degree i a).
notatac1. ap index_related_obj. am. ap related_obj. am. rw H1.
ap iff_eq; ir. nin H2. Exact (B H2). sh '(R H2). ap R_inc.
rw index_rw. am. rw U_rw; am.
Save.



End def. 

Definition like := [a:E](create_ens (U a) (scalars a) (index a) (plus a) (times a) (mult a) (degree a)) == a.

Definition same := [a,b:E]
(A (U a) == (U b)
(A (scalars a) == (scalars b)
(A (index a) == (index b)
(A (plus a) == (plus b)
(A (times a) == (times b)
(A (mult a) == (mult b)
   (degree a) == (degree b)
)))))).

Lemma show_same : (a,b:E)(U a) == (U b) -> (scalars a) == (scalars b) -> (index a) == (index b) ->
((x,y:E)(inc x (U a)) -> (inc y (U a)) -> (plus a x y) == (plus b x y)) ->
((x,y:E)(inc x (U a)) -> (inc y (U a)) -> (times a x y) == (times b x y)) ->
((x,y:E)(inc x (U (scalars a))) -> (inc y (U a)) -> (mult a x y) == (mult b x y)) ->
((i,x:E)(inc i (U (index a))) -> (inc x (U a)) -> (degree a i x) == (degree b i x)) ->
(same a b).
ir. 
uhg; dj. am. am. am. ap plus_eq; am. ap times_eq; am. 
ap mult_eq; am. ap degree_eq;  am. 
Save. 




Lemma like_same_eq : (a,b:E)(like a) -> (like b) -> (same a b) -> a == b.
ir. uh H. uh H0. wr H. wr H0. uh H1; ee. rw H1. 
rw H2. rw H3. rw H4. rw H5. rw H6. rw H7. tv. 
Save.

Lemma create_same : (a:E)(same a (create_ens (U a) (scalars a) (index a) 
(plus a) (times a) (mult a) (degree a))).
ir. 
ap show_same; ir.  rw U_rw. tv. rw scalars_rw; tv. 
rw index_rw; tv. 
rw plus_rw. tv. am. am. 
rw times_rw. tv. am. am.  
rw mult_rw. tv. am. am.  
rw degree_rw. tv. am. am.  
Save. 


Lemma create_like : (a:E)(like (create_ens (U a) (scalars a) (index a) 
(plus a) (times a) (mult a) (degree a))).
ir.
LetTac K:= (create_ens (U a) (scalars a) (index a)
(plus a) (times a) ( mult a) (degree a)). 
uhg.  Assert (same a K). uf K; ap create_same. 
uh H; ee. wr H; wr H0; wr H1; wr H2; wr H3; wr H4; wr H5. tv. 
Save. 



End Algebraic. 




Module Categorical.
Export Basic. 

Syntactic Definition Objects := (O_ (B_ (J_ (E_ (C_ (T_ (S_ (dot (0))))))))).
Syntactic Definition Morphisms := (M_ (O_ (R_ (P_ (H_ (I_ (S_ (M_ (S_ (dot (0))))))))))).
Syntactic Definition Csource := (C_ (S_ (O_ (U_ (R_ (C_ (E_ (dot (1))))))))).
Syntactic Definition Ctarget := (C_ (T_ (A_ (R_ (G_ (E_ (T_ (dot (1))))))))).
Syntactic Definition Comp := (C_ (O_ (M_ (P_ (dot (2)))))).
Syntactic Definition Id := (I_ (D_ (dot (1)))).
Syntactic Definition Covers := (C_ (O_ (V_ (E_ (R_ (S_ (dot (1)))))))).


Definition objects := [x:E](extra x Objects).
Definition morphisms := [x:E](extra x Morphisms).
Definition csource' := [x,a:E](extra x Csource a).
Definition ctarget' := [x,a:E](extra x Ctarget a). 
Definition comp' := [x,a,b:E](extra x Comp a b).
Definition id' := [x,a:E](extra x Id a).
Definition covers' := [x,a:E](extra x Covers a).


Definition ob := [a,x:E](inc x (objects a)). 
Definition mor := [a,u:E](inc u (morphisms a)). 


Definition srce := [a,u:E](mask (mor a u) (csource' a u)).
Definition targ := [a,u:E](mask (mor a u) (ctarget' a u)).

Definition id := [a,x:E](mask (ob a x) (id' a x)).
Definition composable := [a,u,v:E]
(A (mor a u) 
(A (mor a v)
   (srce a u) == (targ a v)
)).  

Definition comp := [a,u,v:E](mask (composable a u v) (comp' a u v)).

Definition covers := [a,x:E](mask (ob a x) (covers' a x)).

Definition is_covering := [a,x,b:E]
(A (ob a x)
(A (sub b (morphisms x))
(A (u:E)(targ a u) == x
   (inc b (covers a x))
))). 


Lemma srce_prime : (a,u:E)(mor a u) -> (srce a u) == (csource' a u).
ir.
uf srce. ap mask_in. am. 
Save.

Lemma targ_prime : (a,u:E)(mor a u) -> (targ a u) == (ctarget' a u).
ir.
uf targ. ap mask_in. am. 
Save.

Lemma id_prime : (a,x:E)(ob a x) -> (id a x) == (id' a x).
ir.
uf id. ap mask_in. am. 
Save. 

Lemma comp_prime : (a,u,v:E)(composable a u v) -> 
(comp a u v) == (comp' a u v).
ir.
uf comp. ap mask_in. am. 
Save. 

Lemma covers_prime : (a,x:E)(ob a x) -> (covers a x) == (covers' a x).
ir.
uf covers. ap mask_in. am. 
Save. 

Lemma srce_eq : (a,b:E)(morphisms a) == (morphisms b) ->
((u:E)(mor a u) -> (srce a u) == (srce b u)) -> (srce a) == (srce b).
ir. 
ap arrow_extensionality; ir. Apply by_cases with (mor a a0); ir. 
ap H0. am. uf srce. 
rw mask_out. rw mask_out. tv. uf mor. wr H. am. am. 
Save. 

Lemma targ_eq : (a,b:E)(morphisms a) == (morphisms b) ->
((u:E)(mor a u) -> (targ a u) == (targ b u)) -> (targ a) == (targ b).
ir. 
ap arrow_extensionality; ir. Apply by_cases with (mor a a0); ir. 
ap H0. am. uf targ. 
rw mask_out. rw mask_out. tv. uf mor. wr H. am. am. 
Save. 

Lemma id_eq : (a,b:E)(objects a) == (objects b) ->
((x:E)(ob a x) -> (id a x) == (id b x)) -> (id a) == (id b).
ir. 
ap arrow_extensionality; ir. Apply by_cases with (ob a a0); ir. 
ap H0. am. uf id. 
rw mask_out. rw mask_out. tv. uf ob. wr H. am. am. 
Save. 

Lemma composable_eq : (a,b:E)(morphisms a) == (morphisms b) ->
(srce a) == (srce b) -> (targ a) == (targ b) -> (composable a) ==
(composable b).
ir. 
ap arrow_extensionality; ir. ap arrow_extensionality; ir.
ap iff_eq; ir. uh H2; uhg; ee. uhg; wr H; am. 
uhg; wr H; am. wr H0. wr H1. am. 
uh H2; uhg; ee. uhg; rw H; am. 
uhg; rw H; am. rw H0. rw H1. am. 
Save.

Lemma comp_eq : (a,b:E)(composable a) == (composable b) ->
((u,v:E)(composable a u v) -> (comp a u v) == (comp b u v)) ->
(comp a) == (comp b).
ir. 
ap arrow_extensionality; ir. ap arrow_extensionality; ir.
Apply by_cases with (composable a a0 a1); ir. ap H0; am. 
uf comp. rw mask_out. rw mask_out; tv.
wr H. am. am. 
Save. 

Lemma covers_eq : (a,b:E)(objects a) == (objects b) ->
((x:E)(ob a x) -> (covers a x) == (covers b x)) -> 
(covers a) == (covers b).
ir. 
ap arrow_extensionality; ir. Apply by_cases with (ob a a0); ir. 
ap H0. am. uf covers. 
rw mask_out. rw mask_out. tv. uf ob. wr H. am. am. 
Save. 

Section def.
Variables v_objects, v_morphisms:E.
Variables v_csource, v_ctarget :E1.
Variable v_comp : E2.
Variables v_id, v_covers: E1.



Definition create_obj  :=[op :nota]
<[op :nota](arity_type (arity op))>Cases op of
(U_ (N_ (D_ (E_ (R_ (L_ (Y_ (I_ (N_ (G_ (dot (0)))))))))))) => v_morphisms |
(O_ (B_ (J_ (E_ (C_ (T_ (S_ (dot (0))))))))) => v_objects |
(M_ (O_ (R_ (P_ (H_ (I_ (S_ (M_ (S_ (dot (0))))))))))) => v_morphisms |
(C_ (S_ (O_ (U_ (R_ (C_ (E_ (dot (1))))))))) => v_csource |
(C_ (T_ (A_ (R_ (G_ (E_ (T_ (dot (1))))))))) => v_ctarget |
(C_ (O_ (M_ (P_ (dot (2))))))=> v_comp |
(I_ (D_ (dot (1)))) => v_id|
(C_ (O_ (V_ (E_ (R_ (S_ (dot (1)))))))) => v_covers|
u => (da u)
end. 

Definition create_ens := 
(createN create_obj).

Lemma ob_related_obj : (a:E)(inc a v_objects) -> 
(related create_obj a).
ir. sub_relate 'Objects. am. 
Save. 

Lemma mor_related_obj : (a:E)(inc a v_morphisms) -> 
(related create_obj a).
ir. sub_relate 'Morphisms. am. 
Save. 

Lemma U_rw : (U create_ens) == v_morphisms.
ir; uf U; uf create_ens. notatac1; am. 
Save. 

Lemma objects_rw : (objects create_ens) == v_objects.
ir; uf objects; uf create_ens. notatac1; am. 
Save. 

Lemma morphisms_rw : (morphisms create_ens) == v_morphisms.
ir; uf morphisms; uf create_ens. notatac1; am. 
Save. 

Lemma mor_rw: (a:E)(mor create_ens a) == (inc a v_morphisms).
ir. 
uf mor. rw morphisms_rw. tv. 
Save. 

Lemma ob_rw : (a:E)(ob create_ens a) == (inc a v_objects).
ir. 
uf ob. rw objects_rw. tv. 
Save. 


Lemma srce_rw : (a:E)(inc a v_morphisms) ->
(srce create_ens a) == (v_csource a).
ir. rw srce_prime.  
uf csource'; uf create_ens. 
notatac1; ap mor_related_obj; am. 
uhg. rw morphisms_rw. am. 
Save.

Lemma targ_rw : (a:E)(inc a v_morphisms) ->
(targ create_ens a) == (v_ctarget a).
ir. rw targ_prime.  
uf ctarget'; uf create_ens. notatac1; ap mor_related_obj; am. 
uhg. rw morphisms_rw. am. 
Save.



Lemma comp_rw : (a,b:E)(inc a v_morphisms)->(inc b v_morphisms) ->
(v_csource a) == (v_ctarget b) -> 
(comp create_ens a b) == (v_comp a b).
ir.
rw comp_prime. 
uf comp'; uf create_ens. notatac1; ap mor_related_obj; am. 
uhg; ee. rw mor_rw; am. rw mor_rw; am. rw srce_rw.
rw targ_rw. am. am. am.
Save.



Lemma id_rw : (a:E)(inc a v_objects) ->
(id create_ens a) == (v_id a).
ir. rw id_prime. 
uf id'; uf create_ens. notatac1; ap ob_related_obj; am. 
rw ob_rw; am. 
Save.

Lemma covers_rw : (a:E)(inc a v_objects) ->
(covers create_ens a) == (v_covers a).
ir. rw covers_prime. 
uf covers'; uf create_ens. notatac1; ap ob_related_obj; am. 
rw ob_rw; am. 
Save.

End def. 


Definition like := [a:E](create_ens 
(objects a) (morphisms a) (srce a) (targ a) 
(comp a) (id a) (covers a)) == a.

Definition same := [a,b:E]
(A (objects a) == (objects b)
(A (morphisms a) == (morphisms b)
(A (ob a) == (ob b)
(A (mor a) == (mor b)
(A (srce a) == (srce b)
(A (targ a) == (targ b)
(A (composable a) == (composable b)
(A (comp a) == (comp b)
(A (id a) == (id b)
   (covers a) == (covers b)
))))))))).

Lemma show_same : (a,b:E)(objects a) == (objects b) -> 
(morphisms a) == (morphisms b) ->
((u:E)(mor a u) -> (srce a u) == (srce b u)) ->
((u:E)(mor a u) ->  (targ a u) == (targ b u)) ->
((u,v:E)(composable a u v) -> (comp a u v) == (comp b u v)) ->
((x:E)(ob a x) ->  (id a x) == (id b x)) ->
((x:E)(ob a x) ->  (covers a x) == (covers b x)) ->
(same a b).
ir. 
uhg; dj. am. am.
uf ob; rw H; tv. 
uf mor; rw H0; tv. ap srce_eq. am. am. 
ap targ_eq; am. ap composable_eq; am. ap comp_eq; am. 
ap id_eq; am. ap covers_eq; am. 
Save. 




Lemma like_same_eq : (a,b:E)(like a) -> (like b) -> 
(same a b) -> a == b.
ir. uh H. uh H0. wr H. wr H0. uh H1; ee.  
rw H1; rw H2; rw H5; rw H6; rw H8; rw H9; rw H10.  tv. 
Save.

Lemma create_same : (a:E)(same a 
(create_ens (objects a) (morphisms a) (srce a) 
(targ a) (comp a) (id a) (covers a))).
ir. 
ap show_same; ir.  
rw objects_rw; tv. 
rw morphisms_rw; tv. 
rw srce_rw. tv. am. 
rw targ_rw. tv. am. 
uh H; ee. 
rw comp_rw. tv. am. am. am. 
rw id_rw. tv. am. 
rw covers_rw. tv. am. 
Save. 


Lemma create_like : (a:E)(like 
(create_ens (objects a) (morphisms a) (srce a) 
(targ a) (comp a) (id a) (covers a))). 
ir.
LetTac K:= (create_ens (objects a) (morphisms a) (srce a) 
(targ a) (comp a) (id a) (covers a)).
uhg.  Assert (same a K). uf K; ap create_same. 
uh H; ee. wr H; wr H0; wr H3; wr H4; wr H6; wr H7; wr H8. tv. 
Save. 





End Categorical. 






Module Order_notation.
Export Basic.

Syntactic Definition Less_Than := (L_ (E_ (S_ (S_ (T_ (H_ (A_ (N_ (dot (2)))))))))).

Definition less_than := [x,a,b:E](extra x Less_Than a b).



Definition leq := [x,a,b:E]
(A (inc a (U x)) 
(A (inc b (U x))
   (nonempty (less_than x a b))
)).

Definition lt := [a,x,y:E](A (leq a x y) ~(x == y)).

Section Construction.
Variables x : E; lq : E->E->Prop. 

Definition create_obj  := [op :nota]
<[op :nota](arity_type (arity op))>Cases op of
(U_ (N_ (D_ (E_ (R_ (L_ (Y_ (I_ (N_ (G_ (dot (0)))))))))))) => x |
(L_ (E_ (S_ (S_ (T_ (H_ (A_ (N_ (dot (2)))))))))) => lq |
u => (da u)
end. 



Definition create := 
(Notation_gen.createN create_obj).

Lemma related_obj: (a:E)(inc a x) -> (related create_obj a).
ir. sub_relate 'Underlying. am. 
Save. 

Lemma  underlying_create: (U create) == x. 
ir; uf U; uf create. notatac1. 
Save. 

Lemma less_than_rw : (a,b:E)(inc a x) -> (inc b x)
-> (less_than create a b) == (lq a b).
ir; uf less_than; uf create. notatac1; ap related_obj; am. 
Save.


Lemma leq_create : (a,b:E)(inc a x) -> (inc b x)
-> (leq create a b) == (lq a b).
ir. uf leq.
rw less_than_rw.
ap iff_eq; ir. ee. nin H3. Exact (B H3). 
rw underlying_create. ee. am. am.
sh '(R H1). 
ap R_inc. am. am. 
Save.

Lemma leq_create_all : (a,b:E)
(leq create a b) ==
(A (inc a x) (A (inc b x) (lq a b))).
ir. ap iff_eq. 
uf leq. rw underlying_create. ir; ee. am. am.
rwi less_than_rw H1. nin H1. Exact (B H1). am.
am. ir. rw leq_create; ee; am. 
Save.

End Construction. 



Definition like := [a:E]a==(create (U a) (leq a)).

Lemma create_like : (a:E)(like (create (U a) (leq a))). 
ir. 
uf like. 
Assert (U (create (U a) (leq a))) == (U a). 
ap underlying_create. rw H. 
Assert (leq (create (U a) (leq a))) == (leq a). 
ap arrow_extensionality; ir. 
ap arrow_extensionality; ir. 
ap iff_eq; ir. rwi leq_create_all H0; ee; am. 
ufi leq H0. ee. rw leq_create_all; ee. am. 
am. uf leq; ee; am. 
rw H0. tv. 
Save. 

Recursive Tactic Definition cluc := 
Match Context With 
[id1 : ?1 |- ?] -> rwi underlying_create id1; cluc
|
[|- ?1] -> rw underlying_create
| _-> Idtac.

Lemma leq_create_then : (a:E; l:E->E->Prop; x,y:E)
(leq (create a l) x y) -> 
(A (inc x a) (A (inc y a) (l x y))).
ir. rwi leq_create_all H. am. Save.



Lemma leq_create_if :  (a:E; l:E->E->Prop; x,y:E)
(inc x a) -> (inc y a) ->(l x y) -> (leq (create a l) x y).
ir. rw leq_create; am. 
Save. 


End Order_notation.




End Notation. 


Module Umorphism.

Export Notation.Basic. 



Syntactic Definition Source := (S_ (O_ (U_ (R_ (C_ (E_ (dot (0)))))))).
Syntactic Definition Target := (T_ (A_ (R_ (G_ (E_ (T_ (dot (0)))))))).
Syntactic Definition Mapping := (M_ (A_ (P_ (P_ (I_ (N_ (G_ (dot (1))))))))).


Definition source := [x:E](extra x Source). 
Definition target := [x:E](extra x Target). 
Definition mapping := [x,a:E](extra x Mapping a).



Syntactic Definition ev := mapping. 


Definition pre_create_obj := [x,y:E; f:E1; op : nota]
<[op :nota](arity_type (arity op))>Cases op of
(U_ (N_ (D_ (E_ (R_ (L_ (Y_ (I_ (N_ (G_ (dot (0)))))))))))) => (U x)|
(S_ (O_ (U_ (R_ (C_ (E_ (dot (0)))))))) => x|
(T_ (A_ (R_ (G_ (E_ (T_ (dot (0)))))))) => y|
(M_ (A_ (P_ (P_ (I_ (N_ (G_ (dot (1))))))))) => f|
u => (da u)
end. 


Section Construction.
Variables x,y:E; f:E1.

Definition create_obj := [op: nota](pre_create_obj x y [a:E](mask (inc a (U x)) (f a)) op).


Definition create := 
(createN create_obj).

Lemma related_obj: (a:E)(inc a (U x)) -> (related create_obj a).
ir. sub_relate 'Underlying. am. 
Save. 

Lemma source_create : (source create) == x. 
ir; uf source; uf create; uf create_obj. 
notatac1; am. 
Save. 

Lemma target_create : (target create) == y. 
ir; uf target; uf create; uf create_obj. notatac1; am. 
Save. 

Lemma ev_create : (a:E)(inc a (U x)) ->(ev create a) == (f a).
ir; uf mapping; uf create; uf create_obj. notatac1. 
ap related_obj; am. Transitivity (mask (inc a (U x)) (f a)).
tv. ap mask_in. am. 
Save. 


Lemma mapping_not_rw : (a:E)(inc a (region create_obj)) ->
~(inc a (U x)) -> (ev create a) ==
emptyset.
ir; uf mapping; uf create; uf create_obj. 
LetTac g:= [a:E]emptyset.
Transitivity (g a). notatac1.
am. Transitivity (mask (inc a (U x)) (f a)). tv. 
Change (mask (inc a (U x)) (f a)) == emptyset. 
ap mask_out. am. tv. 
Save. 

End Construction.




Lemma create_extens : (x,x',y,y':E; f,g:E1)
x==x' -> y == y' ->((a:E)(inc a (U x)) -> 
(f a) == (g a))-> (create x y f) == (create x' y' g).
ir.
uf create. uf create_obj.
LetTac ff:=[a:E](mask (inc a (U x)) (f a)). LetTac gg:=[a:E](mask (inc a (U x')) (g a)).
Assert ff==gg. ap arrow_extensionality; ir. Apply by_cases with (inc a (U x)).
ir. uf ff; uf gg. rw mask_in. rw mask_in. ap H1; am. wr H; am. am. ir.
uf ff; uf gg. rw mask_out. rw mask_out; tv. wr H; am. am. rw H2. rw H. rw H0. tv.
Save.



Definition realizes := [x,y:E; f:E1; a:E]
(A (source a) == x
(A (target a) == y
   (z:E)(inc z (U x)) -> (ev a z) == (f z)
)).

Definition property := [x,y:E; f: E1]
(Transformation.axioms (U x) (U y) f).

Definition like := [a:E](create (source a) (target a) (ev a)) == a.


Lemma create_like : (x,y:E; f:E1)(like (create x y f)).
ir.
uf like. ap create_extens. ap source_create. 
ap target_create. ir. ap ev_create. rwi source_create H. am. 
Save. 



Lemma create_realizes : (x,y:E; f:E1)(realizes x y f (create x y f)).
ir.
Pose source_create.
Pose target_create.
Pose ev_create.
Unfold realizes; xe.
Save.


Lemma realizes_like_eq : (x,y:E; f:E1; a:E)(like a) -> 
(realizes x y f a) ->
(create x y f) == a.
ir. ufi like H. wr H. ap create_extens; 
ufi realizes H0; xd. ir; sy; ap H2; am. 
Save. 


Definition axioms := [a:E](property (source a) (target a) (ev a)).
Definition strong_axioms := [a:E](A (axioms a) (like a)).

Lemma axioms_from_strong : (a:E)(strong_axioms a) -> (axioms a).
ir. Unfold strong_axioms in H; xe.
Save.

Lemma  create_strong_axioms : (x,y:E; f:E1)(property x y f) -> (strong_axioms (create x y f)).
ir.
Unfold strong_axioms.
ee.
Unfold axioms.
rw source_create.
rw target_create.
uf property.
uf Transformation.axioms.
ir.
rw ev_create. 
ufi property  H.
ufi Transformation.axioms  H.
ap H.
am.

am.

ap create_like.
Save.

Lemma create_axioms: (x,y:E; f:E1)(property x y f) -> (axioms (create x y f)).
ir. ap axioms_from_strong. ap create_strong_axioms; au.
Save.

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

Definition compose := [a,b:E](create (source b) (target a) [y:E](ev a (ev b y))).

Lemma identity_strong_axioms : (x:E)(strong_axioms (identity x)).
ir.
uf identity.
ap create_strong_axioms.
uf property.
ap Transformation.identity_axioms.
Save.

Lemma identity_axioms : (x:E)(axioms (identity x)).
ir. Remind '(identity_strong_axioms x). 
ufi strong_axioms H; xe.
Save.


Lemma left_identity : (a:E)(strong_axioms a) -> (compose (identity (target a)) a) == a.
ir.
Unfold compose.
ap realizes_like_eq.
Unfold strong_axioms in H; xe.

Unfold realizes.
xe.
Unfold identity; Rewrite -> target_create.
tv.

ir.
Unfold identity.
Rewrite -> ev_create.
tv.

Unfold strong_axioms in H.
xd.
Save.


Lemma right_identity : (a:E)(strong_axioms a) -> (compose a (identity (source a))) == a.
ir.
Unfold compose.
ap realizes_like_eq.
Unfold strong_axioms in H; xe.

Unfold realizes.
xe.
Unfold identity; Rewrite -> source_create.
tv.

ir.
Unfold identity; Rewrite -> ev_create.
tv.

Unfold identity in H0; Rewrite -> source_create in H0.
am.
Save.

Lemma source_identity : (x:E)(source (identity x)) == x.
ir. Unfold identity; Rewrite -> source_create. tv.
Save.

Lemma target_identity : (x:E)(target (identity x)) == x.
ir. Unfold identity; Rewrite -> target_create. tv.
Save.

Lemma ev_identity : (x,y:E)(inc y (U x)) -> (ev (identity x) y) == y.
ir. Unfold identity; Rewrite -> ev_create; au.
Save.

Lemma source_compose : (a,b:E)(source (compose a b)) == (source b).
ir. Unfold compose; Rewrite source_create; tv.
Save.

Lemma target_compose : (a,b:E)(target (compose a b)) == (target a).
ir. Unfold compose; Rewrite target_create; tv.
Save.

Lemma ev_compose : (a,b,y:E)(inc y (U (source b))) -> (ev (compose a b) y) == 
(ev a (ev b y)).
ir. Unfold compose; Rewrite ev_create; au.
Save.

Definition composable := [a,b:E]
(A (axioms a)
(A (axioms b)
   (source a) == (target b)
)).



Lemma compose_strong_axioms : (a,b:E)(composable a b) -> (strong_axioms (compose a b)).
ir.
Unfold strong_axioms.
xe.
Unfold axioms.
Rewrite -> source_compose.
Rewrite -> target_compose.
Unfold property.
Unfold Transformation.axioms.
ir.
Rewrite -> ev_compose.
Unfold composable in H.
xe.
Unfold axioms in H.
Unfold property in H.
Unfold Transformation.axioms in H.
ap H.
Unfold axioms in H1.
Unfold property in H1.
Unfold Transformation.axioms in H1.
Rewrite -> H2.
ap H1.
am.

am.

Unfold compose.
ap create_like.
Save.

Lemma compose_axioms : (a,b:E)(composable a b) -> (axioms (compose a b)).
ir. Pose K:= (compose_strong_axioms H). Unfold strong_axioms in (Type of K); xe.
Save. 

Lemma extens : (a,b:E)(strong_axioms a) -> (strong_axioms b) -> (source a) == (source b) ->
(target a) == (target b) -> ((x:E)(inc x (U (source a))) -> (inc x (U (source b))) -> (ev a x) == (ev b x)) 
-> a == b.
ir.
Unfold strong_axioms in H H0.
xe.
Unfold like in H5 H4.
Rewrite <- H5.
ap realizes_like_eq; au.
Unfold realizes.
xe.
ir.
sy; ap H3.
am.

Rewrite <- H1.
am.
Save.

Lemma associativity : (a,b,c:E)(composable a b) -> (composable b c) -> 
(compose (compose a b) c) == (compose a (compose b c)).
ir.
ap extens.
ap compose_strong_axioms.
Unfold composable.
xe.
ap compose_axioms; au.

Unfold composable in H0; xe.

Rewrite -> source_compose.
Unfold composable in H0; xe.

ap compose_strong_axioms.
Unfold composable; xe.
Unfold composable in H; xe.

ap compose_axioms.
am.

Rewrite -> target_compose.
Unfold composable in H; xe.

Repeat Rewrite -> source_compose.
tv.

Repeat Rewrite -> target_compose; tv.

ir.
Repeat Rewrite -> ev_compose.
tv.

Repeat Rewrite -> source_compose in H1.
am.

Rewrite -> source_compose in H2.
am.

Repeat Rewrite -> source_compose in H1.
Unfold composable in H0.
xe.
Rewrite -> H4.
ap H3.
am.

Repeat Rewrite -> source_compose in H1.
am.
Save.


Definition inclusion := [a,b:E](create a b [y:E]y).


Lemma inclusion_strong_axioms : (a,b:E)(sub (U a) (U b)) -> 
(strong_axioms (inclusion a b)).
ir.
Unfold inclusion.
ap create_strong_axioms.
Unfold property.
Unfold Transformation.axioms.
ir.
ap H; au.
Save.

Lemma inclusion_axioms : (a,b:E)(sub (U a) (U b)) -> 
(axioms (inclusion a b)).
ir. ap axioms_from_strong. ap inclusion_strong_axioms; au.
Save.


Definition injective := [u:E]
(A (axioms u)
   (Transformation.injective (U (source u)) (U (target u)) (ev u))
).

Lemma injective_rewrite : (u:E)(axioms u) -> (injective u) == 
((x,y:E)(inc x (U (source u))) -> (inc y (U (source u))) -> (ev u x) == (ev u y) -> x == y).
ir.
ap iff_eq; ir.
Unfold injective in H0.
xe.
Unfold Transformation.injective in H4.
xe. au.

Unfold injective; xe.
Unfold Transformation.injective; xe.
Save.

Lemma injective_compose_with : (u,v,w:E)(strong_axioms u) -> (strong_axioms v) ->
(injective w) -> (composable w u) -> (composable w v) ->
(compose w u) == (compose w v) -> u == v.
ir.
ap extens; au.
Transitivity (source (compose w u)).
Rewrite -> source_compose; au.

Rewrite -> H4.
Rewrite -> source_compose; au.

Unfold composable in H2 H3.
xe.
Transitivity (source w); au.

ir.
Unfold injective in H1.
xe.
Unfold Transformation.injective in H7.
xe.
ap H8.
Unfold strong_axioms in H.
xe.
Unfold axioms in H.
Unfold property in H.
Unfold composable in H2.
xe.
Rewrite -> H11.
ap H.
am.

Unfold composable in H3; xe.
Rewrite -> H10.
Unfold strong_axioms in v; xe. au.

Transitivity (ev (compose w u) x).
Rewrite -> ev_compose; au.

Rewrite -> H4.
Rewrite -> ev_compose; au.
Save. 

Definition surjective := [u:E]
(A (axioms u)
   (Transformation.surjective (U (source u)) (U (target u)) (ev u))
).

Lemma surjective_rewrite : (u:E)(axioms u) -> (surjective u) == 
((x:E)(inc x (U (target u))) -> (exists [y:E](A (inc y (U (source u))) (ev u y) == x))).
ir.
ap iff_eq; ir.
Unfold surjective in H0; xe.
Unfold Transformation.surjective in H2; xe. au.

Unfold surjective; xe.
Unfold Transformation.surjective; xe.
Save. 

Definition inverse := [u:E](create (target u) (source u) (Transformation.inverse (U (source u)) (ev u))).

Lemma surjective_inverse_axioms : (u:E)(surjective u) -> (strong_axioms (inverse u)).
ir.
Unfold strong_axioms; xe.
Unfold inverse.
ap create_axioms.
Unfold property.
ap Transformation.surjective_inverse_axioms.
Unfold surjective in H; xe.

Unfold inverse.
ap create_like.
Save. 

Lemma surjective_composable_left : (u:E)(surjective u) -> (composable (inverse u) u).
ir.
Unfold composable.
xe.
ap axioms_from_strong.
ap surjective_inverse_axioms; au.

Unfold surjective in H; xe.

Unfold inverse.
Rewrite -> source_create; tv.
Save.

Lemma surjective_composable_right : (u:E)(surjective u) -> (composable u (inverse u)).
ir.
Unfold composable; xe.
Unfold surjective in H; xe.

ap axioms_from_strong.
ap surjective_inverse_axioms; au.

Unfold inverse; Rewrite -> target_create; tv.
Save. 

Lemma surjective_inverse_right : (u:E)(surjective u) -> (compose u (inverse u)) == (identity (target u)).
ir.
Assert (axioms u).
Unfold surjective in H; xe.

ap extens.
ap compose_strong_axioms.
ap surjective_composable_right.
am.

ap identity_strong_axioms.

Rewrite -> source_compose.
Rewrite -> source_identity.
Unfold inverse; Rewrite -> source_create.
tv.

Rewrite -> target_compose.
Rewrite -> target_identity; tv.

ir.
Rewrite -> ev_compose.
Rewrite -> ev_identity.
Unfold inverse.
Rewrite -> ev_create.
Unfold surjective in H.
xe.
Rewrite -> source_identity in H2.
Pose (Transformation.surjective_inverse_right H3 H2).
ap e.

Rewrite -> source_identity in H2; am.

Rewrite -> source_identity in H2; am.

Rewrite -> source_compose in H1; am.
Save.

Definition bijective := [u:E]
(A (injective u) (surjective u)).

Lemma bijective_transformation_bijective : (u:E)(bijective u) -> (Transformation.bijective
(U (source u)) (U (target u)) (ev u)).
ir.
Unfold bijective in H; xe.
Unfold injective in H.
Unfold surjective in H0.
xe.
Unfold axioms in H.
Unfold property in H.
Unfold Transformation.bijective; xe.
Save. 

Lemma transformation_bijective_bijective : (u:E)(axioms u) -> (Transformation.bijective 
(U (source u)) (U (target u)) (ev u)) -> (bijective u).
ir.
Unfold Transformation.bijective in H0.
Unfold bijective.
xe.
Unfold injective; xe.

Unfold surjective; xe.
Save. 

Definition are_inverse := [u,v:E]
(A (composable u v) 
(A (composable v u)
(A (compose u v) == (identity (source v))
   (compose v u) == (identity (source u))
))).

Lemma inverse_symm : (u,v:E)(are_inverse u v) -> (are_inverse v u).
ir.
Unfold are_inverse.
Unfold are_inverse in H.
xe.
Save. 

Lemma inverse_unique : (u,v,w:E)(strong_axioms v) -> (strong_axioms w) ->
(are_inverse u v) -> (are_inverse u w) -> v == w.
ir.
Transitivity (compose v (identity (source v))).
sy.
ap right_identity.
am.

Unfold are_inverse in H1 H2; ee.
Assert (source v)==(target u).
Unfold composable in H4; xe.

Assert (source v)==(source w).
Rewrite -> H9.
Unfold composable in H3; xe.

Rewrite -> H10.
Rewrite <- H5.
Rewrite <- associativity.
Rewrite -> H8.
Assert (source u)==(target w).
Unfold composable in H2; xe.

Rewrite -> H11.
ap left_identity.
am.

am.

am.
Save. 

Definition has_inverse := [u:E](exists [v:E](are_inverse u v)).

Lemma are_inverse_transfo_inverse : (u,v:E)(are_inverse u v) ->
(Transformation.are_inverse (U (source u)) (U (target u)) (ev u) (ev v)).
ir.
Unfold Transformation.are_inverse.
Unfold are_inverse in H.
xe.
Unfold composable in H; xe.

Unfold composable in H H0; xe.
Rewrite <- H5.
Rewrite -> H6.
am.

ir.
Transitivity (ev (compose v u) x).
sy; ap ev_compose.
am.

Rewrite -> H2.
ap ev_identity.
am.

ir.
Assert (inc y (U (source v))).
Unfold composable in H0; xe.
Rewrite -> H5; am.

Transitivity (ev (compose u v) y).
Rewrite -> ev_compose.
tv.

am.

Rewrite -> H1.
Rewrite -> ev_identity.
tv.

am.
Save. 

Lemma inverse_bijective : (u,v:E)(are_inverse u v) -> (bijective u).
ir.
ap transformation_bijective_bijective.
Unfold are_inverse in H; xe.
Unfold composable in H; xe.

Apply Transformation.inverse_bijective with (ev v).
ap are_inverse_transfo_inverse.
am.
Save.

Lemma bijective_inverse : (u:E)(bijective u) -> (are_inverse u (inverse u)).
ir.
Unfold bijective in H; xe.
Pose (surjective_composable_left H0).
Pose (surjective_composable_right H0).
Pose (surjective_inverse_right H0).
Unfold are_inverse; ee. am. am. 
Unfold composable in (Type of c); ee. 
Rewrite -> H3.
ap e.

Apply injective_compose_with with u.
ap compose_strong_axioms; au.

ap identity_strong_axioms.

am.

Unfold composable.
ee.
Unfold injective in H; xe.

ap compose_axioms; au.

Rewrite -> target_compose.
Unfold composable in (Type of c0); xe.

Unfold composable; ee.
Unfold injective in H; xe.

ap identity_axioms.

Rewrite -> target_identity; tv.

Rewrite <- associativity.
Rewrite -> e.
ap extens.
ap compose_strong_axioms.
Unfold composable; ee.
ap identity_axioms.

Unfold injective in H; xe.

Rewrite -> source_identity.
tv.

ap compose_strong_axioms.
Unfold composable; ee.
Unfold injective in H; xe.

ap identity_axioms.

Rewrite -> target_identity; tv.

Rewrite -> source_compose.
Rewrite -> source_compose.
Rewrite -> source_identity; tv.

Repeat Rewrite -> target_compose.
Rewrite -> target_identity.
tv.

ir.
Repeat Rewrite -> ev_compose.
Repeat Rewrite -> ev_identity.
tv.

Rewrite -> source_compose in H2.
Rewrite -> source_identity in H2; am.

Unfold injective in H; ee.
Unfold axioms in H.
Unfold property in H; xe.
ap H.
Rewrite -> source_compose in H2.
Rewrite -> source_identity in H2.
am.

Rewrite -> source_compose in H2; am.

Rewrite -> source_compose in H2.
Rewrite -> source_identity in H2.
am.

am.

am.
Save.


Lemma bijective_has_inverse : (u:E)(bijective u) -> (has_inverse u).
ir. Unfold has_inverse. Apply exists_intro with (inverse u).
ap bijective_inverse; au.
Save. 


Lemma bijective_eq_has_inverse : (u:E)(bijective u) == (has_inverse u).
ir.
ap iff_eq; ir.
Unfold has_inverse.
Apply exists_intro with (inverse u).
ap bijective_inverse; au.

Unfold has_inverse in H.
nin H.
Apply inverse_bijective with x; au.
Save.

Lemma bijective_eq_inverse : (u:E)(bijective u) == (are_inverse u (inverse u)).
ir.
ap iff_eq; ir.
ap bijective_inverse.
am.

Apply inverse_bijective with (inverse u); am.
Save. 

Lemma has_inverse_eq_inverse : (u:E)(has_inverse u) == (are_inverse u (inverse u)).
ir.
Rewrite <- bijective_eq_inverse.
Rewrite -> bijective_eq_has_inverse.
tv.
Save. 


Definition Uempty_obj := [i:nota]
Cases i of 
u => (da u) end.

Definition Uempty := (Notation_gen.createN Uempty_obj). 


Definition Uempty_initial := [a:E](inclusion Uempty a).

Lemma underlying_Uempty : (U Uempty) == emptyset.
uf Uempty. uf U. notatac1. 
Save. 

Lemma Uempty_initial_strong_axioms : (a:E)(strong_axioms (Uempty_initial a)).
ir. uf Uempty_initial. ap inclusion_strong_axioms. rw underlying_Uempty. uf sub; ir.
nin H. Elim x0. Save. 

Lemma use_axioms : (u,x,y,a:E)(Umorphism.axioms u) -> (source u) == x -> (target u) == y ->
(inc a (U x)) -> (inc (ev u a) (U y)).
ir. cx. wr H1. ap H. rw H0. am.
Save. 

Recursive Tactic Definition clst := 
Match Context With 
[id1 : ?1 |- ? ] -> First 
[Rewrite source_create in id1; clst 
| Rewrite target_create in id1; clst
| Rewrite source_identity in id1; clst
| Rewrite target_identity in id1; clst
| Rewrite source_compose in id1; clst
| Rewrite target_compose in id1; clst]
|
[|- ? ] -> First 
[Rewrite source_create; clst 
| Rewrite target_create; clst
| Rewrite source_identity; clst
| Rewrite target_identity; clst
| Rewrite source_compose; clst
| Rewrite target_compose; clst]
|_-> Idtac.




End Umorphism.



Module Presheaf_notation. 

Export Notation.Basic.

Export Umorphism. 
Export Notation.Categorical. 
Export Notation.Algebraic.

Syntactic Definition Cat := (C_ (A_ (T_ (dot (0))))).
Syntactic Definition Restr := (R_ (E_ (S_ (T_ (R_ (dot (1))))))).

Definition cat := [x:E](extra x Cat).
Definition restr' := [x,a:E](extra x Restr a). 


(*** a presheaf is just a collection of Umorphisms (restr u),
however we want to have (U a) being the set of ordered pairs
(x,z) where x is an object and (inc z (U (val a x))) ***)


Definition restr := [a,u:E](mask (mor (cat a) u) (restr' a u)).

Definition val := [a,x:E](source (restr a (id (cat a) x))).

Lemma restr_prime : (a,u:E)(mor (cat a) u) -> 
(restr a u) == (restr' a u).
ir. 
uf restr. ap mask_in. am. 
Save. 

Lemma restr_eq : (a,b:E)(cat a) == (cat b) -> 
((u:E)(mor (cat a) u) -> (restr a u) == (restr b u)) ->
(restr a) == (restr b).
ir. 
ap arrow_extensionality; ir. 
Apply by_cases with (mor (cat a) a0). ir. 
ap H0; am. ir. uf restr. rw mask_out. 
rw mask_out; tv. wr H. am. am. 
Save.

Lemma val_eq : (a,b:E)(cat a) == (cat b) -> (restr a) == (restr b) ->
(val a) == (val b). 
ir. 
uf val. rw H. rw H0. tv. 
Save. 

Definition U_val_prod := [a,x:E](Image.create
(U (val a x)) [z:E](pair x z)).

Definition U_constr := [a:E](union (Image.create (objects (cat a))
(U_val_prod a))).

Lemma inc_U_constr : (a,z:E)(inc z (U_constr a)) ==
(A (is_pair z)
(A (ob (cat a) (pr1 z))
    (inc (pr2 z) (U (val a (pr1 z))))
)). 
ir.
ap iff_eq; ir.  ufi U_constr H. 
Remind '(union_exists H). nin H0. ee. 
Remind '(Image.ex H1). nin H2. 
ee. Copy H0. wri H3 X0. 
ufi U_val_prod X0. 
Remind '(Image.ex X0). nin H4. ee. wr H5. 
ap pair_is_pair. 
Remind '(Image.ex H1). nin H2. 
ee. Copy H0. wri H3 X0. 
ufi U_val_prod X0. 
Remind '(Image.ex X0). nin H4. ee. wr H5. 
rw pr1_pair. Exact H2. 
Remind '(Image.ex H1). nin H2. 
ee. Copy H0. wri H3 X0. 
ufi U_val_prod X0. 
Remind '(Image.ex X0). nin H4. ee. wr H5. 
rw pr2_pair. rw pr1_pair. am. ee. 
uf U_constr. 
Apply union_inc with (U_val_prod a (pr1 z)). 
uf U_val_prod. ap Image.show_inc. 
sh '(pr2 z). ee. am. ap  pair_recov. am. 
ap Image.show_inc. sh '(pr1 z). ee. am. 
tv. 
Save. 

 
Section def1.
Variables v_underlying, v_cat, v_scalars, v_index:E.
Variables v_restr :E1.


Definition create_obj1  :=[op :nota]
<[op :nota](arity_type (arity op))>Cases op of
(U_ (N_ (D_ (E_ (R_ (L_ (Y_ (I_ (N_ (G_ (dot (0)))))))))))) => v_underlying |
(C_ (A_ (T_ (dot (0))))) => v_cat |
(S_ (C_ (A_ (L_ (A_ (R_ (S_ (dot (0))))))))) => v_scalars |
(I_ (N_ (D_ (E_ (X_ (dot (0))))))) => v_index |
(R_ (E_ (S_ (T_ (R_ (dot (1))))))) => v_restr |
u => (da u)
end. 

Definition create_ens1 := 
(createN create_obj1).


Lemma morphisms_formula : (x:E)(morphisms x) == 
(V (J (R Morphisms) emptyset) x). 
ir. tv. 
Save.

Lemma related_morphisms : (o:obj; x:E)
(related o x) ->(related o (morphisms x)).
ir.
uhg. rw morphisms_formula. ap region_value. am.
Save.



Lemma mor_cat_related_obj : (a:E)(mor v_cat a) -> 
(related create_obj1 a).
ir. 
uh H. 
Remind '(region_preserves create_obj1 Cat). 
Assert (related create_obj1 v_cat). 
Exact H0. 
Assert (related create_obj1 (morphisms v_cat)). 
ap related_morphisms; am. 
uhg. ap '(region_preserves_sub H2). am. 
Save. 




Lemma U_rw1 : (U create_ens1) == v_underlying.
ir; uf U; uf create_ens1. notatac1; am. 
Save. 

Lemma cat_rw1 : (cat create_ens1) == v_cat.
ir; uf cat; uf create_ens1. notatac1; am. 
Save. 

Lemma scalars_rw1 : (scalars create_ens1) == v_scalars.
ir; uf scalars; uf create_ens1. notatac1; am. 
Save. 

Lemma index_rw1 : (index create_ens1) == v_index.
ir; uf index; uf create_ens1. notatac1; am. 
Save. 


Lemma restr_rw1: (a:E)(mor v_cat a) ->
(restr create_ens1 a) == (v_restr a).
ir. 
rw restr_prime. uf restr'. uf create_ens1. 
notatac1. ap mor_cat_related_obj; am. 
rw cat_rw1. am.   
Save. 


End def1. 

Section def. 
Variables v_cat, v_scalars, v_index:E.
Variables v_restr :E1.

Definition create_inter := (create_ens1 emptyset v_cat v_scalars v_index
v_restr). 

Definition create_ens := 
(create_ens1 (U_constr create_inter) v_cat v_scalars v_index
v_restr).

Lemma U_rw_constr : (U create_ens) == (U_constr create_inter).
uf create_ens. rw U_rw1. tv. 
Save.


Lemma cat_rw : (cat create_ens) == v_cat.
uf create_ens. rw cat_rw1. tv. 
Save.

Lemma scalars_rw : (scalars create_ens) == v_scalars.
uf create_ens. rw scalars_rw1. tv. 
Save. 

Lemma index_rw : (index create_ens) == v_index.
uf create_ens. rw index_rw1. tv. 
Save. 

Lemma restr_rw : (u:E)(mor (cat create_ens) u) -> 
(restr create_ens u) == (v_restr u).
ir. 
uf create_ens. rw restr_rw1. tv. rwi cat_rw H. am. 
Save. 

Lemma inc_U_rw : (x:E)(inc x (U create_ens)) ==
(A (is_pair x)
(A (ob (cat create_ens) (pr1 x))
   (inc (pr2 x) (U (val create_ens (pr1 x))))
)). 
ir. 
rw U_rw_constr. 
rw inc_U_constr. Assert (cat create_ens) ==
(cat create_inter). rw cat_rw. 
uf create_inter. rw cat_rw1. tv. rw H. 
Assert (val create_inter (pr1 x)) ==
(val create_ens (pr1 x)). 
uf val. 
Assert (restr create_inter) == (restr create_ens).
ap restr_eq. sy; am. ir. 
rw restr_rw. uf create_inter; rw restr_rw1. 
tv. ufi create_inter H0. 
rwi cat_rw1 H0. am. rw H; am. rw H0. rw H. 
tv. rw H0. 
tv. 
Save. 


End def. 


Definition like := [a:E](create_ens (cat a) 
(scalars a) (index a) (restr a)) == a.

Definition same := [a,b:E]
(A (cat a) == (cat b)
(A (scalars a) == (scalars b)
(A (index a) == (index b)
(A (restr a) == (restr b)
   (val a) == (val b)
)))).

Lemma show_same : (a,b:E)(cat a) == (cat b) 
-> (scalars a) == (scalars b) ->(index a) == (index b) ->
((u:E)(mor (cat a) u) -> 
(restr a u) == (restr b u)) ->
(same a b).
ir. 
uhg; dj. 
am. am. am. 
ap restr_eq. am. am. 
uf val. rw H6. rw H. tv. 
Save. 




Lemma like_same_eq : (a,b:E)(like a) -> (like b) -> (same a b) -> a == b.
ir. uh H. uh H0. wr H. wr H0. uh H1; ee. rw H1. 
rw H2. rw H4. rw H3.   tv. 
Save.

Lemma create_same : (a:E)(same a (create_ens (cat a) 
(scalars a) (index a) (restr a))). 
ir. 
ap show_same; ir.   rw cat_rw; tv. 
rw scalars_rw; tv. rw index_rw; tv. 
rw restr_rw. tv. rw cat_rw. am.   
Save. 


Lemma create_like : (a:E)(like (create_ens (cat a) 
(scalars a) (index a) (restr a))). 
ir.
LetTac K:= (create_ens (cat a) 
(scalars a) (index a) (restr a)). 
uhg.  Assert (same a K). uf K; ap create_same. 
uh H; ee. wr H; wr H0; wr H2; wr H1. tv. 
Save. 

End Presheaf_notation. 


Module Topological.

Export Notation.Basic. 

Syntactic Definition Opens := (O_ (P_ (E_ (N_ (S_ (dot (0))))))).
Syntactic Definition Distance := (D_ (I_ (S_ (T_ (A_ (N_ (C_ (E_ (dot (2)))))))))).
Syntactic Definition Structure := (S_ (T_ (R_ (U_ (C_ (T_ (U_ (R_ (E_ (dot (0))))))))))).

Definition opens := [x:E](extra x Opens). 
Definition distance' := [x,a,b:E](extra x Distance a b).
Definition structure := [x:E](extra x Structure). 


(*** topological and possibly metric spaces, maybe with
other structure put into the Structure variable ***)


Definition distance := [a,x,y:E](mask (A (inc x (U a)) (inc y (U a)))
(distance' a x y)).

Definition is_open := [a,u:E]
(A (sub u (U a))
   (inc u (opens a))
). 

Lemma distance_prime : (a,x,y:E)(inc x (U a)) -> ( inc y (U a))->
(distance a x y) == (distance' a x y).
ir. 
uf distance; ap mask_in. ee; am. 
Save. 

Lemma distance_eq : (a,b:E)(U a) == (U b) ->
((x,y:E)(inc x (U a)) -> (inc y (U a)) -> (distance a x y) ==
(distance b x y)) -> (distance a) == (distance b).
ir. 
ap arrow_extensionality; Intro x. 
ap arrow_extensionality; Intro y.
Apply by_cases with (A (inc x (U a)) (inc y (U a))); ir. 
ee; ap H0; am. uf distance. 
rw mask_out. rw mask_out; tv. 
wr H. am. am. 
Save. 

Section def. 
Variables x, v_opens, v_structure : E.
Variable v_distance : E2.



Definition create_obj  :=[op :nota]
<[op :nota](arity_type (arity op))>Cases op of
(U_ (N_ (D_ (E_ (R_ (L_ (Y_ (I_ (N_ (G_ (dot (0)))))))))))) => x |
(O_ (P_ (E_ (N_ (S_ (dot (0))))))) => v_opens |
(S_ (T_ (R_ (U_ (C_ (T_ (U_ (R_ (E_ (dot (0))))))))))) => v_structure |
(D_ (I_ (S_ (T_ (A_ (N_ (C_ (E_ (dot (2)))))))))) => v_distance |
u => (da u)
end. 

Definition create_ens := 
(createN create_obj).

Lemma related_obj : (a:E)(inc a x) -> (related create_obj a).
ir. sub_relate 'Underlying. am. 
Save. 



Lemma U_rw : (U create_ens) == x.
ir; uf U; uf create_ens. notatac1; am. 
Save. 

Lemma opens_rw : (opens create_ens) == v_opens.
ir; uf opens; uf create_ens. notatac1; am. 
Save. 

Lemma structure_rw : (structure create_ens) == v_structure.
ir; uf structure; uf create_ens. notatac1; am. 
Save. 

Lemma distance_rw : (a,b:E)(inc a x)->(inc b x) ->
(distance create_ens a b) == (v_distance a b).
ir.
rw distance_prime. uf distance'; 
uf create_ens. notatac1; ap related_obj; am.
rw U_rw. am. rw U_rw. am.

Save.



End def. 

Definition like := [a:E](create_ens (U a) 
(opens a) (structure a) (distance a)) == a.

Definition same := [a,b:E]
(A (U a) == (U b)
(A (opens a) == (opens b)
(A (is_open a) == (is_open b)
(A (structure a) == (structure b)
   (distance a) == (distance b)
)))).

Lemma show_same : (a,b:E)(U a) == (U b) -> (opens a) == (opens b) 
-> (structure a) == (structure b) ->
((x,y:E)(inc x (U a)) -> (inc y (U a)) -> 
(distance a x y) == (distance b x y)) ->
(same a b).
ir. 
uhg; dj. am. am. 
ap arrow_extensionality; ir. 
ap iff_eq; ir. uhg; uh H5; ee. wr H3; am. 
wr H4; am. uhg; uh H5; ee. rw H3; am. 
rw H4; am. am. 
ap distance_eq; am. 
Save. 




Lemma like_same_eq : (a,b:E)(like a) -> (like b) -> (same a b) -> a == b.
ir. uh H. uh H0. wr H. wr H0. uh H1; ee. rw H1. 
rw H2. rw H4. rw H5.  tv. 
Save.

Lemma create_same : (a:E)(same a (create_ens (U a) 
(opens a) (structure a) 
(distance a))).
ir. 
ap show_same; ir.  rw U_rw. tv. rw opens_rw; tv. 
rw structure_rw; tv. 
rw distance_rw. tv. am. am.  
Save. 


Lemma create_like : (a:E)(like (create_ens (U a) (opens a) 
(structure a) 
(distance a))).
ir.
LetTac K:= (create_ens (U a) (opens a) 
(structure a) 
(distance a)). 
uhg.  Assert (same a K). uf K; ap create_same. 
uh H; ee. wr H; wr H0; wr H2; wr H3. tv. 
Save. 



End Topological.