more work for igft

diff --git a/helm/software/matita/nlibrary/logic/connectives.ma b/helm/software/matita/nlibrary/logic/connectives.ma
index 026e9216951c9224737b6493953317effd635369..a149bc9ddf4e88133871e0d73aed62fe02fb613b 100644 (file)
--- a/helm/software/matita/nlibrary/logic/connectives.ma
+++ b/helm/software/matita/nlibrary/logic/connectives.ma
@@ -38,6 +38,11 @@ interpretation "logical or" 'or x y = (Or x y).
 ninductive Ex (A:Type) (P:A → CProp) : CProp ≝
     ex_intro: ∀x:A. P x → Ex A P.
 
+
+ninductive Ex1 (A:Type[1]) (P:A → CProp) : CProp[1] ≝
+    ex_intro1: ∀x:A. P x → Ex1 A P.
+
+interpretation "exists1" 'exists x = (Ex1 ? x).
 interpretation "exists" 'exists x = (Ex ? x).
 
 nrecord iff (A,B: CProp) : CProp ≝

diff --git a/helm/software/matita/nlibrary/topology/igft.ma b/helm/software/matita/nlibrary/topology/igft.ma
index c009f2464f07665c1515ac0577aeca30ae148835..3e9e359d5f01109f9743e7e0f0f7d27f1c303ee3 100644 (file)
--- a/helm/software/matita/nlibrary/topology/igft.ma
+++ b/helm/software/matita/nlibrary/topology/igft.ma
@@ -1,13 +1,13 @@
 include "sets/sets.ma".
 
