From 3e4dee5271019834cfe061d43789380cb3871b7c Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sun, 4 Jan 2009 20:33:56 +0000
Subject: [PATCH] 1. CProp_n fixed to be equal to Type_n to better understand
 what is happening    with universe levels 2. major proof step: I have proved
 (up to universe inconsistency :-( that    every RELation induces an OA
 morphism. In particular, these means:      A) having correctly defined the
 four images on subsets      B) having proved the fundamental symmetry      C)
 having proved the two fundamental adjunctions

---
 .../formal_topology/overlap/categories.ma     |  22 ++--
 .../formal_topology/overlap/relations.ma      | 104 ++++++++++++++----
 .../formal_topology/overlap/subsets.ma        |  12 +-
 3 files changed, 100 insertions(+), 38 deletions(-)

diff --git a/helm/software/matita/contribs/formal_topology/overlap/categories.ma b/helm/software/matita/contribs/formal_topology/overlap/categories.ma
index 86bc2529c..67db8176c 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/categories.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/categories.ma
@@ -31,15 +31,17 @@ coercion Type_OF_Type1.
 coercion Type_OF_Type2.
 coercion Type_OF_Type3.
 
-definition CProp0 := CProp.
-definition CProp1 := CProp.
-definition CProp2 := CProp.
+definition CProp0 := Type0.
+definition CProp1 := Type1.
+definition CProp2 := Type2.
+(*
 definition CProp0_lt_CProp1 := (CProp0 : CProp1).
 definition CProp1_lt_CProp2 := (CProp1 : CProp2).
 
 definition CProp_OF_CProp0: CProp0 → CProp := λx.x.
 definition CProp_OF_CProp1: CProp1 → CProp := λx.x.
 definition CProp_OF_CProp2: CProp2 → CProp := λx.x.
+*)
 
 record equivalence_relation (A:Type0) : Type1 ≝
  { eq_rel:2> A → A → CProp0;
@@ -194,7 +196,7 @@ definition CPROP: setoid1.
      | intros 1; split; intro; assumption
      | intros 3; cases H; split; assumption
      | intros 5; cases H; cases H1; split; intro;
-        [ apply (H4 (H2 x1)) | apply (H3 (H5 z1))]]]
+        [ apply (f2 (f x1)) | apply (f1 (f3 z1))]]]
 qed.
 
 alias symbol "eq" = "setoid1 eq".
@@ -233,8 +235,8 @@ definition if_morphism: binary_morphism1 CPROP CPROP CPROP.
  constructor 1;
   [ apply (λA,B. A → B)
   | intros; split; intros;
-     [ apply (if ?? e1); apply H; apply (fi ?? e); assumption
-     | apply (fi ?? e1); apply H; apply (if ?? e); assumption]]
+     [ apply (if ?? e1); apply f; apply (fi ?? e); assumption
+     | apply (fi ?? e1); apply f; apply (if ?? e); assumption]]
 qed.
 
 (*
@@ -303,8 +305,8 @@ definition unary_morphism_setoid: setoid → setoid → setoid1.
   | constructor 1;
      [ intros (f g); apply (∀a:s. eq ? (f a) (g a));
      | intros 1; simplify; intros; apply refl;
-     | simplify; intros; apply sym; apply H;
-     | simplify; intros; apply trans; [2: apply H; | skip | apply H1]]]
+     | simplify; intros; apply sym; apply f;
+     | simplify; intros; apply trans; [2: apply f; | skip | apply f1]]]
 qed.
 
 definition SET: category1.
@@ -354,8 +356,8 @@ definition unary_morphism1_setoid1: setoid1 → setoid1 → setoid2.
        alias symbol "eq" = "setoid1 eq".
        apply (∀a: carr1 s. f a = g a);
      | intros 1; simplify; intros; apply refl1;
-     | simplify; intros; apply sym1; apply H;
-     | simplify; intros; apply trans1; [2: apply H; | skip | apply H1]]]
+     | simplify; intros; apply sym1; apply f;
+     | simplify; intros; apply trans1; [2: apply f; | skip | apply f1]]]
 qed.
 
 definition SET1: category2.
diff --git a/helm/software/matita/contribs/formal_topology/overlap/relations.ma b/helm/software/matita/contribs/formal_topology/overlap/relations.ma
index c99239beb..f5141a2ed 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/relations.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/relations.ma
@@ -174,34 +174,69 @@ lemma extS_com: ∀o1,o2,o3,c1,c2,S. extS o1 o3 (c2 ∘ c1) S = extS o1 o2 c1 (e
     assumption]
 qed.
 *)
-axiom daemon: False.
+(* senza questo exT "fresco", universe inconsistency *)
+inductive exT (A:Type0) (P:A→CProp0) : CProp0 ≝
+  ex_introT: ∀w:A. P w → exT A P.
+
+lemma hint: ∀U. carr U → Type_OF_setoid1 ?(*(setoid1_of_SET U)*).
+ [ apply setoid1_of_SET; apply U
+ | intros; apply c;]
+qed.
+coercion hint.
+
 (* the same as ⋄ for a basic pair *)
