include "topology/igft.ma".
+ntheorem axiom_cond: âA:Ax.âa:A.âi:đ a.a â đ a i.
+#A; #a; #i; @2 i; #x; #H; @; napply H;
+nqed.
+
+nlemma hint_auto1 : âA,U,V. (âx.x â U â x â V) â cover_set cover A U V.
+nnormalize; nauto.
+nqed.
+
+alias symbol "covers" (instance 1) = "covers".
+alias symbol "covers" (instance 2) = "covers set".
+alias symbol "covers" (instance 3) = "covers".
+ntheorem transitivity: âA:Ax.âa:A.âU,V. a â U â U â V â a â V.
+#A; #a; #U; #V; #aU; #UV;
+nelim aU;
+##[ #c; #H; nauto;
+##| #c; #i; #HCU; #H; @2 i; nauto;
+##]
+nqed.
+
+ndefinition emptyset: âA.Ί^A â ÎťA.{x | False}.
+
+notation "â
" non associative with precedence 90 for @{ 'empty }.
+interpretation "empty" 'empty = (emptyset ?).
+
+naxiom EM : âA:Ax.âa:A.âi_star.(a â đ a i_star) ⨠( a â đ a i_star).
+
+ntheorem th2_3 :
+ âA:Ax.âa:A. a â â
â âi. ÂŹ a â đ a i.
+#A; #a; #H; nelim H;
+##[ #n; *;
+##| #b; #i_star; #IH1; #IH2;
+ ncases (EM ⌠b i_star);
+ ##[##2: (* nauto; *) #W; @i_star; napply W;
+ ##| nauto;
+ ##]
+##]
+nqed.
+
+ninductive eq1 (A : Type[0]) : Type[0] â CProp[0] â
+| refl1 : eq1 A A.
+
+notation "hvbox( a break âź b)" non associative with precedence 40
+for @{ 'eqT $a $b }.
+
+interpretation "eq between types" 'eqT a b = (eq1 a b).
+
ninductive unit : Type[0] â one : unit.
-naxiom E: setoid.
-naxiom R: E â Ί^E.
+nrecord uAx : Type[1] â {
+ uax_ : Ax;
+ with_ : âa:uax_.đ a âź unit
+}.
-ndefinition axs: Ax.
-@ E (Îť_.unit) (Îťa,x.R a);
+ndefinition uax : uAx â Ax.
+#A; @ (uax_ A) (Îťx.unit); #a; #_; napply (đ a ?); nlapply one; ncases (with_ A a); nauto;
nqed.
+ncoercion uax : âu:uAx. Ax â uax on _u : uAx to Ax.
+
+naxiom A: Type[0].
+naxiom S: A â Ί^A.
+
+ndefinition axs: uAx.
+@; ##[ @ A (Îť_.unit) (Îťa,x.S a); ##| #_; @; ##]
+nqed.
+
+alias id "S" = "cic:/matita/ng/topology/igft/S.fix(0,0,1)".
unification hint 0 â ;
x â axs
(* -------------- *) â˘
- S x ⥠E.
-
-ndefinition emptyset: Ί^axs â {x | False}.
+ S x ⥠A.
-ndefinition Z: Ί^axs â {x | x â emptyset}.
-alias symbol "covers" = "covers".
-alias symbol "covers" = "covers set".
-alias symbol "covers" = "covers".
-alias symbol "covers" = "covers set".
-ntheorem cover_trans: âA:Ax.âa:A.âU,V. a â U â U â V â a â V.
-#A; #a; #U; #V; #aU; #UV;
-nelim aU;
-##[ #c; #H; napply (UV ⌠H);
-##| #c; #i; #HCU; #H; napply (cinfinity ⌠i); napply H;
-##]
+ntheorem col2_4 :
+ âA:uAx.âa:A. a â â
â ÂŹ a â đ a ?. ##[ (* bug *) ##2: nnormalize; napply one; ##]
+#A; #a; #H; nelim H;
+##[ #n; *;
+##| #b; #i_star; #IH1; #IH2; #H3; nlapply (IH2 ⌠H3); #H4; nauto;
+##]
+nqed.
+
+ndefinition Z : Ί^axs â { x | x â â
}.
+
+ntheorem cover_monotone: âA:Ax.âa:A.âU,V.U â V â a â U â a â V.
+#A; #a; #U; #V; #HUV; #H; nelim H;
+##[ nauto;
+##| #b; #i; #HCU; #W; @2 i; #x; nauto; ##]
+nqed.
+
+ntheorem th3_1: ÂŹâa:axs.Z â S a ⧠S a â Z.
+*; #a; *; #ZSa; #SaZ;
+ncut (a â Z); ##[
+ nlapply (axiom_cond ⌠a one); #AxCon; nchange in AxCon with (a â S a);
+ (* nauto; *) napply (cover_monotone ⌠AxCon); nassumption; ##] #H;
+ncut (a â â
); ##[ napply (transitivity ⌠H); #x; #E; napply E; ##] #H1;
+ncut (ÂŹ a â S a); ##[ napply (col2_4 ⌠H1); ##] #H2;
+ncut (a â S a); ##[ napply ZSa; napply H1; ##] #H3;
+nauto;
nqed.
+include "nat/nat.ma".
+
+naxiom phi : nat â nat â nat.
+
+notation > "Ď" non associative with precedence 90 for @{ 'phi }.
+interpretation "phi" 'phi = phi.
+
+notation < "Ď a i" non associative with precedence 90 for @{ 'phi2 $a $i}.
+interpretation "phi2" 'phi2 a i = (phi a i).
+notation < "Ď a" non associative with precedence 90 for @{ 'phi1 $a }.
+interpretation "phi2" 'phi1 a = (phi a).
+
+ndefinition caxs : uAx.
+@; ##[ @ nat (Îť_.unit); #a; #_; napply { x | Ď a x = O } ##| #_; @; ##]
+nqed.
+
+
+alias id "S" = "cic:/matita/ng/topology/igft/S.fix(0,0,1)".
+unification hint 0 â ;
+ x â caxs
+ (* -------------- *) â˘
+ S x ⥠nat.
+
+naxiom h : nat â nat.
+
+naxiom Ph : âx.h x = O â x â â
.
+
+ninductive eq2 (A : Type[1]) (a : A) : A â CProp[0] â
+| refl2 : eq2 A a a.
+
+interpretation "eq2" 'eq T a b = (eq2 T a b).
+
+ntheorem th_ch3: ÂŹâa:caxs.âx.Ď a x = h x.
+*; #a; #H;
+ncut ((đ a one) â { x | x â â
}); (* bug *)
+nchange in xx with { x | h x
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
ntheorem cantor: âa:axs. ÂŹ (Z â R a ⧠R a â Z).
#a; *; #ZRa; #RaZ;
-ncut (a â R a); ##[ @2; ##[ napply one; ##] #x; #H; @; napply H; ##] #H1;
-ncut (a â emptyset); ##[
+ncut (a â R a); ##[ @2; ##[ napply one; ##] #x; #H; @; napply H; ##] #H1;
+ncut (a â â
); ##[
napply (cover_trans ⌠H1);
#x; #H; nlapply (RaZ ⌠H); #ABS; napply ABS; ##] #H2;
ncut (a â R a); ##[ napply ZRa; napply H2; ##] #H3;
nelim H2 in H3;
-##[ nauto.
-##| nnormalize; nauto. ##] (* se lo lancio su entrambi fallisce di width *)
+##[ nauto.
+##| nnormalize; nauto. ##] (* se lo lancio su entrambi fallisce di width *)
+nqed.
+
+ninductive deduct (A : nAx) (U : Ί^A) : A â CProp[0] â
+| drefl : âa.a â U â deduct A U a
+| dcut : âa.âi:đ a. (ây:đ a i.deduct A U (đ a i y)) â deduct A U a.
+
+notation " a ⢠b " non associative with precedence 45 for @{ 'deduct $a $b }.
+interpretation "deduct" 'deduct a b = (deduct ? b a).
+
+ntheorem th2_3_1 : âA:nAx.âa:A.âi:đ a. a ⢠đđŚ[đ a i].
+#A; #a; #i;
+ncut (ây:đ a i.đ a i y ⢠đđŚ[đ a i]); ##[ #y; @; @y; @; ##] #H1;
+napply (dcut ⌠i); nassumption;
+nqed.
+
+ntheorem th2_3_2 :
+ âA:nAx.âa:A.âi:đ a.âU,V. a ⢠U â (âu.u â U â u ⢠V) â a ⢠V.
+#A; #a; #i; #U; #V; #aU; #xUxV;
+nelim aU;
+##[ nassumption;
+##| #b; #i; #dU; #dV; @2 i; nassumption;
+##]
nqed.
+ntheorem th2_3 :
+ âA:nAx.
+ (âa:A.âi_star.(ây:đ a i_star.đ a i_star y = a) ⨠(ây:đ a i_star.đ a i_star y = a)) â
+ âa:A. a â â
â âi:đ a. ÂŹ a \in Z
+#A; #EM; #a; #H; nelim H;
+##[ #n; *;
+##| #b; #i_star; #IH1; #IH2;
+ ncases (EM b i_star);
+ ##[##2: #W; @i_star; napply W;
+ ##| *; #y_star; #E; nlapply (IH2 y_star); nrewrite > E; #OK; napply OK;
+ ##]
+##]
+nqed.
+
+ninductive eq1 (A : Type[0]) : Type[0] â CProp[0] â
+| refl1 : eq1 A A.
+
+notation "hvbox( a break âź b)" non associative with precedence 40
+for @{ 'eqT $a $b }.
+
+interpretation "eq between types" 'eqT a b = (eq1 a b).
+
+nrecord uAx : Type[1] â {
+ uax_ : Ax;
+ with_ : âa:uax_.đ a âź unit
+}.
+
+ndefinition uax : uAx â Ax.
+*; #A; #E; @ A (Îťx.unit); #a; ncases (E a);
+##[ #i; napply (đ a i);
+##| #i; nnormalize; #j; napply (đ a i j);
+##]
+nqed.
+
+ncoercion uax : âu:unAx. nAx â uax on _u : unAx to nAx.
+
+
+nlemma cor_2_5 : âA:unAx.âa:A.âi.a ⢠â
â ÂŹ(a â đđŚ[đ a i]).
+#A; #a; #i; #H; nelim H in i;
+##[ #w; *;
+##| #a; #i; #IH1; #IH2;
+
+
+
+
\ No newline at end of file