-nrecord axiom_set : Type[1] ≝ { 
-  S:> Type[0];
+nrecord Ax : Type[1] ≝ { 
+  S:> setoid; (* Type[0]; *)
   I: S → Type[0];
   C: ∀a:S. I a → Ω ^ S
 }.
 
-notation "𝐈  \sub( ❨term 90 a❩ )" non associative with precedence 70 for @{ 'I $a }.
-notation "𝐂 \sub ( ❨term 90 a,\emsp term 90 i❩ )" non associative with precedence 70 for @{ 'C $a $i }.
+notation "𝐈  \sub( ❨a❩ )" non associative with precedence 70 for @{ 'I $a }.
+notation "𝐂 \sub ( ❨a,\emsp i❩ )" non associative with precedence 70 for @{ 'C $a $i }.
 
 notation > "𝐈 term 90 a" non associative with precedence 70 for @{ 'I $a }.
 notation > "𝐂 term 90 a term 90 i" non associative with precedence 70 for @{ 'C $a $i }.
@@ -15,7 +15,7 @@ notation > "𝐂 term 90 a term 90 i" non associative with precedence 70 for @{
 interpretation "I" 'I a = (I ? a).
 interpretation "C" 'C a i = (C ? a i).
 
-ndefinition cover_set ≝ λc:∀A:axiom_set.Ω^A → A → CProp[0].λA,C,U.
+ndefinition cover_set ≝ λc:∀A:Ax.Ω^A → A → CProp[0].λA,C,U.
   ∀y.y ∈ C → c A U y.
 
 (* a \ltri b *)
@@ -24,7 +24,7 @@ for @{ 'covers $a $b }.
 
 interpretation "covers set temp" 'covers C U = (cover_set ?? C U).
 
-ninductive cover (A : axiom_set) (U : Ω^A) : A → CProp[0] ≝ 
+ninductive cover (A : Ax) (U : Ω^A) : A → CProp[0] ≝ 
 | creflexivity : ∀a:A. a ∈ U → cover ? U a
 | cinfinity    : ∀a:A.∀i:𝐈 a. 𝐂 a i ◃ U → cover ? U a.
 napply cover;
@@ -33,7 +33,7 @@ nqed.
 interpretation "covers" 'covers a U = (cover ? U a).
 interpretation "covers set" 'covers a U = (cover_set cover ? a U).
 
-ndefinition fish_set ≝ λf:∀A:axiom_set.Ω^A → A → CProp[0].
+ndefinition fish_set ≝ λf:∀A:Ax.Ω^A → A → CProp[0].
  λA,U,V.
   ∃a.a ∈ V ∧ f A U a.
 
@@ -43,7 +43,7 @@ for @{ 'fish $a $b }.
 
 interpretation "fish set temp" 'fish A U = (fish_set ?? U A).
 
-ncoinductive fish (A : axiom_set) (F : Ω^A) : A → CProp[0] ≝ 
+ncoinductive fish (A : Ax) (F : Ω^A) : A → CProp[0] ≝ 
 | cfish : ∀a. a ∈ F → (∀i:𝐈 a .𝐂  a i ⋉ F) → fish A F a.
 napply fish;
 nqed.
@@ -51,7 +51,7 @@ nqed.
 interpretation "fish set" 'fish A U = (fish_set fish ? U A).
 interpretation "fish" 'fish a U = (fish ? U a).
 
-nlet corec fish_rec (A:axiom_set) (U: Ω^A)
+nlet corec fish_rec (A:Ax) (U: Ω^A)
  (P: Ω^A) (H1: P ⊆ U)
   (H2: ∀a:A. a ∈ P → ∀j: 𝐈 a. 𝐂 a j ≬ P):
    ∀a:A. ∀p: a ∈ P. a ⋉ U ≝ ?.
@@ -65,11 +65,11 @@ nqed.
 notation "◃U" non associative with precedence 55
 for @{ 'coverage $U }.
 
-ndefinition coverage : ∀A:axiom_set.∀U:Ω^A.Ω^A ≝ λA,U.{ a | a ◃ U }.
+ndefinition coverage : ∀A:Ax.∀U:Ω^A.Ω^A ≝ λA,U.{ a | a ◃ U }.
 
 interpretation "coverage cover" 'coverage U = (coverage ? U).
 
-ndefinition cover_equation : ∀A:axiom_set.∀U,X:Ω^A.CProp[0] ≝  λA,U,X. 
+ndefinition cover_equation : ∀A:Ax.∀U,X:Ω^A.CProp[0] ≝  λA,U,X. 
   ∀a.a ∈ X ↔ (a ∈ U ∨ ∃i:𝐈 a.∀y.y ∈ 𝐂 a i → y ∈ X).  
 
 ntheorem coverage_cover_equation : ∀A,U. cover_equation A U (◃U).
@@ -95,11 +95,11 @@ nqed.
 notation "⋉F" non associative with precedence 55
 for @{ 'fished $F }.
 
-ndefinition fished : ∀A:axiom_set.∀F:Ω^A.Ω^A ≝ λA,F.{ a | a ⋉ F }.
+ndefinition fished : ∀A:Ax.∀F:Ω^A.Ω^A ≝ λA,F.{ a | a ⋉ F }.
 
 interpretation "fished fish" 'fished F = (fished ? F).
 
-ndefinition fish_equation : ∀A:axiom_set.∀F,X:Ω^A.CProp[0] ≝ λA,F,X.
+ndefinition fish_equation : ∀A:Ax.∀F,X:Ω^A.CProp[0] ≝ λA,F,X.
   ∀a. a ∈ X ↔ a ∈ F ∧ ∀i:𝐈 a.∃y.y ∈ 𝐂 a i ∧ y ∈ X. 
   
 ntheorem fised_fish_equation : ∀A,F. fish_equation A F (⋉F).
@@ -115,3 +115,54 @@ ntheorem fised_max_fish_equation : ∀A,F,G. fish_equation A F G → G ⊆ ⋉F.
 #b; ncases (H b); #H1; #_; #bG; ncases (H1 bG); #E1; #E2; nassumption; 
 nqed. 
 
+nrecord nAx : Type[2] ≝ { 
+  nS:> setoid; (*Type[0];*)
+  nI: nS → Type[0];
+  nD: ∀a:nS. nI a → Type[0];
+  nd: ∀a:nS. ∀i:nI a. nD a i → nS
+}.
+
+notation "𝐃 \sub ( ❨a,\emsp i❩ )" non associative with precedence 70 for @{ 'D $a $i }.
+notation "𝐝 \sub ( ❨a,\emsp i,\emsp j❩ )" non associative with precedence 70 for @{ 'd $a $i $j}.
+
+notation > "𝐃 term 90 a term 90 i" non associative with precedence 70 for @{ 'D $a $i }.
+notation > "𝐝 term 90 a term 90 i term 90 j" non associative with precedence 70 for @{ 'd $a $i $j}.
+
+interpretation "D" 'D a i = (nD ? a i).
+interpretation "d" 'd a i j = (nd ? a i j).
+
+ndefinition image ≝ λA:nAx.λa:A.λi. { x | ∃j:𝐃 a i. x = 𝐝 a i j }.
+
+notation > "𝐈𝐦  [𝐝 term 90 a term 90 i]" non associative with precedence 70 for @{ 'Im $a $i }.
+notation "𝐈𝐦  [𝐝 \sub ( ❨a,\emsp i❩ )]" non associative with precedence 70 for @{ 'Im $a $i }.
+
+interpretation "image" 'Im a i = (image ? a i).
+
+ndefinition Ax_of_nAx : nAx → Ax.
+#A; @ A (nI ?); #a; #i; napply (𝐈𝐦 [𝐝 a i]);
+nqed.
+
+ninductive sigma (A : Type[0]) (P : A → CProp[0]) : Type[0] ≝ 
+ sig_intro : ∀x:A.P x → sigma A P. 
+
+interpretation "sigma" 'sigma \eta.p = (sigma ? p). 
+
+ndefinition nAx_of_Ax : Ax → nAx.
+#A; @ A (I ?);
+##[ #a; #i; napply (Σx:A.x ∈ 𝐂 a i);
+##| #a; #i; *; #x; #_; napply x;
+##]
+nqed.
+
+ninductive ord (A : nAx) : Type[0] ≝ 
+ | oO : ord A
+ | oS : ord A → ord A
+ | oL : ∀a:A.∀i.∀f:𝐃 a i → ord A. ord A.
+
+nlet rec famU (A : nAx) (U : Ω^A) (x : ord A) on x : Ω^A ≝ 
+  match x with
+  [ oO ⇒ U
+  | oS y ⇒ let Un ≝ famU A U y in Un ∪ { x | ∃i.∀j:𝐃 x i.𝐝 x i j ∈ Un} 
+  | oL a i f ⇒ { x | ∃j.x ∈ famU A U (f j) } ].
+  
+ndefinition ord_coverage ≝ λA,U.{ y | ∃x:ord A. y ∈ famU ? U x }.