-definition image: ∀U,V:REL. binary_morphism1 (arrows1 ? U V) (Ω \sup U) ?(*(Ω \sup V)*).
-cases daemon; qed.
+definition image: ∀U,V:REL. binary_morphism1 (arrows1 ? U V) (Ω \sup U) (Ω \sup V).
  intros; constructor 1;
-  [ apply (λr: arrows1 ? U V.λS: Ω \sup U. {y | ∃x:U. x ♮r y ∧ x ∈ S});
-    intros; simplify; split; intro; cases H; exists [1,3: apply w]
+  [ apply (λr: arrows1 ? U V.λS: Ω \sup U. {y | (*∃x:U. x ♮r y ∧ x ∈ S*)
+      exT ? (λx:carr U.x ♮r y ∧ x ∈ S) });
+    intros; simplify; split; intro; cases e1; exists [1,3: apply w]
      [ apply (. (#‡e)‡#); assumption
      | apply (. (#‡e ^ -1)‡#); assumption]
-  | intros; split; simplify; intros; cases H; exists [1,3: apply w]
+  | intros; split; simplify; intros; cases e2; exists [1,3: apply w]
      [ apply (. #‡(#‡e1)); cases x; split; try assumption;
        apply (if ?? (e ??)); assumption
      | apply (. #‡(#‡e1 ^ -1)); cases x; split; try assumption;
        apply (if ?? (e ^ -1 ??)); assumption]]
 qed.
 
-(*
 (* the same as □ for a basic pair *)
 definition minus_star_image: ∀U,V:REL. binary_morphism1 (arrows1 ? U V) (Ω \sup U) (Ω \sup V).
  intros; constructor 1;
-  [ apply (λr: arrows1 ? U V.λS: Ω \sup U. {y | ∀x:U. x ♮r y → x ∈ S});
-    intros; simplify; split; intros; apply H1;
-     [ apply (. #‡H \sup -1); assumption
-     | apply (. #‡H); assumption]
-  | intros; split; simplify; intros; [ apply (. #‡H1); | apply (. #‡H1 \sup -1)]
-    apply H2; [ apply (if ?? (H \sup -1 ??)); | apply (if ?? (H ??)) ] assumption]
+  [ apply (λr: arrows1 ? U V.λS: Ω \sup U. {y | ∀x:carr U. x ♮r y → x ∈ S});
+    intros; simplify; split; intros; apply f;
+     [ apply (. #‡e ^ -1); assumption
+     | apply (. #‡e); assumption]
+  | intros; split; simplify; intros; [ apply (. #‡e1); | apply (. #‡e1 ^ -1)]
+    apply f; [ apply (if ?? (e ^ -1 ??)); | apply (if ?? (e ??)) ] assumption]
+qed.
+
+(* the same as * for a basic pair *)
+definition star_image: ∀U,V:REL. binary_morphism1 (arrows1 ? U V) (Ω \sup V) (Ω \sup U).
+ intros; constructor 1;
+  [ apply (λr: arrows1 ? U V.λS: Ω \sup V. {x | ∀y:carr V. x ♮r y → y ∈ S});
+    intros; simplify; split; intros; apply f;
+     [ apply (. e ^ -1‡#); assumption
+     | apply (. e‡#); assumption]
+  | intros; split; simplify; intros; [ apply (. #‡e1); | apply (. #‡e1 ^ -1)]
+    apply f; [ apply (if ?? (e ^ -1 ??)); | apply (if ?? (e ??)) ] assumption]
+qed.
+
+(* the same as - for a basic pair *)
+definition minus_image: ∀U,V:REL. binary_morphism1 (arrows1 ? U V) (Ω \sup V) (Ω \sup U).
+ intros; constructor 1;
+  [ apply (λr: arrows1 ? U V.λS: Ω \sup V. {x | (*∃x:U. x ♮r y ∧ x ∈ S*)
+      exT ? (λy:carr V.x ♮r y ∧ y ∈ S) });
+    intros; simplify; split; intro; cases e1; exists [1,3: apply w]
+     [ apply (. (e‡#)‡#); assumption
+     | apply (. (e ^ -1‡#)‡#); assumption]
+  | intros; split; simplify; intros; cases e2; exists [1,3: apply w]
+     [ apply (. #‡(#‡e1)); cases x; split; try assumption;
+       apply (if ?? (e ??)); assumption
+     | apply (. #‡(#‡e1 ^ -1)); cases x; split; try assumption;
+       apply (if ?? (e ^ -1 ??)); assumption]]
 qed.
 
+(*
 (* minus_image is the same as ext *)
 
 theorem image_id: ∀o,U. image o o (id1 REL o) U = U.
@@ -263,12 +298,37 @@ include "o-algebra.ma".
 definition orelation_of_relation: ∀o1,o2:REL. arrows1 ? o1 o2 → ORelation (SUBSETS o1) (SUBSETS o2).
  intros;
  constructor 1;
-  [ 
-  |
-  |
-  |
-  |
-  |
-  |
-  ]
-qed.
\ No newline at end of file
+  [ constructor 1;
+     [ apply (λU.image ?? t U);
+     | intros; apply (#‡e); ]
+  | constructor 1;
+     [ apply (λU.minus_star_image ?? t U);
+     | intros; apply (#‡e); ]
+  | constructor 1;
+     [ apply (λU.star_image ?? t U);
+     | intros; apply (#‡e); ]
+  | constructor 1;
+     [ apply (λU.minus_image ?? t U);
+     | intros; apply (#‡e); ]
+  | intros; split; intro;
+     [ change in f with (∀a. a ∈ image ?? t p → a ∈ q);
+       change with (∀a:o1. a ∈ p → a ∈ star_image ?? t q);
+       intros 4; apply f; exists; [apply a] split; assumption;
+     | change in f with (∀a:o1. a ∈ p → a ∈ star_image ?? t q);
+       change with (∀a. a ∈ image ?? t p → a ∈ q);
+       intros; cases f1; cases x; clear f1 x; apply (f ? f3); assumption; ]
+  | intros; split; intro;
+     [ change in f with (∀a. a ∈ minus_image ?? t p → a ∈ q);
+       change with (∀a:o2. a ∈ p → a ∈ minus_star_image ?? t q);
+       intros 4; apply f; exists; [apply a] split; assumption;
+     | change in f with (∀a:o2. a ∈ p → a ∈ minus_star_image ?? t q);
+       change with (∀a. a ∈ minus_image ?? t p → a ∈ q);
+       intros; cases f1; cases x; clear f1 x; apply (f ? f3); assumption; ]
+  | intros; split; intro; cases f; clear f;
+     [ cases x; cases x2; clear x x2; exists; [apply w1]
+        [ assumption;
+        | exists; [apply w] split; assumption]
+     | cases x1; cases x2; clear x1 x2; exists; [apply w1]
+        [ exists; [apply w] split; assumption;
+        | assumption; ]]]
+qed. sistemare anche l'hint da un'altra parte e capire l'exT (doppio!)
\ No newline at end of file
diff --git a/helm/software/matita/contribs/formal_topology/overlap/subsets.ma b/helm/software/matita/contribs/formal_topology/overlap/subsets.ma
index 9847d4c55..73872bfed 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/subsets.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/subsets.ma
@@ -16,7 +16,7 @@ include "categories.ma".
 
 record powerset_carrier (A: objs1 SET) : Type1 ≝ { mem_operator: unary_morphism1 A CPROP }.
 
-definition subseteq_operator: ∀A: SET. powerset_carrier A → powerset_carrier A → CProp1 ≝
+definition subseteq_operator: ∀A: SET. powerset_carrier A → powerset_carrier A → CProp0 ≝
  λA:objs1 SET.λU,V.∀a:A. mem_operator ? U a → mem_operator ? V a.
 
 theorem transitive_subseteq_operator: ∀A. transitive2 ? (subseteq_operator A).
@@ -147,14 +147,14 @@ definition big_intersects:
   [ intro; whd; whd in I;
     apply ({x | ∀i:I. x ∈ t i});
     simplify; intros; split; intros; [ apply (. (e‡#)); | apply (. (e \sup -1‡#)); ]
-    apply H;
+    apply f;
   | intros; split; intros 2; simplify in f ⊢ %; intro;
      [ apply (. (#‡(e i))); apply f;
      | apply (. (#‡(e i)\sup -1)); apply f]]
 qed.
 
 (* senza questo exT "fresco", universe inconsistency *)
-inductive exT (A:Type) (P:A→CProp) : CProp ≝
+inductive exT (A:Type0) (P:A→CProp0) : CProp0 ≝
   ex_introT: ∀w:A. P w → exT A P.
 
 definition big_union:
@@ -162,7 +162,7 @@ definition big_union:
  intros; constructor 1;
   [ intro; whd; whd in A; whd in I;
     apply ({x | (*∃i:carr I. x ∈ t i*) exT (carr I) (λi. x ∈ t i)});
-    simplify; intros; split; intros; cases H; clear H; exists; [1,3:apply w]
+    simplify; intros; split; intros; cases e1; clear e1; exists; [1,3:apply w]
     [ apply (. (e‡#)); | apply (. (e \sup -1‡#)); ]
     apply x;
   | intros; split; intros 2; simplify in f ⊢ %; cases f; clear f; exists; [1,3:apply w]
@@ -208,8 +208,8 @@ definition SUBSETS: objs1 SET → OAlgebra.
         | (* senza questa change, universe inconsistency *)
           whd; change in ⊢ (? ? (λ_:%.?)) with (carr I);
           exists; [apply w] assumption]]
-  | intros; intros 2; cases (H (singleton ? a) ?);
+  | intros; intros 2; cases (f (singleton ? a) ?);
      [ exists; [apply a] [assumption | change with (a = a); apply refl1;]
      | change in x1 with (a = w); change with (mem A a q); apply (. (x1 \sup -1‡#));
        assumption]]
-qed.
\ No newline at end of file
+qed.
-- 
2.39.2